diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,21 @@
+MIT License
+
+Copyright (c) 2016 Dima Szamozvancev
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/app/Main.hs b/app/Main.hs
new file mode 100644
--- /dev/null
+++ b/app/Main.hs
@@ -0,0 +1,6 @@
+module Main where
+
+import Lib
+
+main :: IO ()
+main = someFunc
diff --git a/mezzo.cabal b/mezzo.cabal
new file mode 100644
--- /dev/null
+++ b/mezzo.cabal
@@ -0,0 +1,72 @@
+name:                mezzo
+version:             0.1.0.0
+synopsis:            Typesafe music composition
+description:         A Haskell music composition library that enforces common
+                     musical rules in the type system.
+homepage:            https://github.com/DimaSamoz/mezzo#readme
+license:             BSD3
+license-file:        LICENSE
+author:              Dima Szamozvancev
+maintainer:          ds709@cam.ac.uk
+copyright:           2016 Dima Samozvancev
+category:            Music
+build-type:          Simple
+-- extra-source-files:
+cabal-version:       >=1.10
+
+library
+  hs-source-dirs:      src
+  exposed-modules:     Lib
+                     , Mezzo
+                     , Mezzo.Model
+                     , Mezzo.Model.Prim
+                     , Mezzo.Model.Music
+                     , Mezzo.Model.Types
+                     , Mezzo.Model.Harmony.Motion
+                     , Mezzo.Model.Harmony.Chords
+                     , Mezzo.Model.Harmony.Functional
+                     , Mezzo.Model.Reify
+
+                     , Mezzo.Compose.Types
+                     , Mezzo.Compose.Builder
+                     , Mezzo.Compose.Templates
+                     , Mezzo.Compose.Basic
+                     , Mezzo.Compose.Harmonic
+                     , Mezzo.Compose.Combine
+
+                     , Mezzo.Render.MIDI
+
+  build-depends:       base >= 4.7 && < 5
+                     , ghc-typelits-natnormalise
+                     , template-haskell
+                     , HCodecs
+                     , boxes
+  default-language:    Haskell2010
+
+executable mezzo-exe
+  hs-source-dirs:      app
+  main-is:             Main.hs
+  ghc-options:         -threaded -rtsopts -with-rtsopts=-N
+  build-depends:       base
+                     , mezzo
+  default-language:    Haskell2010
+
+test-suite mezzo-test
+  type:                exitcode-stdio-1.0
+  hs-source-dirs:      test
+  main-is:             Main.hs
+  other-modules:       Main
+                     , PrimSpec
+                     , TypeSpec
+  build-depends:       base
+                     , mezzo
+                     , hspec
+                     , QuickCheck
+                    --  , deepseq
+                     , should-not-typecheck
+  ghc-options:         -threaded -rtsopts -with-rtsopts=-N
+  default-language:    Haskell2010
+
+source-repository head
+  type:     git
+  location: https://github.com/DimaSamoz/mezzo
diff --git a/src/Lib.hs b/src/Lib.hs
new file mode 100644
--- /dev/null
+++ b/src/Lib.hs
@@ -0,0 +1,6 @@
+module Lib
+    ( someFunc
+    ) where
+
+someFunc :: IO ()
+someFunc = putStrLn "someFunc"
diff --git a/src/Mezzo.hs b/src/Mezzo.hs
new file mode 100644
--- /dev/null
+++ b/src/Mezzo.hs
@@ -0,0 +1,6 @@
+module Mezzo
+    ( someFunc
+    ) where
+
+someFunc :: IO ()
+someFunc = putStrLn "someFunc"
diff --git a/src/Mezzo/Compose/Basic.hs b/src/Mezzo/Compose/Basic.hs
new file mode 100644
--- /dev/null
+++ b/src/Mezzo/Compose/Basic.hs
@@ -0,0 +1,94 @@
+{-# LANGUAGE TypeInType, TypeApplications, TemplateHaskell, RankNTypes, FlexibleContexts, GADTs #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Mezzo.Compose.Basic
+-- Description :  Basic composition units
+-- Copyright   :  (c) Dima Szamozvancev
+-- License     :  MIT
+--
+-- Maintainer  :  ds709@cam.ac.uk
+-- Stability   :  experimental
+-- Portability :  portable
+--
+-- Literals for pitches, notes, durations, etc.
+--
+-----------------------------------------------------------------------------
+
+module Mezzo.Compose.Basic where
+
+import GHC.TypeLits
+import Data.Kind
+import Control.Monad
+
+import Mezzo.Model
+import Mezzo.Compose.Types
+import Mezzo.Compose.Builder
+import Mezzo.Compose.Templates
+
+-- * Atomic literals
+
+-- ** Pitch class literals
+pitchClassLits
+
+-- ** Accidental literals
+accidentalLits
+
+-- ** Octave literals
+octaveLits
+
+-- ** Duration literals and terminators
+join <$> traverse mkDurLits [''Whole, ''Half, ''Quarter, ''Eighth, ''Sixteenth]
+
+mk32ndLits
+
+-- * Pitches
+
+-- ** Constructor
+
+-- | Create a new pitch with the given class, accidental and octave.
+pitch :: Primitive (Pitch pc acc oct) => PC pc -> Acc acc -> Oct oct -> Pit (Pitch pc acc oct)
+pitch pc acc oct = Pit
+
+-- | Value representing silence, the "pitch" of rests.
+silence :: Pit Silence
+silence = Pit
+
+-- ** Concrete literals
+mkPitchLits
+
+-- ** Pitch specifiers (admitting continuations)
+mkPitchSpecs
+
+r :: RestS
+r dur = dur Pit
+-- | Raise a pitch by a semitone.
+sharp :: RootM r (Sharpen r)
+sharp = constConv Root
+
+-- | Lower a pitch by a semitone.
+flat :: RootM r (Flatten r)
+flat = constConv Root
+
+-- * Notes
+
+-- ** Constructors
+-- | Create a new root from a pitch.
+rootP :: IntRep p => Pit p -> Root (PitchRoot p)
+rootP p = Root
+
+-- | Create a new root from a key and a scale degree.
+rootS :: Primitive (DegreeRoot k d) => KeyS k -> ScaDeg d -> Root (DegreeRoot k d)
+rootS k d = Root
+
+-- | Create a new note from a root and duration.
+noteP :: (Primitive d, IntRep p) => Pit p -> Dur d -> Music (FromRoot (PitchRoot p) d)
+noteP p = Note (rootP p)
+
+noteS :: (Primitive d, IntRep (DegreeRoot k sd))
+      => KeyS k -> ScaDeg sd -> Dur d -> Music (FromRoot (DegreeRoot k sd) d)
+noteS k sd = Note (rootS k sd)
+
+-- | Create a rest from a duration.
+rest :: Primitive d => Dur d -> Music (FromSilence d)
+rest = Rest
diff --git a/src/Mezzo/Compose/Builder.hs b/src/Mezzo/Compose/Builder.hs
new file mode 100644
--- /dev/null
+++ b/src/Mezzo/Compose/Builder.hs
@@ -0,0 +1,203 @@
+{-# LANGUAGE TypeInType, RankNTypes, ExistentialQuantification, GADTs #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Mezzo.Compose.Builder
+-- Description :  Music builder
+-- Copyright   :  (c) Dima Szamozvancev
+-- License     :  MIT
+--
+-- Maintainer  :  ds709@cam.ac.uk
+-- Stability   :  experimental
+-- Portability :  portable
+--
+-- Pattern of combinatorially building musical terms of various types.
+--
+-----------------------------------------------------------------------------
+
+module Mezzo.Compose.Builder
+    (
+    -- * General builder types
+      Spec
+    , Conv
+    , Mut
+    , Term
+    , AConv
+    , AMut
+    , Mut'
+    , spec
+    , constConv
+    -- * Music-specific builder types
+    , RootS
+    , RestS
+    , ChorS
+    , RootM
+    , ChorM
+    , ChorC
+    , ChorC'
+    , RootT
+    , RestT
+    , ChorT
+    )
+    where
+
+import Mezzo.Model
+
+import GHC.TypeLits
+
+-------------------------------------------------------------------------------
+-- General types
+-------------------------------------------------------------------------------
+
+-- | Specifier: specifies a value of some type which starts the building.
+type Spec t = forall m. (t -> m) -> m
+
+-- | Converter: converts a value of type s to a value of type t.
+type Conv s t = s -> Spec t
+
+-- | Mutator: mutates a value of type t.
+type Mut t = Conv t t
+
+-- | Terminator: finishes building a value of type t and returns a result of type r.
+type Term t r = t -> r
+
+-- | Converter with argument: converts a value of type s to a value of type t, consuming an argument of type a.
+type AConv a s t = s -> a -> Spec t
+
+-- | Mutator with argument: mutates a value of type t, consuming an argument of type a.
+type AMut a t = AConv a t t
+
+-- | Flexible mutator: mutator that allows slight changes in the type (otherwise use 'Conv').
+type Mut' t t' = Conv t t'
+
+-- | Returns a new specifier for the given value.
+spec :: t -> Spec t
+spec i c = c i
+
+-- | A converter that ignores its argument and returns the given constant value.
+constConv :: t -> Conv s t
+constConv = const . spec
+
+-- | A mutator that does nothing.
+nop :: Mut t
+nop = spec
+
+-------------------------------------------------------------------------------
+-- Music specific types
+-------------------------------------------------------------------------------
+
+-- | Root specifier.
+type RootS r = Primitive r => Spec (Root r)
+
+-- | Rest specifier.
+type RestS = Spec (Pit Silence)
+
+-- | Chord specifier.
+type ChorS c = Primitive c => Spec (Cho c)
+
+-- | Root mutator.
+type RootM r r' = (Primitive r, Primitive r') => Mut' (Root r) (Root r')
+
+-- | Chord mutator.
+type ChorM c c' = (Primitive c, Primitive c') => Mut' (Cho c) (Cho c')
+
+-- | Converter from roots to chords.
+type ChorC' c r t i = (Primitive r, Primitive t, Primitive i) => AConv (Inv i) (Root r) (Cho (c r t i))
+
+-- | Converter from roots to chords, using the default inversion.
+type ChorC c r t = (Primitive r, Primitive t) => Conv (Root r) (Cho (c r t Inv0))
+
+-- | Note terminator.
+type RootT r d = Primitive r => Term (Root r) (Music (FromRoot r d))
+
+--  | Rest terminator.
+type RestT d = Term (Pit Silence) (Music (FromSilence d))
+
+-- | Chord terminator.
+type ChorT c d = Primitive c => Term (Cho c) (Music (FromChord c d))
+
+-- inKey :: KeyS key -> a -> a
+-- inKey key cont = let ?k = key in cont
+--
+--
+-- i :: (?k :: KeyS key) => RootS (DegreeRoot key I)
+-- i = spec Root
+--
+-- c :: RootS (PitchRoot (Pitch C Natural Oct3))
+-- c = spec Root
+--
+-- sharp :: RootM r (Sharpen r)
+-- sharp = constConv Root
+--
+-- maj :: ChorC Triad r MajTriad
+-- maj = constConv Cho
+--
+-- qn :: RootT r 8
+-- qn p = Note p Dur
+--
+-- qc :: KnownNat n => ChorT (c :: ChordType n) 8
+-- qc c = Chord c Dur
+
+
+-------------------------------------------------------------------------------
+-- Silly examples
+-- Most of these are quite pointless, but show that the pattern enables us to
+-- write DSLs with a very fluent feel.
+-------------------------------------------------------------------------------
+
+inc :: Mut Int
+inc i = spec (succ i)
+
+toString :: Conv Int String
+toString n = spec (show n)
+
+ex :: Mut String
+ex s = spec (s ++ "!")
+
+smile :: Term String String
+smile s = s ++ " :)"
+
+say :: String -> Spec String
+say = spec
+
+add :: Int -> Spec Int
+add = spec
+
+and' :: Mut t
+and' = nop
+
+to :: Int -> Mut Int
+to y x = spec (x + y)
+
+display :: Conv Int String
+display = spec . show
+
+result :: Term String String
+result = ("result: " ++)
+
+compute :: Double -> Spec Double
+compute = spec
+
+plus :: AMut Double Double
+plus i p = spec (i + p)
+
+please :: Term Double Double
+please = id
+
+percent :: Mut Double
+percent = nop
+
+of' :: Double -> Mut Double
+of' d p = spec (d * (p / 100))
+
+stack :: Spec [Int]
+stack = spec []
+
+push :: AMut Int [Int]
+push s v = spec (v : s)
+
+pop :: Mut [Int]
+pop = spec . tail
+
+end :: Term [Int] [Int]
+end = id
diff --git a/src/Mezzo/Compose/Combine.hs b/src/Mezzo/Compose/Combine.hs
new file mode 100644
--- /dev/null
+++ b/src/Mezzo/Compose/Combine.hs
@@ -0,0 +1,120 @@
+{-# LANGUAGE TypeInType, TypeApplications, TypeOperators, FlexibleContexts, RankNTypes,
+    FlexibleInstances, ScopedTypeVariables, GADTs, TypeFamilies #-}
+{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Mezzo.Compose.Combine
+-- Description :  Music combinators
+-- Copyright   :  (c) Dima Szamozvancev
+-- License     :  MIT
+--
+-- Maintainer  :  ds709@cam.ac.uk
+-- Stability   :  experimental
+-- Portability :  portable
+--
+-- Properties and combinators for 'Music' values.
+--
+-----------------------------------------------------------------------------
+
+module Mezzo.Compose.Combine
+    (
+    -- * Music properties and padding
+      musicDur
+    , durToInt
+    , duration
+    , voices
+    , pad
+    -- * Melody composition
+    , play
+    ) where
+
+import Mezzo.Model
+import Mezzo.Compose.Basic
+import Mezzo.Compose.Builder
+import Mezzo.Compose.Types
+import Mezzo.Model.Prim
+import Mezzo.Model.Types
+import Mezzo.Model.Music
+
+import GHC.TypeLits
+
+-------------------------------------------------------------------------------
+-- Music properties
+-------------------------------------------------------------------------------
+
+-- | Get the duration of a piece of music.
+musicDur :: Primitive l => Music (m :: Partiture n l) -> Dur l
+musicDur _ = Dur
+
+-- | Convert a duration to an integer.
+durToInt :: Primitive d => Dur d -> Int
+durToInt = prim
+
+-- | Get the numeric duration of a piece of music.
+duration :: Primitive l => Music (m :: Partiture n l) -> Int
+duration = durToInt . musicDur
+
+-- | Get the number of voices in a piece of music.
+voices :: Music m -> Int
+voices (Note r d) = 1
+voices (Rest d) = 1
+voices (m1 :|: m2) = voices m1
+voices (m1 :-: m2) = voices m1 + voices m2
+voices (Chord c d) = chordVoices c
+
+-- | Get the number of voices in a chord.
+-- Thanks to Michael B. Gale
+chordVoices :: forall (n :: Nat) (c :: ChordType n) . Primitive n => Cho c -> Int
+chordVoices _ = prim (undefined :: ChordType n) -- Need to get a kind-level variable to the term level
+
+-- | Add an empty voice to the end of a piece of music.
+pad :: (HarmConstraints m (FromSilence b), Primitive b) => Music (m :: Partiture (a - 1) b) -> Music ((m +-+ FromSilence b) :: Partiture a b)
+pad m = m :-: rest (musicDur m)
+
+-------------------------------------------------------------------------------
+-- Melodies
+-------------------------------------------------------------------------------
+
+-- | Convert a melody (a sequence of notes and rests) to `Music`.
+play :: (Primitive d) => Melody m d -> Music m
+play m@(ps :| p)    = case ps of Melody -> mkMelNote m p ; ps' -> play ps' :|: mkMelNote m p
+play m@(ps :<<< p)  = case ps of Melody -> mkMelNote m p ; ps' -> play ps' :|: mkMelNote m p
+play m@(ps :<< p)   = case ps of Melody -> mkMelNote m p ; ps' -> play ps' :|: mkMelNote m p
+play m@(ps :< p)    = case ps of Melody -> mkMelNote m p ; ps' -> play ps' :|: mkMelNote m p
+play m@(ps :^ p)    = case ps of Melody -> mkMelNote m p ; ps' -> play ps' :|: mkMelNote m p
+play m@(ps :> p)    = case ps of Melody -> mkMelNote m p ; ps' -> play ps' :|: mkMelNote m p
+play m@(ps :>> p)   = case ps of Melody -> mkMelNote m p ; ps' -> play ps' :|: mkMelNote m p
+play m@(ps :<<. p)  = case ps of Melody -> mkMelNote m p ; ps' -> play ps' :|: mkMelNote m p
+play m@(ps :<. p)   = case ps of Melody -> mkMelNote m p ; ps' -> play ps' :|: mkMelNote m p
+play m@(ps :^. p)   = case ps of Melody -> mkMelNote m p ; ps' -> play ps' :|: mkMelNote m p
+play m@(ps :>. p)   = case ps of Melody -> mkMelNote m p ; ps' -> play ps' :|: mkMelNote m p
+play m@(ps :>>. p)  = case ps of Melody -> mkMelNote m p ; ps' -> play ps' :|: mkMelNote m p
+play m@(ps :~| p)   = case ps of Melody -> mkMelRest m ; ps' -> play ps'   :|: mkMelRest m
+play m@(ps :~<<< p) = case ps of Melody -> mkMelRest m ; ps' -> play ps'   :|: mkMelRest m
+play m@(ps :~<< p)  = case ps of Melody -> mkMelRest m ; ps' -> play ps'   :|: mkMelRest m
+play m@(ps :~< p)   = case ps of Melody -> mkMelRest m ; ps' -> play ps'   :|: mkMelRest m
+play m@(ps :~^ p)   = case ps of Melody -> mkMelRest m ; ps' -> play ps'   :|: mkMelRest m
+play m@(ps :~> p)   = case ps of Melody -> mkMelRest m ; ps' -> play ps'   :|: mkMelRest m
+play m@(ps :~>> p)  = case ps of Melody -> mkMelRest m ; ps' -> play ps'   :|: mkMelRest m
+play m@(ps :~<<. p) = case ps of Melody -> mkMelRest m ; ps' -> play ps'   :|: mkMelRest m
+play m@(ps :~<. p)  = case ps of Melody -> mkMelRest m ; ps' -> play ps'   :|: mkMelRest m
+play m@(ps :~^. p)  = case ps of Melody -> mkMelRest m ; ps' -> play ps'   :|: mkMelRest m
+play m@(ps :~>. p)  = case ps of Melody -> mkMelRest m ; ps' -> play ps'   :|: mkMelRest m
+play m@(ps :~>>. p) = case ps of Melody -> mkMelRest m ; ps' -> play ps'   :|: mkMelRest m
+
+-- | Make a note of suitable duration from a root specifier.
+mkMelNote :: (IntRep r, Primitive d) => Melody m d -> RootS r -> Music (FromRoot r d)
+mkMelNote m p = p (\r -> Note r (melDur m))
+
+-- | Make a rest of suitable duration from a rest specifier.
+mkMelRest :: Primitive d => Melody m d -> Music (FromSilence d)
+mkMelRest m = r (\_ -> Rest (melDur m))
+
+-- | Alias for the start of the melody.
+melody :: Melody (End :-- None) Quarter
+melody = Melody
+
+-- | Get the duration of the notes in a melody.
+melDur :: Primitive d => Melody m d -> Dur d
+melDur _ = Dur
diff --git a/src/Mezzo/Compose/Harmonic.hs b/src/Mezzo/Compose/Harmonic.hs
new file mode 100644
--- /dev/null
+++ b/src/Mezzo/Compose/Harmonic.hs
@@ -0,0 +1,74 @@
+{-# LANGUAGE TypeInType, TypeApplications, TemplateHaskell, RankNTypes,
+    GADTs, ImplicitParams, FlexibleContexts #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Mezzo.Compose.Harmonic
+-- Description :  Harmonic composition units
+-- Copyright   :  (c) Dima Szamozvancev
+-- License     :  MIT
+--
+-- Maintainer  :  ds709@cam.ac.uk
+-- Stability   :  experimental
+-- Portability :  portable
+--
+-- Literals for chords and progressions.
+--
+-----------------------------------------------------------------------------
+
+module Mezzo.Compose.Harmonic where
+
+import Mezzo.Model
+import Mezzo.Compose.Types
+import Mezzo.Compose.Builder
+import Mezzo.Compose.Templates
+import Mezzo.Compose.Basic
+
+-- * Atomic literals
+
+-- ** Scale degree literals
+scaleDegreeLits
+
+-- ** Mode literals
+modeLits
+
+-- ** Triad type literals
+triTyLits
+
+-- ** Seventh type literals
+sevTyLits
+
+_dbl :: TriType t -> SevType (Doubled t)
+_dbl t = SevType
+
+-- ** Inversion literals
+invLits
+
+-- ** Constructors
+
+-- | Create a new key from a pitch class, accidental and mode.
+key :: PC p -> Acc a -> Mod m -> KeyS (Key p a m)
+key p a m = KeyS
+
+-- | Create a triad from a root, a triad type and an inversion.
+triad :: Root r -> TriType t -> Inv i -> Cho (Triad r t i)
+triad r t i = Cho
+
+-- | Create a seventh chord from a root, a triad type and an inversion.
+seventh :: Root r -> SevType t -> Inv i -> Cho (SeventhChord r t i)
+seventh r t i = Cho
+
+-- * Chord builders
+
+-- ** Triad converters
+mkTriConvs
+
+-- ** Seventh chord converters
+mkSevConvs
+
+-- ** Doubled triad converters
+mkDoubledConvs
+
+-- ** Inversion mutators
+inv :: ChorM c (InvertChord c)
+inv = constConv Cho
diff --git a/src/Mezzo/Compose/Templates.hs b/src/Mezzo/Compose/Templates.hs
new file mode 100644
--- /dev/null
+++ b/src/Mezzo/Compose/Templates.hs
@@ -0,0 +1,344 @@
+{-# LANGUAGE TypeInType, TemplateHaskell, ExplicitForAll, ViewPatterns #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Mezzo.Compose.Templates
+-- Description :  TH templates
+-- Copyright   :  (c) Dima Szamozvancev
+-- License     :  MIT
+--
+-- Maintainer  :  ds709@cam.ac.uk
+-- Stability   :  experimental
+-- Portability :  portable
+--
+-- Template Haskell functions to generate music literals.
+--
+-----------------------------------------------------------------------------
+
+module Mezzo.Compose.Templates
+    ( pitchClassLits
+    , accidentalLits
+    , octaveLits
+    , mkDurLits
+    , mk32ndLits
+    , mkPitchLits
+    , mkPitchSpecs
+    , scaleDegreeLits
+    , modeLits
+    , triTyLits
+    , sevTyLits
+    , invLits
+    , mkTriConvs
+    , mkSevConvs
+    , mkDoubledConvs
+    ) where
+
+import Mezzo.Model
+import Mezzo.Compose.Types
+import Mezzo.Compose.Builder
+
+import Language.Haskell.TH
+import Language.Haskell.TH.Syntax (sequenceQ)
+import Data.Char
+import Control.Monad (join)
+
+
+-------------------------------------------------------------------------------
+-- Literal templates
+-------------------------------------------------------------------------------
+
+-- | Generate pitch class literal declarations.
+pitchClassLits :: DecsQ
+pitchClassLits = genLitDecs pcFormatter "PC" ''PitchClass
+
+-- | Generate accidental literal declarations.
+accidentalLits :: DecsQ
+accidentalLits = genLitDecs accFormatter "Acc" ''Accidental
+
+-- | Generate octave literal declarations.
+octaveLits :: DecsQ
+octaveLits = genLitDecs octFormatter "Oct" ''OctaveNum
+
+-- | Generate scale degree literal declarations.
+scaleDegreeLits :: DecsQ
+scaleDegreeLits = genLitDecs scaDegFormatter "ScaDeg" ''ScaleDegree
+
+-- | Generate mode literal declarations.
+modeLits :: DecsQ
+modeLits = genLitDecs modeFormatter "Mod" ''Mode -- Might want to extend modes later
+
+-- | Generate triad type literal declarations.
+triTyLits :: DecsQ
+triTyLits = genLitDecs choTyFormatter "TriType" ''TriadType
+
+-- | Generate seventh type literal declarations.
+sevTyLits :: DecsQ
+sevTyLits = do
+    dcs <- filter (\n -> nameBase n /= "Doubled") <$> getDataCons ''SeventhType
+    join <$> traverse (mkSingLit choTyFormatter "SevType") dcs
+
+invLits :: DecsQ
+invLits = genLitDecs invFormatter "Inv" ''Inversion
+
+-------------------------------------------------------------------------------
+-- Templates and generators
+-------------------------------------------------------------------------------
+
+-- | Make a literal value declaration for a singleton with the given format string,
+-- singleton name and data constructor.
+mkSingLit :: Formatter -> String -> Name -> DecsQ
+mkSingLit format sing dataName = do
+        tySig <- sigD valName $ appT pcTyCon ty
+        dec <- [d| $(valPat) = $(pcDataCon) |]
+        return $ tySig : dec
+    where
+        valName = mkName (format dataName)
+        valPat = varP valName
+        pcTyCon = conT $ mkName sing
+        ty = promotedT dataName
+        pcDataCon = conE $ mkName sing
+
+-- | Generate concrete pitch literals for each pitch class, accidental and octave.
+mkPitchLits :: DecsQ
+mkPitchLits = do
+    pcNames <- getDataCons ''PitchClass
+    accNames <- getDataCons ''Accidental
+    octNames <- getDataCons ''OctaveNum
+    let declareVal pc acc oct = do  -- Generates a type signature and value declaration for the specified pitch
+            let pcStr = pcFormatter pc
+                accStr = shortAccFormatter acc
+                octStr = shortOctFormatter oct
+                valName = mkName $ pcStr ++ accStr ++ octStr
+            tySig <- sigD valName $ [t| Pit (Pitch $(conT pc) $(conT acc) $(conT oct)) |]
+            dec <- [d| $(varP valName) = pitch $(varE $ mkName pcStr) $(varE $ mkName (accFormatter acc)) $(varE $ mkName (octFormatter oct)) |]
+            return $ tySig : dec
+    join <$> sequence (declareVal <$> pcNames <*> accNames <*> octNames)    -- Every combination of PCs, Accs and Octs
+
+mkDurLits :: Name -> DecsQ
+mkDurLits name = do
+    let litName = mkName $ durLitFormatter name
+        litName' = mkName $ (durLitFormatter name ++ "\'")
+    literal <- do
+            tySig1 <- sigD litName $ [t| Dur $(conT name) |]
+            dec1 <- [d| $(varP litName) = Dur |]
+            tySig1' <- sigD litName' $ [t| Dur (Dot $(conT name)) |]
+            dec1' <- [d| $(varP litName') = Dur |]
+            return $ tySig1 : dec1 ++ tySig1' : dec1'
+    noteTerm <- do
+            let valName = mkName $ head (durLitFormatter name) : "n"
+            tySig2 <- sigD valName $ [t| forall r. IntRep r => RootT r $(conT name) |]
+            dec2 <- [d| $(varP valName) = \p -> Note p $(varE litName) |]
+            let valName' = mkName $ head (durLitFormatter name) : "n\'"
+            tySig2' <- sigD valName' $ [t| forall r. IntRep r => RootT r (Dot $(conT name)) |]
+            dec2' <- [d| $(varP valName') = \p -> Note p $(varE litName') |]
+            return $ tySig2 : dec2 ++ tySig2' : dec2'
+    restTerm <- do
+            let valName = mkName $ head (durLitFormatter name) : "r"
+            tySig2 <- sigD valName $ [t| RestT $(conT name) |]
+            dec2 <- [d| $(varP valName) = const (Rest $(varE litName)) |]
+            let valName' = mkName $ head (durLitFormatter name) : "r\'"
+            tySig2' <- sigD valName' $ [t| RestT (Dot $(conT name)) |]
+            dec2' <- [d| $(varP valName') = const (Rest $(varE litName')) |]
+            return $ tySig2 : dec2 ++ tySig2' : dec2'
+    chordTerm <- do
+            let valName = mkName $ head (durLitFormatter name) : "c"
+            tySig2 <- sigD valName $ [t| forall n r. (Primitive n, IntListRep r) => ChorT (r :: ChordType n) $(conT name) |]
+            dec2 <- [d| $(varP valName) = \c -> Chord c $(varE litName) |]
+            let valName' = mkName $ head (durLitFormatter name) : "c\'"
+            tySig2' <- sigD valName' $ [t| forall n r. (Primitive n, IntListRep r) => ChorT (r :: ChordType n) (Dot $(conT name)) |]
+            dec2' <- [d| $(varP valName') = \c -> Chord c $(varE litName') |]
+            return $ tySig2 : dec2 ++ tySig2' : dec2'
+    return $ literal ++ noteTerm ++ restTerm ++ chordTerm
+
+mk32ndLits :: DecsQ -- Don't want to make dotted literals for thirty second notes.
+mk32ndLits = do
+    let litName = mkName $ "th"
+    literal <- do
+            tySig1 <- sigD litName $ [t| Dur $(conT ''ThirtySecond) |]
+            dec1 <- [d| $(varP litName) = Dur |]
+            return $ tySig1 : dec1
+    noteTerm <- do
+            let valName = mkName $ "tn"
+            tySig2 <- sigD valName $ [t| forall r. IntRep r => RootT r $(conT ''ThirtySecond) |]
+            dec2 <- [d| $(varP valName) = \p -> Note p $(varE litName) |]
+            return $ tySig2 : dec2
+    restTerm <- do
+            let valName = mkName $ "tr"
+            tySig2 <- sigD valName $ [t| RestT $(conT ''ThirtySecond) |]
+            dec2 <- [d| $(varP valName) = const (Rest $(varE litName)) |]
+            return $ tySig2 : dec2
+    chordTerm <- do
+            let valName = mkName $ "tc"
+            tySig2 <- sigD valName $ [t| forall n r. (Primitive n, IntListRep r) => ChorT (r :: ChordType n) $(conT ''ThirtySecond) |]
+            dec2 <- [d| $(varP valName) = \c -> Chord c $(varE litName)  |]
+            return $ tySig2 : dec2
+    return $ literal ++ noteTerm ++ restTerm ++ chordTerm
+
+-- | Generate pitch root specifiers for earch pitch class, accidental and octave.
+-- These allow for combinatorial input with CPS-style durations and modifiers.
+mkPitchSpecs :: DecsQ
+mkPitchSpecs = do
+    pcNames <- getDataCons ''PitchClass
+    accNames <- getDataCons ''Accidental
+    octNames <- getDataCons ''OctaveNum
+    let declareVal pc acc oct = do
+            let pcStr = tail $ pcFormatter pc
+                accStr = shorterAccFormatter acc
+                octStr = shortOctFormatter oct
+                valName = mkName $ pcStr ++ accStr ++ octStr
+            tySig <- sigD valName $
+                [t| RootS (PitchRoot (Pitch $(conT pc) $(conT acc) $(conT oct) )) |]
+            dec <- [d| $(varP valName) = spec Root |]
+            return $ tySig : dec
+    join <$> sequence (declareVal <$> pcNames <*> accNames <*> octNames)
+
+-- | Generate converters from roots to triads, for each triad type.
+mkTriConvs :: DecsQ
+mkTriConvs = do
+    triTyNames <- getDataCons ''TriadType
+    let declareFun choTy = do
+            let choStr = tail (choTyFormatter choTy)
+                valName1 = mkName $ choStr ++ "'"
+                valName2 = mkName $ choStr
+            tySig1 <- sigD valName1 $
+                [t| forall r i. ChorC' Triad r $(conT choTy) i |]
+            dec1 <- [d| $(varP valName1) = \i -> constConv Cho |]
+            tySig2 <- sigD valName2 $
+                [t| forall r. ChorC Triad r $(conT choTy) |]
+            dec2 <- [d| $(varP valName2) = constConv Cho |]
+            return $ (tySig1 : dec1) ++ (tySig2 : dec2)
+    join <$> traverse declareFun triTyNames
+
+-- | Generate converters from roots to seventh chords, for each seventh type.
+mkSevConvs :: DecsQ
+mkSevConvs = do
+    sevTyNames <- filter (\n -> nameBase n /= "Doubled") <$> getDataCons ''SeventhType
+    let declareFun choTy = do
+            let choStr = tail (choTyFormatter choTy)
+                valName1 = mkName $ choStr ++ "'"
+                valName2 = mkName $ choStr
+            tySig1 <- sigD valName1 $
+                [t| forall r i. ChorC' SeventhChord r $(conT choTy) i |]
+            dec1 <- [d| $(varP valName1) = \i -> constConv Cho |]
+            tySig2 <- sigD valName2 $
+                [t| forall r. ChorC SeventhChord r $(conT choTy) |]
+            dec2 <- [d| $(varP valName2) = constConv Cho |]
+            return $ (tySig1 : dec1) ++ (tySig2 : dec2)
+    join <$> traverse declareFun sevTyNames
+
+-- | Generate converters from roots to doubled seventh chords, for each triad type.
+mkDoubledConvs :: DecsQ
+mkDoubledConvs = do
+    triTyNames <- getDataCons ''TriadType
+    let declareFun choTy = do
+            let choStr = tail (choTyFormatter choTy)
+                valName1 = mkName $ choStr ++ "D'"
+                valName2 = mkName $ choStr ++ "D"
+            tySig1 <- sigD valName1 $
+                [t| forall r i. ChorC' SeventhChord r (Doubled $(conT choTy)) i |]
+            dec1 <- [d| $(varP valName1) = \i -> constConv Cho |]
+            tySig2 <- sigD valName2 $
+                [t| forall r. ChorC SeventhChord r (Doubled $(conT choTy)) |]
+            dec2 <- [d| $(varP valName2) = constConv Cho |]
+            return $ (tySig1 : dec1) ++ (tySig2 : dec2)
+    join <$> traverse declareFun triTyNames
+
+
+
+
+-------------------------------------------------------------------------------
+-- Formatters
+-------------------------------------------------------------------------------
+
+-- | Type synonym for a formatter, that specifies how a data constructor name is
+-- diplayed as a literal value.
+type Formatter = Name -> String
+
+-- | 'PitchClass' formatter.
+pcFormatter :: Formatter
+pcFormatter pc = '_' : map toLower (nameBase pc)
+
+-- | 'Accidental' formatter.
+accFormatter :: Formatter
+accFormatter = map toLower . take 2 . nameBase
+
+-- | 'OctaveNum' formatter.
+octFormatter :: Formatter
+octFormatter oct = 'o' : drop 3 (nameBase oct)
+
+-- | One letter accidental with explicit 'Naturals'.
+shortAccFormatter :: Formatter
+shortAccFormatter (accFormatter -> "fl") = "f"
+shortAccFormatter (accFormatter -> name) = [head name]
+
+-- | One letter accidental with implicit 'Naturals'.
+shorterAccFormatter :: Formatter
+shorterAccFormatter (shortAccFormatter -> "n") = ""
+shorterAccFormatter (shortAccFormatter -> name) = name
+
+-- | Symbolic suffix format for octaves.
+shortOctFormatter :: Formatter
+shortOctFormatter name = case nameBase name of
+    "Oct_1" -> "_5"
+    "Oct0"  -> "_4"
+    "Oct1"  -> "_3"
+    "Oct2"  -> "__"
+    "Oct3"  -> "_"
+    "Oct4"  -> ""
+    "Oct5"  -> "'"
+    "Oct6"  -> "''"
+    "Oct7"  -> "'3"
+    "Oct8"  -> "'4"
+
+-- | Formatter for duration literals.
+durLitFormatter :: Formatter
+durLitFormatter = map toLower . take 2 . nameBase
+
+-- | Formatter for pitch literals.
+pitchLitFormatter :: Name -> Name -> Name -> String
+pitchLitFormatter pc acc oct = pcFormatter pc ++ shortAccFormatter acc ++ shortOctFormatter oct
+
+-- | Formatter for scale degrees.
+scaDegFormatter :: Formatter
+scaDegFormatter name = "_" ++ map toLower (nameBase name)
+
+-- | Formatter for key modes.
+modeFormatter :: Formatter
+modeFormatter (nameBase -> name) = map toLower (take 3 name) ++ dropWhile isLower (tail name)
+
+-- | Formatter for chords types.
+choTyFormatter :: Formatter
+choTyFormatter n = case nameBase n of
+    "MajTriad"       -> "_maj"
+    "MinTriad"       -> "_min"
+    "AugTriad"       -> "_aug"
+    "DimTriad"       -> "_dim"
+    "MajSeventh"     -> "_maj7"
+    "MajMinSeventh"  -> "_sev"
+    "MinSeventh"     -> "_min7"
+    "HalfDimSeventh" -> "_hdim7"
+    "DimSeventh"     -> "_dim7"
+
+-- | Formatter for inversions.
+invFormatter :: Formatter
+invFormatter (nameBase -> name) = "i" ++ [last name]
+
+-------------------------------------------------------------------------------
+-- Auxiliary functions
+-------------------------------------------------------------------------------
+
+-- | Get the data constructors of a type.
+getDataCons :: Name -> Q [Name]
+getDataCons tyName = do
+    TyConI (DataD _ _ _ _ dcs _) <- reify tyName
+    return $ reverse $ map (\(NormalC pc _) -> pc) dcs
+
+-- | Map a function generating declarations from a data constructor to all
+-- data constructors of a type.
+mapToDataCons :: (Name -> DecsQ) -> Name -> DecsQ
+mapToDataCons f tyName = do
+    dcNames <- getDataCons tyName
+    join <$> traverse f dcNames
+
+genLitDecs :: Formatter -> String -> Name -> DecsQ
+genLitDecs format singName name = mapToDataCons (mkSingLit format singName) name
diff --git a/src/Mezzo/Compose/Types.hs b/src/Mezzo/Compose/Types.hs
new file mode 100644
--- /dev/null
+++ b/src/Mezzo/Compose/Types.hs
@@ -0,0 +1,172 @@
+{-# LANGUAGE TypeInType, TypeOperators, GADTs, TypeFamilies, MultiParamTypeClasses,
+    FlexibleInstances, UndecidableInstances, ScopedTypeVariables, FlexibleContexts, RankNTypes #-}
+
+{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Mezzo.Compose.Types
+-- Description :  Common types
+-- Copyright   :  (c) Dima Szamozvancev
+-- License     :  MIT
+--
+-- Maintainer  :  ds709@cam.ac.uk
+-- Stability   :  experimental
+-- Portability :  portable
+--
+-- Types used by the composition library.
+--
+-----------------------------------------------------------------------------
+
+module Mezzo.Compose.Types
+    (
+    -- * Duration type synonyms
+      Whole
+    , Half
+    , Quarter
+    , Eighth
+    , Sixteenth
+    , ThirtySecond
+    -- * Melody
+    , Melody (..)
+    )
+    where
+
+import Mezzo.Model
+import Mezzo.Model.Prim
+
+import Mezzo.Compose.Builder
+
+import Data.Kind
+import GHC.TypeLits
+
+infixl 5 :|
+infixl 5 :<<<
+infixl 5 :<<
+infixl 5 :<
+infixl 5 :^
+infixl 5 :>
+infixl 5 :>>
+infixl 5 :<<.
+infixl 5 :<.
+infixl 5 :^.
+infixl 5 :>.
+infixl 5 :>>.
+infixl 5 :~|
+infixl 5 :~<<<
+infixl 5 :~<<
+infixl 5 :~<
+infixl 5 :~^
+infixl 5 :~>
+infixl 5 :~>>
+infixl 5 :~<<.
+infixl 5 :~<.
+infixl 5 :~^.
+infixl 5 :~>.
+infixl 5 :~>>.
+
+-------------------------------------------------------------------------------
+-- Duration type synonyms
+-------------------------------------------------------------------------------
+
+-- | Whole note duration.
+type Whole = 32
+
+-- | Half note duration.
+type Half = 16
+
+-- | Quarter note duration.
+type Quarter = 8
+
+-- | Eighth note duration.
+type Eighth = 4
+
+-- | Sixteenth note duration.
+type Sixteenth = 2
+
+-- | Thirty-second note duration.
+type ThirtySecond = 1
+
+-------------------------------------------------------------------------------
+-- Musical lists
+-------------------------------------------------------------------------------
+
+-- | Single-voice melody: gives an easy way to input notes and rests of different lengths.
+data Melody :: forall l. Partiture 1 l -> Nat -> Type where
+    -- | Start a new melody. If the first note duration is not specified ('(:|)' is used),
+    -- the default duration is a quarter.
+    Melody  :: Melody (End :-- None) Quarter
+    -- | Add a note with the same duration as the previous one.
+    (:|)    :: (MelConstraints ms (FromRoot r d), IntRep r, Primitive d)
+           => Melody ms d -> RootS r -> Melody (ms +|+ FromRoot r d) d
+    -- | Add a thirty-second note.
+    (:<<<)  :: (MelConstraints ms (FromRoot r ThirtySecond), IntRep r, Primitive d)
+           => Melody ms d -> RootS r -> Melody (ms +|+ FromRoot r ThirtySecond) ThirtySecond
+    -- | Add a sixteenth note.
+    (:<<)   :: (MelConstraints ms (FromRoot r Sixteenth), IntRep r, Primitive d)
+           => Melody ms d -> RootS r -> Melody (ms +|+ FromRoot r Sixteenth) Sixteenth
+    -- | Add an eighth note.
+    (:<)    :: (MelConstraints ms (FromRoot r Eighth), IntRep r, Primitive d)
+           => Melody ms d -> RootS r -> Melody (ms +|+ FromRoot r Eighth) Eighth
+    -- | Add a quarter note.
+    (:^)    :: (MelConstraints ms (FromRoot r Quarter), IntRep r, Primitive d)
+           => Melody ms d -> RootS r -> Melody (ms +|+ FromRoot r Quarter) Quarter
+    -- | Add a half note.
+    (:>)    :: (MelConstraints ms (FromRoot r Half), IntRep r, Primitive d)
+           => Melody ms d -> RootS r -> Melody (ms +|+ FromRoot r Half) Half
+    -- | Add a whole note.
+    (:>>)   :: (MelConstraints ms (FromRoot r Whole), IntRep r, Primitive d)
+           => Melody ms d -> RootS r -> Melody (ms +|+ FromRoot r Whole) Whole
+    -- | Add a dotted sixteenth note.
+    (:<<.)  :: (MelConstraints ms (FromRoot r (Dot Sixteenth)), IntRep r, Primitive d)
+           => Melody ms d -> RootS r -> Melody (ms +|+ FromRoot r (Dot Sixteenth)) (Dot Sixteenth)
+    -- | Add a dotted eighth note.
+    (:<.)   :: (MelConstraints ms (FromRoot r (Dot Eighth)), IntRep r, Primitive d)
+           => Melody ms d -> RootS r -> Melody (ms +|+ FromRoot r (Dot Eighth)) (Dot Eighth)
+    -- | Add a dotted quarter note.
+    (:^.)   :: (MelConstraints ms (FromRoot r (Dot Quarter)), IntRep r, Primitive d)
+           => Melody ms d -> RootS r -> Melody (ms +|+ FromRoot r (Dot Quarter)) (Dot Quarter)
+    -- | Add a dotted half note.
+    (:>.)   :: (MelConstraints ms (FromRoot r (Dot Half)), IntRep r, Primitive d)
+           => Melody ms d -> RootS r -> Melody (ms +|+ FromRoot r (Dot Half)) (Dot Half)
+    -- | Add a dotted whole note.
+    (:>>.)  :: (MelConstraints ms (FromRoot r (Dot Whole)), IntRep r, Primitive d)
+           => Melody ms d -> RootS r -> Melody (ms +|+ FromRoot r (Dot Whole)) (Dot Whole)
+    -- | Add a rest with the same duration as the previous one.
+    (:~|)   :: (MelConstraints ms (FromSilence d), Primitive d)
+           => Melody ms d -> RestS -> Melody (ms +|+ FromSilence d) d
+    -- | Add a thirty-second rest.
+    (:~<<<) :: (MelConstraints ms (FromSilence ThirtySecond), Primitive d)
+           => Melody ms d -> RestS -> Melody (ms +|+ FromSilence ThirtySecond) ThirtySecond
+    -- | Add a sixteenth rest.
+    (:~<<)  :: (MelConstraints ms (FromSilence Sixteenth), Primitive d)
+           => Melody ms d -> RestS -> Melody (ms +|+ FromSilence Sixteenth) Sixteenth
+    -- | Add an eighth rest.
+    (:~<)   :: (MelConstraints ms (FromSilence Eighth), Primitive d)
+           => Melody ms d -> RestS -> Melody (ms +|+ FromSilence Eighth) Eighth
+    -- | Add a quarter rest.
+    (:~^)   :: (MelConstraints ms (FromSilence Quarter), Primitive d)
+           => Melody ms d -> RestS -> Melody (ms +|+ FromSilence Quarter) Quarter
+    -- | Add a half rest.
+    (:~>)   :: (MelConstraints ms (FromSilence Half), Primitive d)
+           => Melody ms d -> RestS -> Melody (ms +|+ FromSilence Half) Half
+    -- | Add a whole rest.
+    (:~>>)  :: (MelConstraints ms (FromSilence Whole), Primitive d)
+           => Melody ms d -> RestS -> Melody (ms +|+ FromSilence Whole) Whole
+    -- | Add a dotted sixteenth rest.
+    (:~<<.) :: (MelConstraints ms (FromSilence (Dot Sixteenth)), Primitive d)
+           => Melody ms d -> RestS -> Melody (ms +|+ FromSilence (Dot Sixteenth)) (Dot Sixteenth)
+    -- | Add a dotted eighth rest.
+    (:~<.)  :: (MelConstraints ms (FromSilence (Dot Eighth)), Primitive d)
+           => Melody ms d -> RestS -> Melody (ms +|+ FromSilence (Dot Eighth)) (Dot Eighth)
+    -- | Add a dotted quarter rest.
+    (:~^.)  :: (MelConstraints ms (FromSilence (Dot Quarter)), Primitive d)
+           => Melody ms d -> RestS -> Melody (ms +|+ FromSilence (Dot Quarter)) (Dot Quarter)
+    -- | Add a dotted half rest.
+    (:~>.)  :: (MelConstraints ms (FromSilence (Dot Half)), Primitive d)
+           => Melody ms d -> RestS -> Melody (ms +|+ FromSilence (Dot Half)) (Dot Half)
+    -- | Add a dotted whole rest.
+    (:~>>.) :: (MelConstraints ms (FromSilence (Dot Whole)), Primitive d)
+           => Melody ms d -> RestS -> Melody (ms +|+ FromSilence (Dot Whole)) (Dot Whole)
+
+-- raiseByOct :: Melody m d -> Melody (RaiseAllByOct m) d
diff --git a/src/Mezzo/Model.hs b/src/Mezzo/Model.hs
new file mode 100644
--- /dev/null
+++ b/src/Mezzo/Model.hs
@@ -0,0 +1,55 @@
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Mezzo.Model
+-- Description :  Mezzo music model
+-- Copyright   :  (c) Dima Szamozvancev
+-- License     :  MIT
+--
+-- Maintainer  :  ds709@cam.ac.uk
+-- Stability   :  experimental
+-- Portability :  portable
+--
+-- Module providing the external interface to the Mezzo type-level music model.
+--
+-----------------------------------------------------------------------------
+
+module Mezzo.Model (module X) where
+
+-- Uses import/export shortcut as suggested by HLint.
+
+import Mezzo.Model.Types as X
+    (
+      PitchClass (..)
+    , Accidental (..)
+    , OctaveNum (..)
+    , Duration (..)
+    , PC (..)
+    , Acc (..)
+    , Oct (..)
+    , Dur (..)
+    , PitchType (..)
+    , Pit (..)
+    , Mode (..)
+    , ScaleDegree (..)
+    , KeyType (..)
+    , RootType (..)
+    , Mod (..)
+    , ScaDeg (..)
+    , KeyS (..)
+    , Root (..)
+    , RootToPitch
+    , PitchToNat
+    , Sharpen
+    , Flatten
+    , Dot
+    , FromRoot
+    , FromSilence
+    , Voice
+    , Partiture
+    , RaiseAllByOct
+    )
+import Mezzo.Model.Harmony.Chords as X
+import Mezzo.Model.Harmony.Functional as X
+import Mezzo.Model.Music as X
+import Mezzo.Model.Reify as X
diff --git a/src/Mezzo/Model/Harmony/Chords.hs b/src/Mezzo/Model/Harmony/Chords.hs
new file mode 100644
--- /dev/null
+++ b/src/Mezzo/Model/Harmony/Chords.hs
@@ -0,0 +1,242 @@
+{-# LANGUAGE  TypeInType, UndecidableInstances, GADTs, TypeOperators,
+    TypeApplications, TypeFamilies, ScopedTypeVariables, FlexibleInstances #-}
+{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Mezzo.Model.Harmony.Chords
+-- Description :  Models of chords
+-- Copyright   :  (c) Dima Szamozvancev
+-- License     :  MIT
+--
+-- Maintainer  :  ds709@cam.ac.uk
+-- Stability   :  experimental
+-- Portability :  portable
+--
+-- Types and type functions modelling harmonic chords.
+--
+-----------------------------------------------------------------------------
+
+module Mezzo.Model.Harmony.Chords
+    (
+    -- * Chords
+      TriadType (..)
+    , SeventhType (..)
+    , Inversion (..)
+    , TriType (..)
+    , SevType (..)
+    , Inv (..)
+    , InvertChord
+    , ChordType (..)
+    , Cho (..)
+    , FromChord
+    , ChordsToPartiture
+    ) where
+
+import GHC.TypeLits
+import Data.Kind (Type)
+
+import Mezzo.Model.Types
+import Mezzo.Model.Prim
+import Mezzo.Model.Reify
+
+-------------------------------------------------------------------------------
+-- Chords
+-------------------------------------------------------------------------------
+
+-- | The type of a triad.
+data TriadType = MajTriad | MinTriad | AugTriad | DimTriad
+
+-- | The type of a seventh chord.
+data SeventhType = MajSeventh | MajMinSeventh | MinSeventh | HalfDimSeventh | DimSeventh | Doubled TriadType
+
+-- | The inversion of a chord.
+data Inversion = Inv0 | Inv1 | Inv2 | Inv3
+
+-- | The singleton type for 'TriadType'.
+data TriType (t :: TriadType) = TriType
+
+-- | The singleton type for 'SeventhType'.
+data SevType (t :: SeventhType) = SevType
+
+-- | The singleton type for 'Inversion'.
+data Inv (t :: Inversion) = Inv
+
+-- | A chord type, indexed by the number of notes.
+data ChordType :: Nat -> Type where
+    Triad :: RootType -> TriadType   -> Inversion -> ChordType 3
+    SeventhChord :: RootType -> SeventhType -> Inversion -> ChordType 4
+
+data Cho (c :: ChordType n) = Cho
+
+-- | Convert a triad type to a list of intervals between the individual pitches.
+type family TriadTypeToIntervals (t :: TriadType) :: Vector IntervalType 3 where
+    TriadTypeToIntervals MajTriad =
+                Interval Perf Unison :-- Interval Maj Third :-- Interval Perf Fifth :-- None
+    TriadTypeToIntervals MinTriad =
+                Interval Perf Unison :-- Interval Min Third :-- Interval Perf Fifth :-- None
+    TriadTypeToIntervals AugTriad =
+                Interval Perf Unison :-- Interval Maj Third :-- Interval Aug Fifth  :-- None
+    TriadTypeToIntervals DimTriad =
+                Interval Perf Unison :-- Interval Min Third :-- Interval Dim Fifth  :-- None
+
+-- | Convert a seventh chord type to a list of intervals between the individual pitches.
+type family SeventhTypeToIntervals (s :: SeventhType) :: Vector IntervalType 4 where
+    SeventhTypeToIntervals MajSeventh     = TriadTypeToIntervals MajTriad :-| Interval Maj Seventh
+    SeventhTypeToIntervals MajMinSeventh  = TriadTypeToIntervals MajTriad :-| Interval Min Seventh
+    SeventhTypeToIntervals MinSeventh     = TriadTypeToIntervals MinTriad :-| Interval Min Seventh
+    SeventhTypeToIntervals HalfDimSeventh = TriadTypeToIntervals DimTriad :-| Interval Min Seventh
+    SeventhTypeToIntervals DimSeventh     = TriadTypeToIntervals DimTriad :-| Interval Dim Seventh
+    SeventhTypeToIntervals (Doubled tt)   = TriadTypeToIntervals tt       :-| Interval Perf Octave
+
+-- | Apply an inversion to a list of pitches.
+type family Invert (i :: Inversion) (n :: Nat) (ps :: Vector PitchType n) :: Vector PitchType n where
+    Invert Inv0 n ps         = ps
+    -- Need awkward workarounds because of #12564.
+    Invert Inv1 n (p :-- ps) = ps :-| RaiseByOct p
+    Invert Inv2 n (p :-- ps) = Invert Inv1 (n - 1) (p :-- Tail' ps) :-| RaiseByOct (Head' ps)
+    Invert Inv3 n (p :-- ps) = Invert Inv2 (n - 1) (p :-- (Head' (Tail' ps)) :-- (Tail' (Tail' (ps)))) :-| RaiseByOct (Head' ps)
+
+-- | Invert a doubled triad chord.
+type family InvertDoubled (i :: Inversion) (ps :: Vector PitchType 4) :: Vector PitchType 4 where
+    InvertDoubled Inv0 ps = ps
+    InvertDoubled Inv1 ps = Invert Inv1 3 (Init' ps) :-| (RaiseByOct (Head' (Tail' ps)))
+    InvertDoubled Inv2 ps = Invert Inv2 3 (Init' ps) :-| (RaiseByOct (Head' (Tail' (Tail' ps))))
+    InvertDoubled Inv3 ps = RaiseAllBy' ps (Interval Perf Octave)
+
+type family InvSucc (i :: Inversion) :: Inversion where
+    InvSucc Inv0 = Inv1
+    InvSucc Inv1 = Inv2
+    InvSucc Inv2 = Inv3
+    InvSucc Inv3 = Inv0
+
+type family InvertChord (c :: ChordType n) :: ChordType n where
+    InvertChord (Triad r t Inv2) = Triad r t Inv0
+    InvertChord (Triad r t i) = Triad r t (InvSucc i)
+    InvertChord (SeventhChord r t i) = SeventhChord r t (InvSucc i)
+
+-- | Build a list of pitches with the given intervals starting from a root.
+type family BuildOnRoot (r :: RootType) (is :: Vector IntervalType n) :: Vector PitchType n where
+    BuildOnRoot (PitchRoot Silence) _    = TypeError (Text "Can't build a chord on a rest.")
+    BuildOnRoot r None       = None
+    BuildOnRoot r (i :-- is) = RaiseBy (RootToPitch r) i :-- BuildOnRoot r is
+
+-- | Convert a chord to a list of constituent pitches.
+type family ChordToPitchList (c :: ChordType n) :: Vector PitchType n  where
+    ChordToPitchList (Triad        r t i) = Invert i 3 (BuildOnRoot r (TriadTypeToIntervals t))
+    ChordToPitchList (SeventhChord r (Doubled tt) i)
+                                          = InvertDoubled i (BuildOnRoot r (SeventhTypeToIntervals (Doubled tt)))
+    ChordToPitchList (SeventhChord r t i) = Invert i 4 (BuildOnRoot r (SeventhTypeToIntervals t))
+
+-- | Convert a chord to a partiture with the given length (one voice for each pitch).
+type family FromChord (c :: ChordType n) (l :: Nat) :: Partiture n l where
+    FromChord c l = VectorToColMatrix (ChordToPitchList c) l
+
+type family ChordsToPartiture (v :: Vector (ChordType n) l) (d :: Nat) :: Partiture n (l * d) where
+    ChordsToPartiture None l = None
+    ChordsToPartiture (c :-- cs) d = FromChord c d +|+ ChordsToPartiture cs d
+
+-------------------------------------------------------------------------------
+-- Primitive instances
+-------------------------------------------------------------------------------
+
+-- Chord types
+instance Primitive MajTriad where
+    type Rep MajTriad = Int -> [Int]
+    prim t = \r -> [r, r + 4, r + 7]
+    pretty t = "Maj"
+
+instance Primitive MinTriad where
+    type Rep MinTriad = Int -> [Int]
+    prim t = \r -> [r, r + 3, r + 7]
+    pretty t = "min"
+
+instance Primitive AugTriad where
+    type Rep AugTriad = Int -> [Int]
+    prim t = \r -> [r, r + 4, r + 8]
+    pretty t = "aug"
+
+instance Primitive DimTriad where
+    type Rep DimTriad = Int -> [Int]
+    prim t = \r -> [r, r + 3, r + 6]
+    pretty t = "dim"
+
+instance Primitive MajSeventh where
+    type Rep MajSeventh = Int -> [Int]
+    prim t = \r -> [r, r + 4, r + 7, r + 11]
+    pretty t = "Maj7"
+
+instance Primitive MajMinSeventh where
+    type Rep MajMinSeventh = Int -> [Int]
+    prim t = \r -> [r, r + 4, r + 7, r + 10]
+    pretty t = "7"
+
+instance Primitive MinSeventh where
+    type Rep MinSeventh = Int -> [Int]
+    prim t = \r -> [r, r + 3, r + 7, r + 10]
+    pretty t = "min7"
+
+instance Primitive HalfDimSeventh where
+    type Rep HalfDimSeventh = Int -> [Int]
+    prim t = \r -> [r, r + 3, r + 6, r + 10]
+    pretty t = "hdim7"
+
+instance Primitive DimSeventh where
+    type Rep DimSeventh = Int -> [Int]
+    prim t = \r -> [r, r + 3, r + 6, r + 9]
+    pretty t = "dim7"
+
+instance FunRep Int [Int] c => Primitive (Doubled c) where
+    type Rep (Doubled c) = Int -> [Int]
+    prim t = \r -> prim (TriType @c) r ++ [r + 12]
+    pretty t = pretty (TriType @c) ++ "D"
+
+-- Inversions
+-- Places the first element of the list on its end.
+invChord :: [Int] -> [Int]
+invChord [] = []
+invChord (x : xs) = xs ++ [x + 12]
+
+instance Primitive Inv0 where
+    type Rep Inv0 = [Int] -> [Int]
+    prim i = id
+    pretty i = "I0"
+
+instance Primitive Inv1 where
+    type Rep Inv1 = [Int] -> [Int]
+    prim i = invChord
+    pretty i = "I1"
+
+instance Primitive Inv2 where
+    type Rep Inv2 = [Int] -> [Int]
+    prim i = invChord . invChord
+    pretty i = "I2"
+
+instance Primitive Inv3 where
+    type Rep Inv3 = [Int] -> [Int]
+    prim i = invChord . invChord . invChord
+    pretty i = "I3"
+
+instance (IntRep r, FunRep Int [Int] t, FunRep [Int] [Int] i)
+        => Primitive (Triad r t i) where
+    type Rep (Triad r t i) = [Int]
+    prim c = prim (Inv @i) . prim (TriType @t) $ prim (Root @r)
+    pretty c = pc ++ " " ++ pretty (TriType @t) ++ " " ++ pretty (Inv @i)
+        where pc = takeWhile (\c -> c /= ' ' && c /= '\'' && c /= '_') $ pretty (Root @r)
+
+instance (IntRep r, FunRep Int [Int] tt, FunRep [Int] [Int] i)
+        => Primitive (SeventhChord r (Doubled tt) i) where
+    type Rep (SeventhChord r (Doubled tt) i) = [Int]
+    prim c = inverted ++ [head inverted + 12]
+        where rootPos = prim (TriType @tt) $ prim (Root @r)
+              inverted = prim (Inv @i) rootPos
+    pretty c = pc ++ " " ++ pretty (TriType @tt) ++ "D " ++ pretty (Inv @i)
+        where pc = takeWhile (\c -> c /= ' ' && c /= '\'' && c /= '_') $ pretty (Root @r)
+
+
+instance {-# OVERLAPPABLE #-} (IntRep r, FunRep Int [Int] t, FunRep [Int] [Int] i)
+        => Primitive (SeventhChord r t i) where
+    type Rep (SeventhChord r t i) = [Int]
+    prim c = prim (Inv @i) . prim (SevType @t) $ prim (Root @r)
+    pretty c = pc ++ " " ++ pretty (SevType @t) ++ " " ++ pretty (Inv @i)
+        where pc = takeWhile (\c -> c /= ' ' && c /= '\'' && c /= '_') $ pretty (Root @r)
diff --git a/src/Mezzo/Model/Harmony/Functional.hs b/src/Mezzo/Model/Harmony/Functional.hs
new file mode 100644
--- /dev/null
+++ b/src/Mezzo/Model/Harmony/Functional.hs
@@ -0,0 +1,217 @@
+{-# LANGUAGE  TypeInType, MultiParamTypeClasses, FlexibleInstances,
+    UndecidableInstances, GADTs, TypeOperators, TypeFamilies, FlexibleContexts #-}
+{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Mezzo.Model.Harmony.Functional
+-- Description :  Models of functional harmony
+-- Copyright   :  (c) Dima Szamozvancev
+-- License     :  MIT
+--
+-- Maintainer  :  ds709@cam.ac.uk
+-- Stability   :  experimental
+-- Portability :  portable
+--
+-- Types and type functions modelling principles of functional harmony.
+--
+-----------------------------------------------------------------------------
+
+module Mezzo.Model.Harmony.Functional
+    (
+      Quality (..)
+    , Degree (..)
+    , Piece (..)
+    , Phrase (..)
+    , Cadence (..)
+    , Tonic (..)
+    , Dominant (..)
+    , Subdominant (..)
+    , PieceToChords
+    )
+    where
+
+import GHC.TypeLits
+import Data.Kind
+
+import Mezzo.Model.Types hiding (IntervalClass (..))
+import Mezzo.Model.Prim
+import Mezzo.Model.Harmony.Chords
+
+-- | The quality of a scale degree chord.
+data Quality = MajQ | MinQ | DomQ | DimQ
+
+-- | A scale degree chord in given key, on the given scale, with the given quality.
+data Degree (d :: ScaleDegree) (q :: Quality) (k :: KeyType) (i :: Inversion) where
+    DegChord :: Degree d q k i
+
+-- | Ensure that the degree and quality match the mode.
+class DiatonicDegree (d :: ScaleDegree) (q :: Quality) (k :: KeyType)
+instance MajDegQuality d q => DiatonicDegree d q (Key pc acc MajorMode)
+instance MinDegQuality d q => DiatonicDegree d q (Key pc acc MinorMode)
+
+-- | Ensure that the degree and quality are valid in major mode.
+class MajDegQuality (d :: ScaleDegree) (q :: Quality)
+instance {-# OVERLAPPING #-} MajDegQuality I MajQ
+instance {-# OVERLAPPING #-} MajDegQuality II MinQ
+instance {-# OVERLAPPING #-} MajDegQuality II DomQ  -- Secondary dominant
+instance {-# OVERLAPPING #-} MajDegQuality III MinQ
+instance {-# OVERLAPPING #-} MajDegQuality IV MajQ
+instance {-# OVERLAPPING #-} MajDegQuality V MajQ
+instance {-# OVERLAPPING #-} MajDegQuality V DomQ
+instance {-# OVERLAPPING #-} MajDegQuality VI MinQ
+instance {-# OVERLAPPING #-} MajDegQuality VII DimQ
+instance {-# OVERLAPPABLE #-} TypeError (Text "Can't have a "
+                                    :<>: ShowQual q
+                                    :<>: ShowDeg d
+                                    :<>: Text " degree chord in major mode.")
+                                => MajDegQuality d q
+
+-- | Ensure that the degree and quality are valid in minor mode.
+class MinDegQuality (d :: ScaleDegree) (q :: Quality)
+instance {-# OVERLAPPING #-} MinDegQuality I MinQ
+instance {-# OVERLAPPING #-} MinDegQuality II DimQ
+instance {-# OVERLAPPING #-} MinDegQuality II DomQ  -- Secondary dominant
+instance {-# OVERLAPPING #-} MinDegQuality III MajQ
+instance {-# OVERLAPPING #-} MinDegQuality IV MinQ
+instance {-# OVERLAPPING #-} MinDegQuality V MajQ
+instance {-# OVERLAPPING #-} MinDegQuality V DomQ
+instance {-# OVERLAPPING #-} MinDegQuality VI MajQ
+instance {-# OVERLAPPING #-} MinDegQuality VII MajQ
+instance {-# OVERLAPPABLE #-} TypeError (Text "Can't have a "
+                                    :<>: ShowType q :<>: Text " "
+                                    :<>: ShowType d
+                                    :<>: Text " degree chord in minor mode.")
+                                => MinDegQuality d q
+
+-- | A functionally described piece of music, built from multiple phrases.
+data Piece (k :: KeyType) (l :: Nat) where
+    Cad :: Cadence k l -> Piece k l
+    (:=) :: Phrase k l -> Piece k (n - l) -> Piece k n
+
+-- | A phrase matching a specific functional progression.
+data Phrase (k :: KeyType) (l :: Nat) where
+    -- | A tonic-dominant-tonic progression.
+    PhraseIVI :: Tonic k (l2 - l1) -> Dominant k l1 -> Tonic k (l - l2) -> Phrase k l
+    -- | A dominant-tonic progression.
+    PhraseVI  :: Dominant k l1 -> Tonic k (l - l1) -> Phrase k l
+
+-- | A cadence in a specific key with a specific length.
+data Cadence (k :: KeyType) (l :: Nat) where
+    -- | Authentic cadence with major fifth chord.
+    AuthCad    :: Degree V MajQ k Inv1 -> Degree I q k Inv0 -> Cadence k 2
+    -- | Authentic cadence with dominant seventh fifth chord.
+    AuthCad7   :: Degree V DomQ k Inv2 -> Degree I q k Inv0 -> Cadence k 2
+    -- | Authentic cadence with diminished seventh chord.
+    AuthCadVii :: Degree VII DimQ k Inv0 -> Degree I q k Inv0 -> Cadence k 2
+    -- | Authentic cadence with a cadential 6-4 chord
+    AuthCad64  :: Degree I MajQ k Inv2 -> Degree V DomQ k Inv3 -> Degree I MajQ k Inv1 -> Cadence k 3
+    -- | Half cadence ending with a major fifth chord.
+    HalfCad    :: Degree d q k i -> Degree V MajQ k Inv0 -> Cadence k 2
+    -- | Deceptive cadence from a dominant fifth to a sixth.
+    DeceptCad  :: Degree V DomQ k Inv0 -> Degree VI q k Inv2 -> Cadence k 2
+
+-- | A tonic chord.
+data Tonic (k :: KeyType) (l :: Nat) where
+    -- | A major tonic chord.
+    TonMaj :: Degree I MajQ k Inv0 -> Tonic k 1 -- Temporarily (?) allow only no inversion
+    -- | A minor tonic chord.
+    TonMin :: Degree I MinQ k Inv0 -> Tonic k 1
+
+class NotInv2 (i :: Inversion)
+instance NotInv2 Inv0
+instance TypeError (Text "Can't have a tonic in second inversion.") => NotInv2 Inv2
+instance NotInv2 Inv1
+instance NotInv2 Inv3
+
+-- | A dominant chord progression.
+data Dominant (k :: KeyType) (l :: Nat) where
+    -- | Major fifth dominant.
+    DomVM   :: Degree V MajQ k i -> Dominant k 1
+    -- | Seventh chord fifth degree dominant.
+    DomV7   :: Degree V DomQ k i -> Dominant k 1
+    -- | Diminished seventh degree dominant.
+    DomVii0 :: Degree VII DimQ k i -> Dominant k 1
+    -- | Subdominant followed by dominant.
+    DomSD   :: Subdominant k l1 -> Dominant k (l - l1) -> Dominant k l
+    -- | Secondary dominant followed by dominant.
+    DomSecD :: Degree II DomQ k Inv0 -> Degree V DomQ k Inv2 -> Dominant k 2
+
+-- | A subdominant chord progression.
+data Subdominant (k :: KeyType) (l :: Nat) where
+    -- | Minor second subdominant.
+    SubIIm     :: Degree II MinQ k i -> Subdominant k 1
+    -- | Major fourth subdominant.
+    SubIVM     :: Degree IV MajQ k i -> Subdominant k 1
+    -- | Minor third followed by major fourth subdominant
+    SubIIImIVM :: Degree III MinQ k i1 -> Degree IV MajQ k i2 -> Subdominant k 2
+    -- | Minor fourth dominant.
+    SubIVm     :: Degree IV MinQ k i -> Subdominant k 1
+
+-- | Convert a scale degree to a chord.
+type family DegToChord (d :: Degree d q k i) :: ChordType 4 where
+    DegToChord (DegChord :: Degree d q k i) = SeventhChord (DegreeRoot k d) (QualToType q) i
+
+-- | Convert a quality to a seventh chord type.
+type family QualToType (q :: Quality) :: SeventhType where
+    QualToType MajQ = Doubled MajTriad
+    QualToType MinQ = Doubled MinTriad
+    QualToType DomQ = MajMinSeventh
+    QualToType DimQ = DimSeventh
+
+-- | Convert a cadence to chords.
+type family CadToChords (c :: Cadence k l) :: Vector (ChordType 4) l where
+    CadToChords (AuthCad  d1 d2) = DegToChord d1 :-- DegToChord d2 :-- None
+    CadToChords (AuthCad7 d1 d2) = DegToChord d1 :-- DegToChord d2 :-- None
+    CadToChords (AuthCadVii d1 d2) = DegToChord d1 :-- DegToChord d2 :-- None
+    CadToChords (AuthCad64 d1 d2 d3) = DegToChord d1 :-- DegToChord d2 :-- DegToChord d3 :-- None
+    CadToChords (HalfCad d1 d2) = DegToChord d1 :-- DegToChord d2 :-- None
+    CadToChords (DeceptCad d1 d2) = DegToChord d1 :-- DegToChord d2 :-- None
+
+-- | Convert a tonic to chords.
+type family TonToChords (t :: Tonic k l) :: Vector (ChordType 4) l where
+    TonToChords (TonMaj d) = DegToChord d :-- None
+    TonToChords (TonMin d) = DegToChord d :-- None
+
+-- | Convert a dominant to chords.
+type family DomToChords (l :: Nat) (t :: Dominant k l) :: Vector (ChordType 4) l where
+    DomToChords 1 (DomVM d) = DegToChord d :-- None
+    DomToChords 1 (DomV7 d) = DegToChord d :-- None
+    DomToChords 1 (DomVii0 d) = DegToChord d :-- None
+    DomToChords l (DomSD (s :: Subdominant k l1) d) =
+                    SubdomToChords s ++. DomToChords (l - l1) d
+    DomToChords 2 (DomSecD d1 d2) = DegToChord d1 :-- DegToChord d2 :-- None
+
+-- | Convert a subdominant to chords.
+type family SubdomToChords (t :: Subdominant k l) :: Vector (ChordType 4) l where
+    SubdomToChords (SubIIm d) = DegToChord d :-- None
+    SubdomToChords (SubIVM d) = DegToChord d :-- None
+    SubdomToChords (SubIIImIVM d1 d2) = DegToChord d1 :-- DegToChord d2 :-- None
+    SubdomToChords (SubIVm d) = DegToChord d :-- None
+
+-- | Convert a phrase to chords.
+type family PhraseToChords (l :: Nat) (p :: Phrase k l) :: Vector (ChordType 4) l where
+    PhraseToChords l (PhraseIVI t1 (d :: Dominant k dl) t2) = TonToChords t1 ++. DomToChords dl d ++. TonToChords t2
+    PhraseToChords l (PhraseVI (d :: Dominant k dl) t) = DomToChords dl d ++. TonToChords t
+
+-- | Convert a piece to chords.
+type family PieceToChords (l :: Nat) (p :: Piece k l) :: Vector (ChordType 4) l where
+    PieceToChords l (Cad (c :: Cadence k l)) = CadToChords c
+    PieceToChords l ((p :: Phrase k l1) := ps) = PhraseToChords l1 p ++. PieceToChords (l - l1) ps
+
+-- | Convert a quality to text.
+type family ShowQual (q :: Quality) :: ErrorMessage where
+    ShowQual MajQ = Text "major "
+    ShowQual MinQ = Text "minor "
+    ShowQual DomQ = Text "dominant "
+    ShowQual DimQ = Text "diminished "
+
+-- | Convert a degree to text.
+type family ShowDeg (d :: ScaleDegree) :: ErrorMessage where
+    ShowDeg I = Text "1st"
+    ShowDeg II = Text "2nd"
+    ShowDeg III = Text "3rd"
+    ShowDeg IV = Text "4th"
+    ShowDeg V = Text "5th"
+    ShowDeg VI = Text "6th"
+    ShowDeg VII = Text "7th"
diff --git a/src/Mezzo/Model/Harmony/Motion.hs b/src/Mezzo/Model/Harmony/Motion.hs
new file mode 100644
--- /dev/null
+++ b/src/Mezzo/Model/Harmony/Motion.hs
@@ -0,0 +1,92 @@
+{-# LANGUAGE  TypeInType, MultiParamTypeClasses, FlexibleInstances,
+    UndecidableInstances #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Mezzo.Model.Harmony.Motion
+-- Description :  Models of harmonic motion
+-- Copyright   :  (c) Dima Szamozvancev
+-- License     :  MIT
+--
+-- Maintainer  :  ds709@cam.ac.uk
+-- Stability   :  experimental
+-- Portability :  portable
+--
+-- Classes modelling consonance, dissonance and harmonic motion.
+--
+-----------------------------------------------------------------------------
+
+module Mezzo.Model.Harmony.Motion
+    (
+    -- * Consonant and dissonant intervals
+      PerfConsonantInterval
+    , ImperfConsonantInterval
+    , DissonantInterval
+    -- * Harmonic motion
+    , DirectMotion
+    , ContraryMotion
+    , ObliqueMotion
+    ) where
+
+import GHC.TypeLits
+
+import Mezzo.Model.Types
+import Mezzo.Model.Prim
+
+-------------------------------------------------------------------------------
+-- Consonant and dissonant intervals
+-------------------------------------------------------------------------------
+
+-- | Classifies perfect consonant intervals:
+--
+--  * Perfect unisons
+--  * Perfect fifths
+--  * Perfect octaves
+class PerfConsonantInterval (i :: IntervalType)
+instance PerfConsonantInterval (Interval Perf Unison)
+instance PerfConsonantInterval (Interval Perf Fifth)
+instance PerfConsonantInterval (Interval Perf Octave)
+
+-- | Classifies imperfect consonant intervals:
+--
+--  * Major and minor thirds
+--  * Major and minor sixths
+class ImperfConsonantInterval (i :: IntervalType)
+instance ImperfConsonantInterval (Interval Maj Third)
+instance ImperfConsonantInterval (Interval Min Third)
+instance ImperfConsonantInterval (Interval Maj Sixth)
+instance ImperfConsonantInterval (Interval Min Sixth)
+
+-- | Classifies dissonant intervals:
+--
+--  * Perfect fourth (by common practice convention)
+--  * Augmented and diminished intervals
+--  * Second and seventh intervals
+class DissonantInterval (i :: IntervalType)
+instance DissonantInterval (Interval Perf Fourth)
+instance DissonantInterval (Interval Aug is)
+instance DissonantInterval (Interval Dim is)
+instance DissonantInterval (Interval ic Second)
+instance DissonantInterval (Interval ic Seventh)
+
+-------------------------------------------------------------------------------
+-- Harmonic motion
+-------------------------------------------------------------------------------
+
+-- | Ensures that direct motion is permitted between the two intervals.
+class DirectMotion (i1 :: IntervalType) (i2 :: IntervalType)
+instance {-# OVERLAPPING #-} TypeError (Text "Direct motion into a perfect unison is forbidden.")
+                                => DirectMotion i1 (Interval Perf Unison)
+instance {-# OVERLAPPING #-} TypeError (Text "Direct motion into a perfect fifth is forbidden.")
+                                => DirectMotion i1 (Interval Perf Fifth)
+instance {-# OVERLAPPING #-} TypeError (Text "Direct motion into a perfect octave is forbidden.")
+                                => DirectMotion i1 (Interval Perf Octave)
+instance {-# OVERLAPPABLE #-}      DirectMotion i1 i2
+
+-- | Ensures that contrary motion is permitted between the two intervals.
+class ContraryMotion (i1 :: IntervalType) (i2 :: IntervalType)
+instance ContraryMotion i1 i2
+
+-- | Ensures that oblique motion is permitted between the two intervals.
+class ObliqueMotion (i1 :: IntervalType) (i2 :: IntervalType)
+instance ObliqueMotion i1 i2
diff --git a/src/Mezzo/Model/Music.hs b/src/Mezzo/Model/Music.hs
new file mode 100644
--- /dev/null
+++ b/src/Mezzo/Model/Music.hs
@@ -0,0 +1,303 @@
+{-# LANGUAGE TypeInType, RankNTypes, TypeOperators, GADTs, ConstraintKinds,
+    FlexibleContexts, MultiParamTypeClasses, TypeFamilies, UndecidableInstances,
+    FlexibleInstances #-}
+{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Mezzo.Model.Music
+-- Description :  Mezzo music algebra
+-- Copyright   :  (c) Dima Szamozvancev
+-- License     :  MIT
+--
+-- Maintainer  :  ds709@cam.ac.uk
+-- Stability   :  experimental
+-- Portability :  portable
+--
+-- Algebraic description of music with type-level constraints.
+--
+-----------------------------------------------------------------------------
+
+module Mezzo.Model.Music
+    (
+    -- * Music
+      Music (..)
+    , Score (..)
+    -- * Harmonic constructs
+    , Progression
+    -- * Constraints
+    , MelConstraints
+    , HarmConstraints
+    , ChordConstraints
+    ) where
+
+import Data.Kind
+import GHC.TypeLits
+import Text.PrettyPrint.Boxes
+
+import Mezzo.Model.Prim
+import Mezzo.Model.Harmony.Motion
+import Mezzo.Model.Harmony.Chords
+import Mezzo.Model.Harmony.Functional
+import Mezzo.Model.Types
+import Mezzo.Model.Reify
+
+infixl 4 :|:
+infixl 4 :-:
+
+-------------------------------------------------------------------------------
+-- The 'Music' datatype
+-------------------------------------------------------------------------------
+
+-- | A piece of music consisting of parallel and sequential composition of notes
+-- and rests, subject to constraints.
+--
+-- Currently enforced constraints are:
+--
+--  * Height (number of voices) of two sequentially composed pieces must be equal.
+--  * Width (number of temporal units) of two parallelly composed pieces must be equal.
+--  * Sequentially composed voices cannot have any augmented, diminished or seventh leaps.
+--  * Parallelly composed pieces cannot have any minor second or major seventh harmonic intervals.
+--  * Music must not contain parallel or concealed unisons, fifths or octaves.
+--
+data Music :: forall n l. Partiture n l -> Type where
+    -- | A note specified by a pitch and a duration.
+    Note :: NoteConstraints r d => Root r -> Dur d -> Music (FromRoot r d)
+    -- | A rest specified by a duration.
+    Rest :: RestConstraints d => Dur d -> Music (FromSilence d)
+    -- | Sequential or melodic composition of music.
+    (:|:) :: MelConstraints m1 m2  => Music m1 -> Music m2 -> Music (m1 +|+ m2)
+    -- | Parallel or harmonic composition of music.
+    (:-:) :: HarmConstraints m1 m2 => Music m1 -> Music m2 -> Music (m1 +-+ m2)
+    -- | A chord specified by a chord type and a duration.
+    Chord :: ChordConstraints c d => Cho c -> Dur d -> Music (FromChord c d)
+    -- Progression :: ProgressionConstraints p => Prog p -> Music (FromProg p)
+
+-- | A type encapsulating every 'Music' composition.
+data Score = forall m. Score (Music m)
+
+-------------------------------------------------------------------------------
+-- Harmonic constructs
+-- Types and type synonyms constructing 'Music' instances from harmonic types.
+-------------------------------------------------------------------------------
+
+-- | A chord progression with the given scheme and chord length.
+type Progression (p :: Piece k l) (d :: Nat) = Music (ChordsToPartiture (PieceToChords l p) d)
+
+-------------------------------------------------------------------------------
+-- Musical constraints
+-- Specifications of the rules that valid musical terms have to follow.
+-------------------------------------------------------------------------------
+
+-- | Enable or disable music correctness checking.
+type Strict = True
+
+-- | Applies the constraint c if strict checking is enabled.
+type IfStrict c = If Strict c Valid
+
+-- | Ensures that the note is valid.
+type NoteConstraints r d = (IntRep r, Primitive d)
+
+-- | Ensures that the rest is valid.
+type RestConstraints d = (Primitive d)
+
+-- | Ensures that two pieces of music can be composed sequentially.
+type MelConstraints (m1 :: Partiture n l1) (m2 :: Partiture n l2) =
+        IfStrict (ValidMelConcat m1 m2)
+
+-- | Ensures that two pieces of music can be composed in parallel.
+type HarmConstraints m1 m2 = IfStrict (ValidHarmConcat (Align m1 m2))
+
+-- | Ensures that the chord is valid.
+type ChordConstraints (c :: ChordType n) d = (IntListRep c, Primitive n, Primitive d)
+
+-- | Ensures that a progression is valid.
+type ProgressionConstraints p = Valid
+
+---- Melodic constraints
+
+-- | Ensures that melodic intervals are valid.
+--
+-- A melodic interval is invalid if it is
+--
+--  * any augmented interval or
+--  * any diminished interval or
+--  * any seventh interval.
+class ValidMelInterval (i :: IntervalType)
+instance {-# OVERLAPPING #-}       ValidMelInterval (Interval Aug Unison)
+instance {-# OVERLAPS #-} TypeError (Text "Augmented melodic intervals are not permitted.")
+                                => ValidMelInterval (Interval Aug a)
+instance {-# OVERLAPS #-} TypeError (Text "Diminished melodic intervals are not permitted.")
+                                => ValidMelInterval (Interval Dim a)
+instance {-# OVERLAPPING #-} TypeError (Text "Seventh intervals are not permitted in melody.")
+                                => ValidMelInterval (Interval a Seventh)
+instance {-# OVERLAPPABLE #-}      ValidMelInterval i
+
+-- | Ensures that two pitches form valid melodic leaps.
+--
+-- Two pitches form valid melodic leaps if
+--
+--  * at least one of them is silent (i.e. it is a rest) or
+--  * they form a valid melodic interval.
+class ValidMelLeap (p1 :: PitchType) (p2 :: PitchType)
+instance {-# OVERLAPPING #-}  ValidMelLeap Silence Silence
+instance {-# OVERLAPPING #-}  ValidMelLeap Silence (Pitch pc acc oct)
+instance {-# OVERLAPPING #-}  ValidMelLeap (Pitch pc acc oct) Silence
+instance {-# OVERLAPPABLE #-} ValidMelInterval (MakeInterval a b) => ValidMelLeap a b
+
+-- | Ensures that two voices can be appended.
+--
+-- Two voices can be appended if
+--
+--  * at least one of them is empty or
+--  * the last pitch of the first vector forms a valid melodic leap
+--    with the first pitch of the second vector.
+class ValidMelAppend (a :: Voice l1) (b :: Voice l2)
+instance {-# OVERLAPPING #-}  ValidMelAppend End a
+instance {-# OVERLAPPING #-}  ValidMelAppend a End
+instance {-# OVERLAPPABLE #-} ValidMelLeap (Last vs1) (Head vs2) => ValidMelAppend vs1 vs2
+
+-- | Ensures that two partitures can be horizontally concatenated.
+--
+-- Two part lists can be horizontally concatenated if
+--
+--  * both of them are empty or
+--  * all of the voices can be appended.
+class ValidMelConcat (ps1 :: Partiture n l1) (ps2 :: Partiture n l2)
+instance {-# OVERLAPPING #-}       ValidMelConcat None None
+instance {-# OVERLAPPABLE #-} (ValidMelAppend v1 v2, ValidMelConcat vs1 vs2)
+                                => ValidMelConcat (v1 :-- vs1) (v2 :-- vs2)
+
+
+---- Harmonic constraints
+
+-- | Ensures that harmonic intervals are valid.
+--
+-- A harmonic interval is invalid if it is
+--
+--  * a minor second or
+--  * a major seventh or
+--  * an augmented octave.
+class ValidHarmInterval (i :: IntervalType)
+instance {-# OVERLAPPING #-} TypeError (Text "Can't have minor seconds in chords.")
+                                => ValidHarmInterval (Interval Aug Unison)
+instance {-# OVERLAPPING #-} TypeError (Text "Can't have minor seconds in chords.")
+                                => ValidHarmInterval (Interval Min Second)
+instance {-# OVERLAPPING #-} TypeError (Text "Can't have major sevenths in chords.")
+                                => ValidHarmInterval (Interval Maj Seventh)
+instance {-# OVERLAPPING #-} TypeError (Text "Can't have major sevenths in chords.")
+                                => ValidHarmInterval (Interval Dim Octave)
+instance {-# OVERLAPPING #-} TypeError (Text "Can't have augmented octaves in chords.")
+                                => ValidHarmInterval (Interval Aug Octave)
+instance {-# OVERLAPPABLE #-}      ValidHarmInterval i
+
+-- | Ensures that two pitches form valid harmonic dyad (interval).
+--
+-- Two pitches form valid harmonic dyads if
+--
+--  * at least one of them is silent (i.e. it is a rest) or
+--  * they form a valid harmonic interval.
+class ValidHarmDyad (p1 :: PitchType) (p2 :: PitchType)
+instance {-# OVERLAPPING #-}  ValidHarmDyad Silence Silence
+instance {-# OVERLAPPING #-}  ValidHarmDyad (Pitch pc acc oct) Silence
+instance {-# OVERLAPPING #-}  ValidHarmDyad Silence (Pitch pc acc oct)
+instance {-# OVERLAPPABLE #-} ValidHarmInterval (MakeInterval a b) => ValidHarmDyad a b
+
+-- | Ensures that two voices form pairwise valid harmonic dyads.
+class ValidHarmDyadsInVectors (v1 :: Voice l) (v2 :: Voice l)
+instance AllPairsSatisfy ValidHarmDyad v1 v2 => ValidHarmDyadsInVectors v1 v2
+
+-- | Ensures that two partitures can be vertically concatenated.
+--
+-- Two partitures can be vertically concatenated if
+--
+--  * the top one is empty or
+--  * all but the first voice can be concatenated, and the first voice
+--    forms valid harmonic dyads with every other voice and follows the rules
+--    of valid harmonic motion.
+class ValidHarmConcat (ps :: (Partiture n1 l, Partiture n2 l))
+instance {-# OVERLAPPING #-}       ValidHarmConcat '(None, vs)
+instance {-# OVERLAPPABLE #-} ( ValidHarmConcat '(vs, us)
+                              , AllSatisfyAll [ ValidHarmDyadsInVectors v
+                                              , ValidHarmMotionInVectors v] us)
+                                => ValidHarmConcat '((v :-- vs), us)
+
+
+---- Voice leading constraints
+
+-- | Ensures that four pitches (representing two consequent intervals) follow
+-- the rules for valid harmonic motion.
+--
+-- Harmonic motion is not permitted if
+--
+--  * it is direct motion into a perfect interval (this covers parallel and
+--    concealed fifths, octaves and unisons).
+type family ValidMotion (p1 :: PitchType) (p2 :: PitchType)
+                        (q1 :: PitchType) (q2 :: PitchType)
+                            :: Constraint where
+    ValidMotion Silence _ _ _ = Valid
+    ValidMotion _ Silence _ _ = Valid
+    ValidMotion _ _ Silence _ = Valid
+    ValidMotion _ _ _ Silence = Valid
+    ValidMotion p1 p2 q1 q2   =
+            If ((p1 .~. q1) .||. (p2 .~. q2))
+                (ObliqueMotion (MakeInterval p1 p2) (MakeInterval q1 q2))
+                (If (p1 <<? q1)
+                    (If (p2 <<? q2)
+                        (DirectMotion (MakeInterval p1 p2) (MakeInterval q1 q2))
+                        (ContraryMotion (MakeInterval p1 p2) (MakeInterval q1 q2)))
+                    (If (p2 <<? q2)
+                        (ContraryMotion (MakeInterval p1 p2) (MakeInterval q1 q2))
+                        (DirectMotion (MakeInterval p1 p2) (MakeInterval q1 q2))))
+
+-- | Ensures that the interval formed by the first pitch and the last element
+-- of the first voice can move to the interval formed by the second
+-- pitch and the first element of the second voice.
+class ValidMelPitchVectorMotion (p1 :: PitchType) (p2 :: PitchType) (v1 :: Voice l1) (v2 :: Voice l2)
+instance {-# OVERLAPPING #-}    ValidMelPitchVectorMotion p1 p2 End End
+instance {-# OVERLAPPABLE #-} ValidMotion p1 (Last v1) p2 (Head v2)
+                            =>  ValidMelPitchVectorMotion p1 p2 v1 v2
+-- Can't have v1 be End and v2 be not End, since if v1 under p1 is not nil, there
+-- must be an accompanying voice under p2
+
+-- | Ensures that two partitures follow the rules of motion when
+-- horizontally concatenated.
+--
+-- Two horizontally concatenated partitures follow the rules of harmonic motion if
+--
+--  * both are empty or
+--  * their lower voices can be concatenated and the joining elements of the
+--    top voice form intervals with the joining elements of the other voices
+--    which follow the rules of harmonic motion.
+class ValidMelMatrixMotion (ps1 :: Partiture n l1) (ps2 :: Partiture n l2)
+instance {-# OVERLAPPING #-}       ValidMelMatrixMotion None None
+instance {-# OVERLAPPABLE #-} ( ValidMelMatrixMotion vs1 vs2
+                              , AllPairsSatisfy' (ValidMelPitchVectorMotion (Last v1) (Head v2)) vs1 vs2)
+                                => ValidMelMatrixMotion (v1 :-- vs1) (v2 :-- vs2)
+
+-- | Ensures that two voices form pairwise intervals which follow the
+-- rules of harmonic motion.
+class ValidHarmMotionInVectors (v1 :: Voice l) (v2 :: Voice p)
+instance {-# OVERLAPPING #-}       ValidHarmMotionInVectors End End
+instance {-# OVERLAPPING #-} ValidHarmMotionInVectors (p :* d1 :- End) (q :* d2 :- End)
+instance {-# OVERLAPPABLE #-} ( ValidMotion p q (Head ps) (Head qs)
+                              , ValidHarmMotionInVectors ps qs)
+                                => ValidHarmMotionInVectors (p :* d1 :- ps) (q :* d2 :- qs)
+
+-------------------------------------------------------------------------------
+-- Pretty-printing
+-------------------------------------------------------------------------------
+
+instance Show (Music m) where show = render . ppMusic
+
+-- | Pretty-print a 'Music' value.
+ppMusic :: Music m -> Box
+ppMusic (Note r d) = char '|' <+> doc r <+> doc d
+ppMusic (Rest d) = char '|' <+> text "~~~~" <+> doc d
+ppMusic (m1 :|: m2) = ppMusic m1 <> emptyBox 1 1 <> ppMusic m2
+ppMusic (m1 :-: m2) = ppMusic m1 // ppMusic m2
+ppMusic (Chord c d) = char '|' <+> doc c <+> doc d
+
+-- | Convert a showable value into a pretty-printed box.
+doc :: Show a => a -> Box
+doc = text . show
diff --git a/src/Mezzo/Model/Prim.hs b/src/Mezzo/Model/Prim.hs
new file mode 100644
--- /dev/null
+++ b/src/Mezzo/Model/Prim.hs
@@ -0,0 +1,302 @@
+{-# LANGUAGE TypeInType, TypeOperators, TypeFamilies, GADTs,
+    UndecidableInstances, ConstraintKinds #-}
+{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Mezzo.Model.Prim
+-- Description :  Mezzo type primitives
+-- Copyright   :  (c) Dima Szamozvancev
+-- License     :  MIT
+--
+-- Maintainer  :  ds709@cam.ac.uk
+-- Stability   :  experimental
+-- Portability :  portable
+--
+-- Primitive types that make up the base for the Mezzo type model.
+--
+-----------------------------------------------------------------------------
+
+module Mezzo.Model.Prim
+    (
+    -- * Vectors and matrices
+      Vector (..)
+    , Times (..)
+    , Elem (..)
+    , type (**)
+    , OptVector (..)
+    , Head
+    , Head'
+    , Last
+    , Tail'
+    , Init'
+    , Length
+    , Length'
+    , Matrix
+    , type (++)
+    , type (++.)
+    , type (:-|)
+    , type (+*+)
+    , type (+|+)
+    , type (+-+)
+    , Align
+    , VectorToColMatrix
+    -- * Logic and arithmetic
+    , If
+    , Not
+    , type (.&&.)
+    , type (.||.)
+    , type (.~.)
+    , MaxN
+    , MinN
+    -- * Constraints
+    , Valid
+    , Invalid
+    , AllSatisfy
+    , AllPairsSatisfy
+    , AllPairsSatisfy'
+    , SatisfiesAll
+    , AllSatisfyAll
+    ) where
+
+import Data.Kind
+import GHC.TypeLits
+
+infixr 7 :*
+infixr 7 **
+infixr 6 :-
+infixr 5 :--
+infixl 4 ++
+infixl 4 +*+
+infixl 4 +|+
+infixl 4 +-+
+infixl 3 .&&.
+infixl 3 .||.
+infixl 5 .~.
+
+-------------------------------------------------------------------------------
+-- Type-level vectors and matrices
+-------------------------------------------------------------------------------
+
+-- | Simple length-indexed vector.
+data Vector :: Type -> Nat -> Type where
+    None :: Vector t 0
+    (:--) :: t -> Vector t (n - 1) -> Vector t n
+
+-- | Singleton type for the number of repetitions of an element.
+data Times (n :: Nat) where
+    T :: Times n
+
+-- | An element of a "run-length encoded" vector, containing the value and
+-- the number of repetitions
+data Elem :: Type -> Nat -> Type where
+    (:*) :: t -> Times n -> Elem t n
+
+-- | Replicate a value the specified number of times to create a new 'Elem'.
+type family (v :: t) ** (d :: Nat) :: Elem t d where
+    v ** d = v :* (T :: Times d)
+
+-- | A length-indexed vector, optimised for repetitions.
+data OptVector :: Type -> Nat -> Type where
+    End  :: OptVector t 0
+    (:-) :: Elem t l -> OptVector t (n - l) -> OptVector t n
+
+-- | Get the first element of an optimised vector.
+type family Head (v :: OptVector t n) :: t where
+    Head End           = TypeError (Text "Vector has no head element.")
+    Head (v :* _ :- _) = v
+
+-- | Get the first element of a simple vector.
+type family Head' (v :: Vector t n) :: t where
+    Head' None      = TypeError (Text "Vector has no head element.")
+    Head' (v :-- _) = v
+
+-- | Get the last element of the vector.
+type family Last (v :: OptVector t n) :: t where
+    Last End             = TypeError (Text "Vector has no last element.")
+    Last (v :* _ :- End) = v
+    Last (_ :- vs)       = Last vs
+
+-- | Get the tail of the vector.
+type family Tail' (v :: Vector t n) :: Vector t (n - 1) where
+    Tail' None = TypeError (Text "Vector has no tail.")
+    Tail' (_ :-- vs) = vs
+
+-- | Get everything but the last element of the vector.
+type family Init' (v :: Vector t n) :: Vector t (n - 1) where
+    Init' None = TypeError (Text "Vector is empty.")
+    Init' (p :-- None) = None
+    Init' (p :-- ps) = p :-- Init' ps
+
+-- | Get the length of an optimised vector.
+type family Length (v :: OptVector t n) :: Nat where
+    Length (v :: OptVector t n) = n
+
+-- | Get the length of a vector.
+type family Length' (v :: Vector t n) :: Nat where
+    Length' (v :: Vector t n) = n
+
+-- | Append two optimised vectors.
+type family (x :: OptVector t n) ++ (y :: OptVector t m) :: OptVector t (n + m) where
+    ys        ++ End = ys
+    End       ++ ys = ys
+    (x :- xs) ++ ys = x :- (xs ++ ys)
+
+-- | Append two simple vectors.
+type family (x :: Vector t n) ++. (y :: Vector t m) :: Vector t (n + m) where
+    None       ++. ys = ys
+    (x :-- xs) ++. ys = x :-- (xs ++. ys)
+
+-- | Add an element to the end of a simple vector.
+type family (v :: Vector t n) :-| (e :: t) :: Vector t (n + 1) where
+    v :-| e = v ++. (e :-- None)
+
+-- | Repeat the value the specified number of times to create a new 'OptVector'.
+type family (a :: t) +*+ (n :: Nat) :: OptVector t n where
+    x +*+ 0 = End
+    x +*+ n = x ** n :- End
+
+-- | A dimension-indexed matrix.
+type Matrix t p q = Vector (OptVector t q) p
+
+-- | Horizontal concatenation of type-level matrices.
+-- Places the first matrix to the left of the second.
+type family (a :: Matrix t p q) +|+ (b :: Matrix t p r) :: Matrix t p (q + r) where
+    None         +|+ None         = None
+    (r1 :-- rs1) +|+ (r2 :-- rs2) = (r1 ++ r2) :-- (rs1 +|+ rs2)
+
+-- | Vertical concatenation of type-level matrices.
+-- Places the first matrix on top of the second.
+type family (a :: Matrix t p r) +-+ (b :: Matrix t q r) :: Matrix t (p + q) r where
+    m1 +-+ m2 = ConcatPair (Align m1 m2)
+
+-- | Concatenates a type-level pair of vectors.
+type family ConcatPair (vs :: (Vector t p, Vector t q)) :: Vector t (p + q) where
+    ConcatPair '(v1, v2) = v1 ++. v2
+
+-- | Vertically aligns two matrices by separating elements so that the element
+-- boundaries line up.
+type family Align (a :: Matrix t p r) (b :: Matrix t q r) :: (Matrix t p r, Matrix t q r) where
+    Align None m = '(None, m)
+    Align m None = '(m, None)
+    Align (r1 :-- rs1) (r2 :-- rs2) =
+            '(FragmentMatByVec (r1 :-- rs1) r2, FragmentMatByVec (r2 :-- rs2) r1)
+
+-- | Fragments a matrix by a vector: all the element boundaries in the vector must
+-- also appear in the fragmented matrix.
+type family FragmentMatByVec (m :: Matrix t q p) (v :: OptVector t p) :: Matrix t q p where
+    FragmentMatByVec None       _ = None
+    FragmentMatByVec (r :-- rs) v = FragmentVecByVec r v :-- FragmentMatByVec rs v
+
+-- | Fragments a vector by another vector: all the element boundaries in the second
+-- vector must also appear in the first.
+type family FragmentVecByVec (v :: OptVector t p) (u :: OptVector t p) :: OptVector t p where
+    FragmentVecByVec End _ = End
+    -- If the lengths of the first element match up, they are not fragmented.
+    FragmentVecByVec (v :* (T :: Times k) :- vs) (u :* (T :: Times k) :- us) =
+            v ** k :- (FragmentVecByVec vs us)
+    -- If the lengths of the first elements don't match up, we fragment the element
+    -- by the shortest of the two lengths, and add the remainder as a separate element.
+    FragmentVecByVec (v :* (T :: Times k) :- vs) (u :* (T :: Times l) :- us) =
+        If (k <=? l)
+            ((v ** k) :- (FragmentVecByVec vs (u ** (l - k) :- us)))
+            ((v ** l) :- (FragmentVecByVec (v ** (k - l) :- vs) us))
+
+-- | Convert a simple vector to a column matrix.
+type family VectorToColMatrix (v :: Vector t n) (l :: Nat) :: Matrix t n l where
+    VectorToColMatrix None _ = None
+    VectorToColMatrix (v :-- vs) l = (VectorToColMatrix vs l) ++. (v ** l :- End :-- None)
+
+-------------------------------------------------------------------------------
+-- Type-level logic and arithmetic
+-------------------------------------------------------------------------------
+
+-- | Conditional expression at the type level.
+type family If (b :: Bool) (t :: k) (e :: k) :: k where
+    If True  t e = t
+    If False t e = e
+
+-- | Negation of type-level Booleans.
+type family Not (a :: Bool) :: Bool where
+    Not True  = False
+    Not False = True
+
+-- | Conjunction of type-level Booleans.
+type family (b1 :: Bool) .&&. (b2 :: Bool) :: Bool where
+    b1 .&&. b2 = If b1 b2 False
+
+-- | Disjunction of type-level Booleans.
+type family (b1 :: Bool) .||. (b2 :: Bool) :: Bool where
+    b1 .||. b2 = If b1 True b2
+
+-- | Equality of types.
+type family (a :: k) .~. (b :: k) :: Bool where
+    a .~. a = True
+    a .~. b = False
+
+-- | Returns the maximum of two natural numbers.
+type family MaxN (n1 :: Nat) (n2 :: Nat) :: Nat where
+    MaxN 0 n2 = n2
+    MaxN n1 0 = n1
+    MaxN n n = n
+    MaxN n1 n2 = If (n1 <=? n2) (n2) (n1)
+
+-- | Returns the minimum of two natural numbers.
+type family MinN (n1 :: Nat) (n2 :: Nat) :: Nat where
+    MinN 0 n2 = 0
+    MinN n1 0 = 0
+    MinN n n = n
+    MinN n1 n2 = If (n1 <=? n2) (n1) (n2)
+
+-------------------------------------------------------------------------------
+-- Constraints
+-------------------------------------------------------------------------------
+
+-- | Valid base constraint.
+type Valid = (() :: Constraint)
+
+-- | Invalid base constraint.
+type Invalid = True ~ False
+
+-- | Create a new constraint which is valid only if every element in the given
+-- vector satisfies the given unary constraint.
+-- Analogue of 'map' for constraints and vectors.
+type family AllSatisfy (c  :: a -> Constraint)
+                       (xs :: OptVector a n)
+                           :: Constraint where
+    AllSatisfy c End            = Valid
+    AllSatisfy c (x :* _ :- xs) = ((c x), AllSatisfy c xs)
+
+-- | Create a new constraint which is valid only if every pair of elements in
+-- the given optimised vectors satisfy the given binary constraint.
+-- Analogue of 'zipWith' for constraints and optimised vectors.
+type family AllPairsSatisfy (c  :: a -> b -> Constraint)
+                            (xs :: OptVector a n) (ys :: OptVector b n)
+                                :: Constraint where
+    AllPairsSatisfy c End            End            = Valid
+    AllPairsSatisfy c (x :* _ :- xs) (y :* _ :- ys) = ((c x y), AllPairsSatisfy c xs ys)
+
+-- | Create a new constraint which is valid only if every pair of elements in
+-- the given vectors satisfy the given binary constraint.
+-- Analogue of 'zipWith' for constraints and vectors.
+type family AllPairsSatisfy' (c  :: a -> b -> Constraint)
+                            (xs :: Vector a n) (ys :: Vector b n)
+                                :: Constraint where
+    AllPairsSatisfy' c None       None       = Valid
+    AllPairsSatisfy' c (x :-- xs) (y :-- ys) = ((c x y), AllPairsSatisfy' c xs ys)
+
+-- | Create a new constraint which is valid only if the given value satisfies
+-- every unary constraint in the given list.
+type family SatisfiesAll (cs :: [a -> Constraint])
+                         (xs :: a)
+                             :: Constraint where
+    SatisfiesAll '[]      a = Valid
+    SatisfiesAll (c : cs) a = (c a, SatisfiesAll cs a)
+
+-- | Create a new constraint which is valid only if every element in the given
+-- vector satisfies every unary constraint in the given list.
+type family AllSatisfyAll (c1 :: [a -> Constraint])
+                          (xs :: Vector a n)
+                              :: Constraint where
+    AllSatisfyAll _ None        = Valid
+    AllSatisfyAll cs (v :-- vs) = (SatisfiesAll cs v, AllSatisfyAll cs vs)
diff --git a/src/Mezzo/Model/Reify.hs b/src/Mezzo/Model/Reify.hs
new file mode 100644
--- /dev/null
+++ b/src/Mezzo/Model/Reify.hs
@@ -0,0 +1,42 @@
+{-# LANGUAGE TypeInType, ScopedTypeVariables, TypeFamilies, FlexibleInstances,
+    UndecidableInstances, ConstraintKinds #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Mezzo.Model.Reify
+-- Description :  MIDI exporting
+-- Copyright   :  (c) Dima Szamozvancev
+-- License     :  MIT
+--
+-- Maintainer  :  ds709@cam.ac.uk
+-- Stability   :  experimental
+-- Portability :  portable
+--
+-- Class of types which can be reified at the term level.
+--
+-----------------------------------------------------------------------------
+
+module Mezzo.Model.Reify where
+
+import Data.Kind
+
+-- | Class of types which can have a primitive representation at runtime.
+class Primitive (a :: k) where
+    -- | The type of the primitive representation.
+    type Rep a
+    -- | Convert a singleton of the type into its primitive representation.
+    prim :: sing a -> Rep a
+    -- | Pretty print a singleton of the type.
+    pretty :: sing a -> String
+
+instance {-# OVERLAPPABLE #-} Primitive t => Show (sing t) where
+    show = pretty
+
+-- | Primitive types with integer representations.
+type IntRep t = (Primitive t, Rep t ~ Int)
+
+-- | Primitive types with integer list representations.
+type IntListRep t = (Primitive t, Rep t ~ [Int])
+
+-- | Primitive types with function representations from type a to type b.
+type FunRep a b t = (Primitive t, Rep t ~ (a -> b))
diff --git a/src/Mezzo/Model/Types.hs b/src/Mezzo/Model/Types.hs
new file mode 100644
--- /dev/null
+++ b/src/Mezzo/Model/Types.hs
@@ -0,0 +1,698 @@
+{-# LANGUAGE TypeInType, GADTs, TypeOperators, TypeFamilies, UndecidableInstances,
+    TypeApplications, ScopedTypeVariables, FlexibleInstances, StandaloneDeriving, ViewPatterns #-}
+{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Mezzo.Model.Types
+-- Description :  Mezzo music types
+-- Copyright   :  (c) Dima Szamozvancev
+-- License     :  MIT
+--
+-- Maintainer  :  ds709@cam.ac.uk
+-- Stability   :  experimental
+-- Portability :  portable
+--
+-- Types modeling basic musical constructs at the type level.
+--
+-----------------------------------------------------------------------------
+
+module Mezzo.Model.Types
+    (
+    -- * Note properties
+      PitchClass (..)
+    , Accidental (..)
+    , OctaveNum (..)
+    , Duration (..)
+    -- ** Singleton types for note properties
+    , PC (..)
+    , Acc (..)
+    , Oct (..)
+    , Dur (..)
+    -- * Pitches
+    , PitchType (..)
+    , Pit (..)
+    , type (=?=)
+    , type (<<=?)
+    , type (<<?)
+    -- * Harmonic types
+    , Mode (..)
+    , ScaleDegree (..)
+    , KeyType (..)
+    , RootType (..)
+    , Mod (..)
+    , ScaDeg (..)
+    , KeyS (..)
+    , Root (..)
+    , RootToPitch
+    , PitchToNat
+    , Sharpen
+    , Flatten
+    , Dot
+    , FromRoot
+    , FromSilence
+    -- * Specialised musical vector types
+    , Voice
+    , Partiture
+    -- * Intervals
+    , IntervalSize (..)
+    , IntervalClass (..)
+    , IntervalType (..)
+    , MakeInterval
+    , HalfStepsUpBy
+    , HalfStepsDownBy
+    , RaiseBy
+    , LowerBy
+    , RaiseAllBy'
+    , LowerAllBy'
+    , RaiseByOct
+    , LowerByOct
+    , RaiseAllByOct
+    ) where
+
+import GHC.TypeLits
+import Data.Proxy
+
+import Mezzo.Model.Prim
+import Mezzo.Model.Reify
+
+infixl 3 <<=?
+infixl 3 <<?
+
+-------------------------------------------------------------------------------
+-- Note properties
+-- The "minimum complete definition" for musical notes and rests.
+-------------------------------------------------------------------------------
+
+-- | The diatonic pitch class of the note.
+data PitchClass = C | D | E | F | G | A | B
+
+-- | The accidental applied to a note.
+data Accidental = Natural | Flat | Sharp
+
+-- | The octave where the note resides (middle C is Oct4).
+data OctaveNum =
+    Oct_1 | Oct0 | Oct1 | Oct2 | Oct3 | Oct4 | Oct5 | Oct6 | Oct7 | Oct8
+
+-- | The duration of the note (a whole note has duration 32).
+type Duration = Nat
+
+---- Singleton types for note properties
+
+-- | The singleton type for 'PitchClass'.
+data PC (pc :: PitchClass) where
+    PC :: Primitive pc => PC pc
+
+-- | The singleton type for 'Accidental'.
+data Acc (acc :: Accidental) where
+    Acc :: Primitive acc => Acc acc
+
+-- | The singleton type for 'Octave'.
+data Oct (oct :: OctaveNum) where
+    Oct :: Primitive oct => Oct oct
+
+-- | The singleton type for 'Duration'.
+data Dur (dur :: Duration) where
+    Dur :: Primitive dur => Dur dur
+
+-------------------------------------------------------------------------------
+-- Pitches
+-- Encapsulates the pitch class, accidental and octave of a note.
+-------------------------------------------------------------------------------
+
+-- | The type of pitches.
+data PitchType where
+    -- | A pitch made up of a pitch class, an accidental and an octave.
+    Pitch :: PitchClass -> Accidental -> OctaveNum -> PitchType
+    -- | Silence, the pitch of rests.
+    Silence :: PitchType
+
+-- | The singleton type for pitches.
+data Pit (p :: PitchType) where
+    Pit :: Primitive p => Pit p
+
+-------------------------------------------------------------------------------
+-- Harmonic types
+-------------------------------------------------------------------------------
+
+-- | The mode of a key: major or minor.
+data Mode = MajorMode | MinorMode
+
+-- | The seven scale degrees.
+data ScaleDegree = I | II | III | IV | V | VI | VII
+
+-- | The of a scale, chord or piece.
+data KeyType = Key PitchClass Accidental Mode
+
+-- | The root of a chord.
+data RootType where
+    -- | A pitch constructs a diatonic root.
+    PitchRoot :: PitchType -> RootType
+    -- | A key and a scale degree constructs a scalar root.
+    DegreeRoot :: KeyType -> ScaleDegree -> RootType
+
+-- | The singleton type for 'Mode'.
+data Mod (m :: Mode) = Mod
+
+-- | The singleton type for 'ScaleDegree'
+data ScaDeg (sd :: ScaleDegree) = ScaDeg
+
+-- | The singleton type for 'KeyType'.
+data KeyS (k :: KeyType) = KeyS
+
+-- | The singleton type for 'Root'.
+data Root (r :: RootType) where
+    Root :: Primitive r => Root r
+
+-- | Convert a root to a pitch.
+--
+-- Note: the default octave for scalar roots is 'Oct2'.
+type family RootToPitch (dr :: RootType) :: PitchType where
+    RootToPitch (PitchRoot p) = p
+    RootToPitch (DegreeRoot (Key pc acc m) d) =
+                    HalfStepsUpBy (Pitch pc acc Oct2) (DegreeOffset m d)
+
+-- | Calculate the semitone offset of a scale degree in a given mode.
+type family DegreeOffset (m :: Mode) (d :: ScaleDegree) where
+    DegreeOffset MajorMode I   = 0
+    DegreeOffset MajorMode II  = 2
+    DegreeOffset MajorMode III = 4
+    DegreeOffset MajorMode IV  = 5
+    DegreeOffset MajorMode V   = 7
+    DegreeOffset MajorMode VI  = 9
+    DegreeOffset MajorMode VII = 11
+    DegreeOffset MinorMode I   = 0
+    DegreeOffset MinorMode II  = 2
+    DegreeOffset MinorMode III = 3
+    DegreeOffset MinorMode IV  = 5
+    DegreeOffset MinorMode V   = 7
+    DegreeOffset MinorMode VI  = 8
+    DegreeOffset MinorMode VII = 10
+
+-- | Sharpen a root.
+type family Sharpen (r :: RootType) :: RootType where
+    Sharpen r = PitchRoot (HalfStepUp (RootToPitch r))
+
+-- | Flatten a root.
+type family Flatten (r :: RootType) :: RootType where
+    Flatten r = PitchRoot (HalfStepDown (RootToPitch r))
+
+-- | Halve a type-level natural.
+type family HalfOf (n :: Nat) :: Nat where
+    HalfOf 0 = 0
+    HalfOf 1 = 0
+    HalfOf 8 = 4
+    HalfOf 32 = 16
+    HalfOf n = 1 + (HalfOf (n - 2))
+
+-- | Form a dotted duration.
+type family Dot (d :: Duration) :: Duration where
+    Dot 1 = TypeError (Text "Can't have dotted thirty-seconds.")
+    Dot n = n + HalfOf n
+
+-- | Create a new partiture with one voice of the given pitch.
+type family FromRoot (r :: RootType) (d :: Nat) :: Partiture 1 d where
+    FromRoot r d = ((RootToPitch r) +*+ d) :-- None
+
+-- | Create a new partiture with one voice of silence.
+type family FromSilence (d :: Nat) :: Partiture 1 d where
+    FromSilence d = (Silence +*+ d) :-- None
+
+-------------------------------------------------------------------------------
+-- Type specialisations
+-------------------------------------------------------------------------------
+
+-- | A 'Voice' is made up of a sequence of pitch repetitions.
+type Voice l = OptVector PitchType l
+
+-- | A 'Partiture' is made up of a fixed number of voices.
+type Partiture n l = Matrix PitchType n l
+
+-------------------------------------------------------------------------------
+-- Intervals
+-------------------------------------------------------------------------------
+
+-- | The size of the interval.
+data IntervalSize =
+    Unison | Second | Third | Fourth | Fifth | Sixth | Seventh | Octave
+
+-- | The class of the interval.
+data IntervalClass = Maj | Perf | Min | Aug | Dim
+
+-- | The type of intervals.
+data IntervalType where
+    -- | An interval smaller than 13 semitones, where musical rules
+    -- can still be enforced.
+    Interval :: IntervalClass -> IntervalSize -> IntervalType
+    -- | An interval larger than 13 semitones, which is large enough
+    -- so that dissonance effects are not significant.
+    Compound :: IntervalType
+
+-------------------------------------------------------------------------------
+-- Interval construction
+-------------------------------------------------------------------------------
+
+-- | Make an interval from two arbitrary pitches.
+type family MakeInterval (p1 :: PitchType) (p2 :: PitchType) :: IntervalType where
+    MakeInterval Silence Silence = TypeError (Text "Can't make intervals from rests.")
+    MakeInterval Silence p2      = TypeError (Text "Can't make intervals from rests.")
+    MakeInterval p1      Silence = TypeError (Text "Can't make intervals from rests.")
+    MakeInterval p1 p2 =
+        If  (p1 <<=? p2)
+            (MakeIntervalOrd p1 p2)
+            (MakeIntervalOrd p2 p1)
+
+-- | Make an interval from two ordered pitches.
+type family MakeIntervalOrd (p1 :: PitchType) (p2 :: PitchType) :: IntervalType where
+    -- Handling base cases.
+    MakeIntervalOrd p p = Interval Perf Unison
+    MakeIntervalOrd (Pitch C Natural o) (Pitch C Sharp o) = Interval Aug Unison
+    MakeIntervalOrd (Pitch C Natural o) (Pitch D Flat o) = Interval Min Second
+    MakeIntervalOrd (Pitch C acc o)     (Pitch D acc o)   = Interval Maj Second
+    MakeIntervalOrd (Pitch C acc o)     (Pitch E acc o)   = Interval Maj Third
+    MakeIntervalOrd (Pitch C acc o)     (Pitch F acc o)   = Interval Perf Fourth
+    MakeIntervalOrd (Pitch C acc o)     (Pitch G acc o)   = Interval Perf Fifth
+    MakeIntervalOrd (Pitch C acc o)     (Pitch A acc o)   = Interval Maj Sixth
+    MakeIntervalOrd (Pitch C acc o)     (Pitch B acc o)   = Interval Maj Seventh
+    -- Handling perfect and augmented octaves.
+    MakeIntervalOrd (Pitch C acc o1) (Pitch C acc o2) =
+            If (OctSucc o1 .~. o2) (Interval Perf Octave) Compound
+    MakeIntervalOrd (Pitch C Natural o1) (Pitch C Sharp o2) =
+            If (OctSucc o1 .~. o2) (Interval Aug Octave) Compound
+    MakeIntervalOrd (Pitch C Flat o1) (Pitch C Natural o2) =
+            If (OctSucc o1 .~. o2) (Interval Aug Octave) Compound
+    -- Handling accidental first pitch.
+    MakeIntervalOrd (Pitch C Flat o) (Pitch pc2 acc o) =
+            Expand (MakeIntervalOrd (Pitch C Natural o) (Pitch pc2 acc o))
+    MakeIntervalOrd (Pitch C Sharp o) (Pitch pc2 acc o) =
+            Shrink (MakeIntervalOrd (Pitch C Natural o) (Pitch pc2 acc o))
+    -- Handling accidental second pitch.
+    MakeIntervalOrd (Pitch C Natural o) (Pitch pc2 Sharp o) =
+            Expand (MakeIntervalOrd (Pitch C Natural o) (Pitch pc2 Natural o))
+    MakeIntervalOrd (Pitch C Natural o) (Pitch pc2 Flat o) =
+            Shrink (MakeIntervalOrd (Pitch C Natural o) (Pitch pc2 Natural o))
+    -- Handling the general case.
+    MakeIntervalOrd (Pitch pc1 acc1 o1) (Pitch pc2 acc2 o2) =
+            If  (o1 .~. o2 .||. OctSucc o1 .~. o2)
+                (MakeIntervalOrd (HalfStepDown (Pitch pc1 acc1 o1)) (HalfStepDown (Pitch pc2 acc2 o2)))
+                Compound
+    -- Handling erroneous construction (shouldn't happen).
+    MakeIntervalOrd _ _ = TypeError (Text "Invalid interval.")
+
+-- | Shrink an interval.
+type family Shrink (i :: IntervalType) :: IntervalType where
+    Shrink (Interval Perf Unison) = TypeError (Text "Can't diminish unisons.")
+    Shrink (Interval Perf is)     = Interval Dim is
+    Shrink (Interval Min  is)     = Interval Dim is
+    Shrink (Interval Maj  is)     = Interval Min is
+    Shrink (Interval Aug  Unison) = Interval Perf Unison
+    Shrink (Interval Aug  Fourth) = Interval Perf Fourth
+    Shrink (Interval Aug  Fifth)  = Interval Perf Fifth
+    Shrink (Interval Aug  Octave) = Interval Perf Octave
+    Shrink (Interval Aug  is)     = Interval Maj is
+    Shrink (Interval Dim  Unison) = TypeError (Text "Can't diminish unisons.")
+    Shrink (Interval Dim  Second) = TypeError (Text "Can't diminish unisons.")
+    Shrink (Interval Dim  Fifth)  = Interval Perf Fourth
+    Shrink (Interval Dim  Sixth)  = Interval Dim Fifth
+    Shrink (Interval Dim  is)     = Interval Min (IntSizePred is)
+    Shrink  Compound              = Compound
+
+-- | Expand an interval.
+type family Expand (i :: IntervalType) :: IntervalType where
+    Expand (Interval Perf Octave)  = Interval Aug Octave
+    Expand (Interval Perf is)      = Interval Aug is
+    Expand (Interval Maj  is)      = Interval Aug is
+    Expand (Interval Min  is)      = Interval Maj is
+    Expand (Interval Dim  Unison)  = TypeError (Text "Can't diminish unisons.")
+    Expand (Interval Dim  Fourth)  = Interval Perf Fourth
+    Expand (Interval Dim  Fifth)   = Interval Perf Fifth
+    Expand (Interval Dim  Octave)  = Interval Perf Octave
+    Expand (Interval Dim  is)      = Interval Min is
+    Expand (Interval Aug  Third)   = Interval Aug Fourth
+    Expand (Interval Aug  Fourth)  = Interval Perf Fifth
+    Expand (Interval Aug  Seventh) = Interval Aug Octave
+    Expand (Interval Aug  Octave)  = Compound
+    Expand (Interval Aug  is)      = Interval Maj (IntSizeSucc is)
+    Expand  Compound               = Compound
+
+-------------------------------------------------------------------------------
+-- Enumerations and orderings
+-- Implementation of enumerators and ordering relations for applicable types.
+-------------------------------------------------------------------------------
+
+-- | Convert a pitch to a natural number (equal to its MIDI code).
+type family PitchToNat (p :: PitchType) :: Nat where
+    PitchToNat Silence = TypeError (Text "Can't convert a rest to a number.")
+    PitchToNat (Pitch C Natural Oct_1) = 0
+    PitchToNat (Pitch C Sharp Oct_1)   = 1
+    PitchToNat (Pitch D Flat Oct_1)    = 1
+    PitchToNat (Pitch C Natural Oct1)  = 24
+    PitchToNat (Pitch C Natural Oct2)  = 36
+    PitchToNat (Pitch C Natural Oct3)  = 48
+    PitchToNat (Pitch C Natural Oct4)  = 60
+    PitchToNat (Pitch C Natural Oct5)  = 72
+    PitchToNat (Pitch C Natural Oct6)  = 84
+    PitchToNat p                       = 1 + PitchToNat (HalfStepDown p)
+
+-- | Convert a natural number to a suitable pitch.
+-- Not a functional relation, so usage is not recommended.
+type family NatToPitch (n :: Nat) where
+    NatToPitch 0 = Pitch C Natural Oct_1
+    NatToPitch 1 = Pitch C Sharp Oct_1
+    NatToPitch n = HalfStepUp (NatToPitch (n - 1))
+
+-- | Greater than or equal to for pitches.
+type family (p1 :: PitchType) <<=? (p2 :: PitchType) where
+    p1 <<=? p2 = PitchToNat p1 <=? PitchToNat p2
+
+-- | Greater than for pitches.
+type family (p1 :: PitchType) <<? (p2 :: PitchType) where
+    p1 <<? p2 = (p1 <<=? p2) .&&. Not (p1 .~. p2)
+
+-- | Enharmonic equality of pitches.
+type family (p :: PitchType) =?= (q :: PitchType) :: Bool where
+    Silence             =?= Silence             = True
+    Silence             =?= _                   = False
+    _                   =?= Silence             = False
+    Pitch pc acc oct    =?= Pitch pc acc oct    = True
+    Pitch C Flat o1     =?= Pitch B Natural o2  = o1 .~. OctSucc o2
+    Pitch C Natural o1  =?= Pitch B Sharp o2    = o1 .~. OctSucc o2
+    Pitch E Natural oct =?= Pitch F Flat oct    = True
+    Pitch E Sharp oct   =?= Pitch F Natural oct = True
+    Pitch F Flat oct    =?= Pitch E Natural oct = True
+    Pitch F Natural oct =?= Pitch E Sharp oct   = True
+    Pitch B Natural o1  =?= Pitch C Flat o2     = OctSucc o1 .~. o2
+    Pitch B Sharp o1    =?= Pitch C Natural o2  = OctSucc o1 .~. o2
+    Pitch pc1 Sharp oct =?= Pitch pc2 Flat oct  = ClassSucc pc1 .~. pc2
+    Pitch pc1 Flat oct  =?= Pitch pc2 Sharp oct = pc1 .~. ClassSucc pc2
+    _                   =?= _                   = False
+
+-- | Convert an octave to a natural number.
+type family OctToNat (o :: OctaveNum) :: Nat where
+    OctToNat Oct_1 = 0
+    OctToNat Oct0  = 1
+    OctToNat Oct1  = 2
+    OctToNat Oct2  = 3
+    OctToNat Oct3  = 4
+    OctToNat Oct4  = 5
+    OctToNat Oct5  = 6
+    OctToNat Oct6  = 7
+    OctToNat Oct7  = 8
+    OctToNat Oct8  = 9
+
+-- | Convert a natural number to an octave.
+type family NatToOct (n :: Nat) :: OctaveNum where
+    NatToOct 0 = Oct_1
+    NatToOct 1 = Oct0
+    NatToOct 2 = Oct1
+    NatToOct 3 = Oct2
+    NatToOct 4 = Oct3
+    NatToOct 5 = Oct4
+    NatToOct 6 = Oct5
+    NatToOct 7 = Oct6
+    NatToOct 8 = Oct7
+    NatToOct 9 = Oct8
+    NatToOct _ = TypeError (Text "Invalid octave.")
+
+-- | Increase the octave by the given number.
+type family IncreaseOctave (o :: OctaveNum) (n :: Nat) :: OctaveNum where
+    IncreaseOctave o n = NatToOct (OctToNat o + n)
+
+-- | Decrease the octave by the given number.
+type family DecreaseOctave (o :: OctaveNum) (n :: Nat) :: OctaveNum where
+    DecreaseOctave o n = NatToOct (OctToNat o - n)
+
+-- | Increment an octave.
+type family OctSucc (o :: OctaveNum) :: OctaveNum where
+    OctSucc o = IncreaseOctave o 1
+
+-- | Decrement an octave.
+type family OctPred (o :: OctaveNum) :: OctaveNum where
+    OctPred o = DecreaseOctave o 1
+
+-- | Convert a pitch class to a natural number.
+type family ClassToNat (pc :: PitchClass) :: Nat where
+    ClassToNat C = 0
+    ClassToNat D = 1
+    ClassToNat E = 2
+    ClassToNat F = 3
+    ClassToNat G = 4
+    ClassToNat A = 5
+    ClassToNat B = 6
+
+-- | Convert a natural number to a pitch class.
+-- Numbers are taken modulo 7: e.g. 8 corresponds to the pitch 8 mod 7 = 1 = D
+type family NatToClass (n :: Nat) :: PitchClass where
+    NatToClass 0 = C
+    NatToClass 1 = D
+    NatToClass 2 = E
+    NatToClass 3 = F
+    NatToClass 4 = G
+    NatToClass 5 = A
+    NatToClass 6 = B
+    NatToClass n = NatToClass (n - 7)
+
+-- | Increase the pitch class by a given number.
+type family IncreaseClass (pc :: PitchClass) (n :: Nat) :: PitchClass where
+    IncreaseClass pc n = NatToClass (ClassToNat pc + n)
+
+-- | Decrease the pitch class by a given number.
+type family DecreaseClass (pc :: PitchClass) (n :: Nat) :: PitchClass where
+    DecreaseClass pc n = NatToClass (ClassToNat pc - n)
+
+-- | Increment a pitch class.
+type family ClassSucc (pc :: PitchClass) :: PitchClass where
+    ClassSucc pc = IncreaseClass pc 1
+
+-- | Decrement a pitch class.
+type family ClassPred (pc :: PitchClass) :: PitchClass where
+    ClassPred pc = DecreaseClass pc 1
+
+-- | Convert an interval size to a natural number.
+type family IntSizeToNat (is :: IntervalSize) :: Nat where
+    IntSizeToNat Unison  = 0
+    IntSizeToNat Second  = 1
+    IntSizeToNat Third   = 2
+    IntSizeToNat Fourth  = 3
+    IntSizeToNat Fifth   = 4
+    IntSizeToNat Sixth   = 5
+    IntSizeToNat Seventh = 6
+    IntSizeToNat Octave  = 7
+
+-- | Convert a natural number to an interval size.
+type family NatToIntSize (n :: Nat) :: IntervalSize where
+    NatToIntSize 0 = Unison
+    NatToIntSize 1 = Second
+    NatToIntSize 2 = Third
+    NatToIntSize 3 = Fourth
+    NatToIntSize 4 = Fifth
+    NatToIntSize 5 = Sixth
+    NatToIntSize 6 = Seventh
+    NatToIntSize 7 = Octave
+    NatToIntSize _ = TypeError (Text "Invalid interval size.")
+
+-- | Increase the interval size by a given number.
+type family IncreaseIntSize (is :: IntervalSize) (n :: Nat) :: IntervalSize where
+    IncreaseIntSize is n = NatToIntSize (IntSizeToNat is + n)
+
+-- | Decrease the interval size by a given number.
+type family DecreaseIntSize (is :: IntervalSize) (n :: Nat) :: IntervalSize where
+    DecreaseIntSize is n = NatToIntSize (IntSizeToNat is - n)
+
+-- | Increment an interval size.
+type family IntSizeSucc (is :: IntervalSize) :: IntervalSize where
+    IntSizeSucc is = IncreaseIntSize is 1
+
+-- | Decrement an interval size.
+type family IntSizePred (is :: IntervalSize) :: IntervalSize where
+    IntSizePred is = DecreaseIntSize is 1
+
+-- | Calculate the width of an interval in half-steps.
+type family IntervalWidth (i :: IntervalType) :: Nat where
+    IntervalWidth (Interval Dim Unison)  = TypeError (Text "Can't diminish unisons.")
+    IntervalWidth (Interval Perf Unison) = 0
+    IntervalWidth (Interval Aug Unison)  = 1
+    IntervalWidth (Interval Dim Fourth)  = 4
+    IntervalWidth (Interval Perf Fourth) = 5
+    IntervalWidth (Interval Aug Fourth)  = 6
+    IntervalWidth (Interval Dim Fifth)   = 6
+    IntervalWidth (Interval Perf Fifth)  = 7
+    IntervalWidth (Interval Aug Fifth)   = 8
+    IntervalWidth (Interval Dim Octave)  = 11
+    IntervalWidth (Interval Perf Octave) = 12
+    IntervalWidth (Interval Aug Octave)  = 13
+    IntervalWidth (Interval Maj Second)  = 2
+    IntervalWidth (Interval Maj Third)   = 4
+    IntervalWidth (Interval Maj Sixth)   = 9
+    IntervalWidth (Interval Maj Seventh) = 11
+    IntervalWidth (Interval Aug is)      = IntervalWidth (Interval Maj is) + 1
+    IntervalWidth (Interval Min is)      = IntervalWidth (Interval Maj is) - 1
+    IntervalWidth (Interval Dim is)      = IntervalWidth (Interval Maj is) - 2
+
+-- | Move a pitch up by a semitone.
+type family HalfStepUp (p :: PitchType) :: PitchType where
+    HalfStepUp Silence              = Silence
+    HalfStepUp (Pitch B  Flat    o) = Pitch B Natural o
+    HalfStepUp (Pitch B  acc     o) = Pitch C acc (OctSucc o)
+    HalfStepUp (Pitch E  Flat    o) = Pitch E Natural o
+    HalfStepUp (Pitch E  acc     o) = Pitch F acc o
+    HalfStepUp (Pitch pc Flat    o) = Pitch pc Natural o
+    HalfStepUp (Pitch pc Natural o) = Pitch pc Sharp o
+    HalfStepUp (Pitch pc Sharp   o) = Pitch (ClassSucc pc) Natural o
+
+-- | Move a pitch down by a semitone.
+type family HalfStepDown (p :: PitchType) :: PitchType where
+    HalfStepDown Silence              = Silence
+    HalfStepDown (Pitch C  Sharp   o) = Pitch C Natural o
+    HalfStepDown (Pitch C  acc     o) = Pitch B acc (OctPred o)
+    HalfStepDown (Pitch F  Sharp   o) = Pitch F Natural o
+    HalfStepDown (Pitch F  acc     o) = Pitch E acc o
+    HalfStepDown (Pitch pc Flat    o) = Pitch (ClassPred pc) Natural o
+    HalfStepDown (Pitch pc Natural o) = Pitch pc Flat o
+    HalfStepDown (Pitch pc Sharp   o) = Pitch pc Natural o
+
+-- | Move a pitch up by the specified number of semitones.
+type family HalfStepsUpBy (p :: PitchType) (n :: Nat) :: PitchType where
+    HalfStepsUpBy p 0 = p
+    HalfStepsUpBy p n = HalfStepUp (HalfStepsUpBy p (n - 1))
+
+-- | Move a pitch down by the specified number of semitones.
+type family HalfStepsDownBy (p :: PitchType) (n :: Nat) :: PitchType where
+    HalfStepsDownBy p 0 = p
+    HalfStepsDownBy p n = HalfStepDown (HalfStepsDownBy p (n - 1))
+
+-- | Raise a pitch by an interval.
+type family RaiseBy (p :: PitchType) (i :: IntervalType) :: PitchType where
+    RaiseBy Silence _           = Silence
+    RaiseBy _ Compound          = TypeError (Text "Can't shift by compound interval")
+    RaiseBy p (Interval Min is) = HalfStepDown (HalfStepsUpBy p (IntervalWidth (Interval Min is) + 1))
+    RaiseBy p (Interval Dim is) = HalfStepDown (HalfStepsUpBy p (IntervalWidth (Interval Dim is) + 1))
+    RaiseBy p i                 = HalfStepsUpBy p (IntervalWidth i)
+
+-- | Lower a pitch by an interval.
+type family LowerBy (p :: PitchType) (i :: IntervalType) :: PitchType where
+    LowerBy Silence _           = Silence
+    LowerBy _ Compound          = TypeError (Text "Can't shift by compound interval")
+    LowerBy p (Interval Maj is) = HalfStepUp (HalfStepsDownBy p (IntervalWidth (Interval Maj is) + 1))
+    LowerBy p (Interval Aug is) = HalfStepUp (HalfStepsDownBy p (IntervalWidth (Interval Aug is) + 1))
+    LowerBy p i                 = HalfStepsDownBy p (IntervalWidth i)
+
+-- | Raise all pitches in a voice by an interval.
+type family RaiseAllBy (ps :: Voice l) (i :: IntervalType) :: Voice l where
+    RaiseAllBy End _ = End
+    RaiseAllBy (p :* d :- ps) i = RaiseBy p i :* d :- RaiseAllBy ps i
+
+-- | Raise multiple pitches by an interval.
+type family RaiseAllBy' (ps :: Vector PitchType n) (i :: IntervalType) :: Vector PitchType n where
+    RaiseAllBy' None _ = None
+    RaiseAllBy' (p :-- ps) i = RaiseBy p i :-- RaiseAllBy' ps i
+
+-- | Lower all pitches in a voice by an interval.
+type family LowerAllBy (ps :: Voice l) (i :: IntervalType) :: Voice l where
+    LowerAllBy End _ = End
+    LowerAllBy (p :* d :- ps) i = LowerBy p i :* d :- LowerAllBy ps i
+
+-- | Lower multiple pitches by an interval.
+type family LowerAllBy' (ps :: Vector PitchType n) (i :: IntervalType) :: Vector PitchType n where
+    LowerAllBy' None _ = None
+    LowerAllBy' (p :-- ps) i = LowerBy p i :-- LowerAllBy' ps i
+
+-- | Raise a pitch by an octave.
+type family RaiseByOct (p :: PitchType) :: PitchType where
+    RaiseByOct p = RaiseBy p (Interval Perf Octave)
+
+-- | Lower a pitch by an octave.
+type family LowerByOct (p :: PitchType) :: PitchType where
+    LowerByOct p = LowerBy p (Interval Perf Octave)
+
+type family RaiseAllByOct (ps :: Voice l) :: Voice l where
+    RaiseAllByOct v = RaiseAllBy v (Interval Perf Octave)
+
+-------------------------------------------------------------------------------
+-- Primitive instances
+-------------------------------------------------------------------------------
+
+instance Primitive Oct_1 where type Rep Oct_1 = Int ; prim o = 0 ; pretty o = "_5"
+instance Primitive Oct0 where type Rep Oct0 = Int ; prim o = 12 ; pretty o = "_4"
+instance Primitive Oct1 where type Rep Oct1 = Int ; prim o = 24 ; pretty o = "_3"
+instance Primitive Oct2 where type Rep Oct2 = Int ; prim o = 36 ; pretty o = "__"
+instance Primitive Oct3 where type Rep Oct3 = Int ; prim o = 48 ; pretty o = "_ "
+instance Primitive Oct4 where type Rep Oct4 = Int ; prim o = 60 ; pretty o = "  "
+instance Primitive Oct5 where type Rep Oct5 = Int ; prim o = 72 ; pretty o = "' "
+instance Primitive Oct6 where type Rep Oct6 = Int ; prim o = 84 ; pretty o = "''"
+instance Primitive Oct7 where type Rep Oct7 = Int ; prim o = 96 ; pretty o = "'3"
+instance Primitive Oct8 where type Rep Oct8 = Int ; prim o = 108; pretty o = "'4"
+
+instance Primitive C where type Rep C = Int ; prim p = 0 ; pretty p = "C"
+instance Primitive D where type Rep D = Int ;  prim p = 2 ; pretty p = "D"
+instance Primitive E where type Rep E = Int ;  prim p = 4 ; pretty p = "E"
+instance Primitive F where type Rep F = Int ;  prim p = 5 ; pretty p = "F"
+instance Primitive G where type Rep G = Int ;  prim p = 7 ; pretty p = "G"
+instance Primitive A where type Rep A = Int ;  prim p = 9 ; pretty p = "A"
+instance Primitive B where type Rep B = Int ;  prim p = 11; pretty p = "B"
+
+instance Primitive Natural where type Rep Natural = Int ; prim a = 0 ; pretty a = " "
+instance Primitive Flat where type Rep Flat = Int ; prim a = -1 ; pretty a = "b"
+instance Primitive Sharp where type Rep Sharp = Int ; prim a = 1 ; pretty a = "#"
+
+-- "Equality constraints are literally magic."
+--                                  - Michael Gale, 2017
+instance (IntRep pc, IntRep acc, IntRep oct)
+        => Primitive (Pitch pc acc oct) where
+    type Rep (Pitch pc acc oct) = Int
+    prim p = prim (PC @pc) + prim (Acc @acc) + prim (Oct @oct)
+    pretty p = pretty (PC @pc) ++ pretty (Acc @acc) ++ pretty (Oct @oct)
+
+instance Primitive Silence where type Rep Silence = Int ; prim s = 60 ; pretty s = "~~~~"
+
+instance IntRep p => Primitive (Root (PitchRoot p)) where
+    type Rep (Root (PitchRoot p)) = Int
+    prim r = prim (Pit @p)
+    pretty r = pretty (Pit @p)
+
+-- Modes
+instance Primitive MajorMode where type Rep MajorMode = Bool ; prim m = True ; pretty m = "Major"
+instance Primitive MinorMode where type Rep MinorMode = Bool ; prim m = False ; pretty m = "minor"
+
+-- Scale degrees
+instance Primitive I    where type Rep I    = Int ; prim d = 0 ; pretty d = "I"
+instance Primitive II   where type Rep II   = Int ; prim d = 1 ; pretty d = "II"
+instance Primitive III  where type Rep III  = Int ; prim d = 2 ; pretty d = "III"
+instance Primitive IV   where type Rep IV   = Int ; prim d = 3 ; pretty d = "IV"
+instance Primitive V    where type Rep V    = Int ; prim d = 4 ; pretty d = "V"
+instance Primitive VI   where type Rep VI   = Int ; prim d = 5 ; pretty d = "VI"
+instance Primitive VII  where type Rep VII  = Int ; prim d = 6 ; pretty d = "VII"
+
+
+instance (IntRep pc, IntRep acc, IntRep mo) => Primitive (Key pc acc mo) where
+    type Rep (Key pc acc mo) = Int
+    prim k = 0 -- to be changed
+    pretty k = pretty (PC @pc) ++ pretty (Acc @acc) ++ " " ++ pretty (Mod @mo)
+
+
+instance (IntRep p, RootToPitch (DegreeRoot k sd) ~ p, Primitive sd)
+        => Primitive (Root (DegreeRoot k sd)) where
+    type Rep (Root (DegreeRoot k sd)) = Int
+    prim r = prim (Pit @p)
+    pretty r = pretty (ScaDeg @sd)
+
+instance IntRep p => Primitive (PitchRoot p) where
+    type Rep (PitchRoot p) = Int
+    prim p = prim (Pit @p)
+    pretty p = pretty (Pit @p)
+
+instance KnownNat n => Primitive n where
+    type Rep n = Int
+    prim = fromInteger . natVal
+    pretty (natVal -> 1) = "Th"
+    pretty (natVal -> 2) = "Si"
+    pretty (natVal -> 3) = "Si."
+    pretty (natVal -> 4) = "Ei"
+    pretty (natVal -> 6) = "Ei."
+    pretty (natVal -> 8) = "Qu"
+    pretty (natVal -> 12) = "Qu."
+    pretty (natVal -> 16) = "Ha"
+    pretty (natVal -> 24) = "Ha."
+    pretty (natVal -> 32) = "Wh"
+    pretty (natVal -> 48) = "Wh."
+    pretty (natVal -> n) = ":" ++ show n
diff --git a/src/Mezzo/Render/MIDI.hs b/src/Mezzo/Render/MIDI.hs
new file mode 100644
--- /dev/null
+++ b/src/Mezzo/Render/MIDI.hs
@@ -0,0 +1,116 @@
+{-# LANGUAGE TypeInType, GADTs #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Mezzo.Render.MIDI
+-- Description :  MIDI exporting
+-- Copyright   :  (c) Dima Szamozvancev
+-- License     :  MIT
+--
+-- Maintainer  :  ds709@cam.ac.uk
+-- Stability   :  experimental
+-- Portability :  portable
+--
+-- Functions for exporting Mezzo compositions into MIDI files.
+-- Skeleton code by Stephen Lavelle.
+--
+-----------------------------------------------------------------------------
+
+module Mezzo.Render.MIDI
+    ( renderMusic, musicToMidi )
+    where
+
+import Mezzo.Model
+
+import Codec.Midi
+
+-------------------------------------------------------------------------------
+-- Types
+-------------------------------------------------------------------------------
+
+-- | A MIDI representation of a musical note.
+data MidiNote = MidiNote
+    { noteNum :: Int        -- ^ MIDI number of a note (middle C is 60).
+    , vel     :: Velocity   -- ^ Performance velocity of the note.
+    , start   :: Ticks      -- ^ Relative start time of the note.
+    , noteDur :: Ticks      -- ^ Duration of the note.
+    } deriving Show
+
+-- | A MIDI event: a MIDI message at a specific timestamp.
+type MidiEvent = (Ticks, Message)
+
+-- | A sequence of MIDI events.
+type MidiTrack = Track Ticks
+
+-------------------------------------------------------------------------------
+-- Operations
+-------------------------------------------------------------------------------
+
+-- | Play a MIDI note with the specified duration and default velocity.
+midiNote :: Int -> Ticks -> MidiNote
+midiNote root dur = MidiNote {noteNum = root, vel = 100, start = 0, noteDur = dur}
+
+midiRest :: Ticks -> MidiNote
+midiRest dur = MidiNote {noteNum = 60, vel = 0, start = 0, noteDur = dur}
+
+-- | Start playing the specified 'MidiNote'.
+keyDown :: MidiNote -> MidiEvent
+keyDown n = (start n, NoteOn {channel = 0, key = noteNum n, velocity = vel n})
+
+-- | Stop playing the specified 'MidiNote'.
+keyUp :: MidiNote -> MidiEvent
+keyUp n = (start n + noteDur n, NoteOn {channel = 0, key = noteNum n, velocity = 0})
+
+-- | Play the specified 'MidiNote'.
+playNote :: Int -> Ticks -> MidiTrack
+playNote root dur = map ($ midiNote root dur) [keyDown, keyUp]
+
+-- | Play a rest of the specified duration.
+playRest :: Ticks -> MidiTrack
+playRest dur = map ($ midiRest dur) [keyDown, keyUp]
+
+-- | Merge two parallel MIDI tracks.
+(><) :: MidiTrack -> MidiTrack -> MidiTrack
+m1 >< m2 = removeTrackEnds $ m1 `merge` m2
+
+-- | Convert a 'Dur' to 'Ticks'.
+durToTicks :: Primitive d => Dur d -> Ticks
+durToTicks d = prim d * 60 -- 1 Mezzo tick (a 32nd note) ~ 60 MIDI ticks
+
+-------------------------------------------------------------------------------
+-- Rendering
+-------------------------------------------------------------------------------
+
+-- | A basic skeleton of a MIDI file.
+midiSkeleton :: MidiTrack -> Midi
+midiSkeleton mel = Midi
+    { fileType = MultiTrack
+    , timeDiv = TicksPerBeat 480
+    , tracks =
+        [ [ (0, ChannelPrefix 0)
+          , (0, TrackName " Grand Piano  ")
+          , (0, InstrumentName "GM Device  1")
+          , (0, TimeSignature 4 2 24 8)
+          , (0, KeySignature 0 0)
+          ]
+        ++ mel
+        ++ [ (0, TrackEnd) ]
+        ]
+    }
+
+-- | Convert a 'Music' piece into a 'MidiTrack'.
+musicToMidi :: Music m -> MidiTrack
+musicToMidi (Note root dur) = playNote (prim root) (durToTicks dur)
+musicToMidi (Rest dur) = playRest (durToTicks dur)
+musicToMidi (m1 :|: m2) = musicToMidi m1 ++ musicToMidi m2
+musicToMidi (m1 :-: m2) = musicToMidi m1 >< musicToMidi m2
+musicToMidi (Chord c d) = foldr1 (><) notes
+    where notes = map (`playNote` durToTicks d) $ prim c
+
+-- | Create a MIDI file with the specified name and track.
+createMidi :: FilePath -> MidiTrack -> IO ()
+createMidi f notes = exportFile f $ midiSkeleton notes
+
+-- | Create a MIDI file with the specified path and composition.
+renderMusic :: FilePath -> Music m -> IO ()
+renderMusic f m = createMidi f (musicToMidi m)
diff --git a/test/Main.hs b/test/Main.hs
new file mode 100644
--- /dev/null
+++ b/test/Main.hs
@@ -0,0 +1,13 @@
+
+
+module Main where
+
+import Test.Hspec
+
+import PrimSpec
+import TypeSpec
+
+main :: IO ()
+main = mapM_ hspec [ primSpec
+                   , typeSpec
+                   ]
diff --git a/test/PrimSpec.hs b/test/PrimSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/PrimSpec.hs
@@ -0,0 +1,304 @@
+{-# OPTIONS_GHC -fdefer-type-errors #-}
+-- {-# OPTIONS_GHC -w #-}
+{-# LANGUAGE TypeInType, TypeOperators, GADTs, MultiParamTypeClasses, FlexibleInstances #-}
+
+module PrimSpec where
+
+import Test.Hspec
+import GHC.TypeLits
+import Control.Exception (evaluate)
+import Test.ShouldNotTypecheck (shouldNotTypecheck)
+
+import Mezzo.Model.Prim
+
+primSpec :: Spec
+primSpec =
+    describe "Mezzo.Model.Prim" $ do
+        describe "Vector operations" $ do
+            it "should replicate elements" $
+                timesReplicate `shouldBe` True
+            it "should get the head of an optimised vector" $
+                optVectorHead `shouldBe` True
+            it "should get the head of a vector" $
+                vectorHead `shouldBe` True
+            it "should get the last element of an optimised vector" $
+                optVectorLast `shouldBe` True
+            it "should get the tail of a vector" $
+                vectorTail `shouldBe` True
+            it "should get the initial elements of a vector" $
+                vectorInit `shouldBe` True
+            it "should get the length of an optimised vector" $
+                optVectorLength `shouldBe` True
+            it "should get the length of a vector" $
+                vectorLength `shouldBe` True
+            it "should append optimised vectors" $
+                optVectorAppend `shouldBe` True
+            it "should append vectors" $
+                vectorAppend `shouldBe` True
+            it "should add an element to the end of a vector" $
+                snoc `shouldBe` True
+            it "should repeat an element to an optimised vector" $
+                repeatVec `shouldBe` True
+
+        describe "Matrix operations" $ do
+            it "should vertically align matrices" $
+                align `shouldBe` True
+            it "should horizontally concatenate matrices" $
+                matHConcat `shouldBe` True
+            it "should vertically concatenate matrices" $
+                matVConcat `shouldBe` True
+            it "should convert vectors to column matrices" $
+                vecToColMatrix `shouldBe` True
+
+        describe "Arithmetic operations" $ do
+            it "should calculate maximum of two numbers" $ do
+                maxNat `shouldBe` True
+            it "should calculate minimum of two numbers" $ do
+                minNat `shouldBe` True
+
+        describe "Constraint operations" $ do
+            it "should apply a constraint to an optimised vector" $ do
+                allSatisfy `shouldBe` True
+                -- shouldNotTypecheck allSatisfyInv
+            it "should apply a binary constraint to two optimised vectors" $ do
+                allPairsSatisfy `shouldBe` True
+                shouldNotTypecheck allPairsSatisfyInv
+            it "should apply a binary constraint to two vectors" $ do
+                allPairsSatisfy' `shouldBe` True
+                shouldNotTypecheck allPairsSatisfyInv'
+            it "should apply all constraints to a value" $ do
+                satisfiesAll `shouldBe` True
+                -- shouldNotTypecheck satisfiesAllInv
+            it "should apply all constraints to all values" $ do
+                allSatisfyAll `shouldBe` True
+                -- shouldNotTypecheck allSatisfyAllInv
+
+
+timesReplicate :: (True ** 23) ~ (True :* (T :: Times 23)) => Bool
+timesReplicate = True
+
+optVectorHead :: (Head (True ** 4 :- End)) ~ True => Bool
+optVectorHead = True
+
+vectorHead :: (Head' (True :-- None)) ~ True => Bool
+vectorHead = True
+
+optVectorLast :: (Last (True ** 4 :- False ** 9 :- End)) ~ False => Bool
+optVectorLast = True
+
+vectorTail :: (Tail' (True :-- False :-- None)) ~ (False :-- None) => Bool
+vectorTail = True
+
+vectorInit :: (Init' (True :-- False :-- None)) ~ (True :-- None) => Bool
+vectorInit = True
+
+optVectorLength :: (Length (True ** 4 :- False ** 9 :- End)) ~ 13 => Bool
+optVectorLength = True
+
+vectorLength :: (Length' (True :-- False :-- None)) ~ 2 => Bool
+vectorLength = True
+
+optVectorAppend :: ((True ** 5 :- False ** 2 :- End) ++ End ++ (False ** 9 :- End))
+                  ~ (True ** 5 :- False ** 2 :- False ** 9 :- End) => Bool
+optVectorAppend = True
+
+vectorAppend :: ((2 :-- 43 :-- None) ++. None ++. (6 :-- None))
+                  ~ (2 :-- 43 :-- 6 :-- None) => Bool
+vectorAppend = True
+
+snoc :: ((2 :-- 5 :-- None) :-| 6) ~ (2 :-- 5 :-- 6 :-- None) => Bool
+snoc = True
+
+repeatVec :: (True +*+ 3) ~ (True ** 3 :- End) => Bool
+repeatVec = True
+
+matHConcat ::
+          -- Normal matrices
+        ( ((True ** 2 :- End :-- False ** 2 :- End :-- None)
+           +|+ (False ** 5 :- End :-- True ** 5 :- End :-- None))
+          ~ ((True ** 2 :- False ** 5 :- End :-- False ** 2 :- True ** 5 :- End :-- None))
+          -- Right empty
+        , ((True ** 2 :- End :-- False ** 2 :- End :-- None)
+           +|+ (End :-- End :-- None))
+          ~ (True ** 2 :- End :-- False ** 2 :- End :-- None)
+          -- Left empty
+        , ((End :-- End :-- None)
+           +|+ (True ** 2 :- End :-- False ** 2 :- End :-- None))
+          ~ (True ** 2 :- End :-- False ** 2 :- End :-- None)
+          -- Both empty
+        , (None +|+ None) ~ None
+        ) => Bool
+matHConcat = True
+
+align ::
+          -- Right fragment
+        ( Align (True ** 2 :- False ** 2 :- End :-- None) (True ** 4 :- End :-- None)
+          ~ '(True ** 2 :- False ** 2 :- End :-- None, True ** 2 :- True ** 2 :- End :-- None)
+          -- Left fragment
+        , Align (False ** 18 :- End :-- None) (True ** 8 :- False ** 10 :- End :-- None)
+          ~ '(False ** 8 :- False ** 10 :- End :-- None, True ** 8 :- False ** 10 :- End :-- None)
+          -- No fragment
+        , Align (True ** 4 :- End :-- None) (False ** 4 :- End :-- None)
+          ~ '(True ** 4 :- End :-- None, False ** 4 :- End :-- None)
+          -- Both fragment
+        , Align (False ** 18 :- True ** 3 :- End :-- None) (True ** 8 :- False ** 13 :- End :-- None)
+          ~ '(False ** 8 :- False ** 10 :- True ** 3 :- End :-- None, True ** 8 :- False ** 10 :- False ** 3 :- End :-- None)
+        ) => Bool
+align = True
+
+matVConcat ::
+          -- No fragmentation
+        (    ((True ** 3 :- False ** 6 :- End :-- None)
+          +-+ (False ** 3 :- True ** 6 :- End :-- None))
+          ~ (True ** 3 :- False ** 6 :- End :-- False ** 3 :- True ** 6 :- End :-- None)
+          -- Top fragment
+        ,    ((True ** 9 :- End :-- None)
+          +-+ (False ** 3 :- True ** 6 :- End :-- None))
+          ~ (True ** 3 :- True ** 6 :- End :-- False ** 3 :- True ** 6 :- End :-- None)
+          -- Bottom fragment
+        ,    ((True ** 3 :- False ** 6 :- End :-- None)
+          +-+ (False ** 9 :- End :-- None))
+          ~ (True ** 3 :- False ** 6 :- End :-- False ** 3 :- False ** 6 :- End :-- None)
+          -- Both fragment
+        ,    ((True ** 3 :- False ** 6 :- End :-- None)
+          +-+ (False ** 6 :- True ** 3 :- End :-- None))
+          ~ (True ** 3 :- False ** 3 :- False ** 3 :- End :-- False ** 3 :- False ** 3 :- True ** 3 :- End :-- None)
+          -- More voices
+        ,    ((True ** 2 :- False ** 8 :- End :-- False ** 2 :- True ** 8 :- End :-- None)
+          +-+ (False ** 4 :- True ** 6 :- End :-- None)
+          +-+ (True ** 1 :- False ** 8 :- True ** 1 :- End :-- False ** 1 :- True ** 8 :- False ** 1 :- End :-- None))
+          ~    ((True ** 1 :- True ** 1 :- False ** 2 :- False ** 5 :- False ** 1 :- End)
+            :-- (False ** 1 :- False ** 1 :- True ** 2 :- True ** 5 :- True ** 1 :- End)
+            :-- (False ** 1 :- False ** 1 :- False ** 2 :- True ** 5 :- True ** 1 :- End)
+            :-- (True ** 1 :- False ** 1 :- False ** 2 :- False ** 5 :- True ** 1 :- End)
+            :-- (False ** 1 :- True ** 1 :- True ** 2 :- True ** 5 :- False ** 1 :- End) :-- None
+            )
+        ) => Bool
+matVConcat = True
+
+vecToColMatrix ::
+        ( (VectorToColMatrix (True :-- False :-- None) 24)
+          ~ (False ** 24 :- End :-- True ** 24 :- End :-- None)
+        , (VectorToColMatrix None 11) ~ None
+        ) => Bool
+vecToColMatrix = True
+
+
+-- Let's assume that the Boolean functions work...
+
+maxNat :: ((MaxN 5 9) ~ 9, (MaxN 7 4) ~ 7, (MaxN 0 8) ~ 8, (MaxN 1 0) ~ 1, (MaxN 3 3) ~ 3
+          , (MaxN (MaxN 133 43) 235) ~ 235) => Bool
+maxNat = True
+
+minNat :: ((MinN 5 9) ~ 5, (MinN 7 4) ~ 4, (MinN 0 8) ~ 0, (MinN 1 0) ~ 0, (MinN 3 3) ~ 3
+          , (MinN (MinN 133 43) 235) ~ 43) => Bool
+minNat = True
+
+allSatisfy :: (AllSatisfy Num (Int ** 1 :- Integer ** 1 :- Double ** 1 :- End)) => Bool
+allSatisfy = True
+
+-- allSatisfyInv :: (AllSatisfy Integral (Double ** 1 :- String ** 1 :- Bool ** 1 :- End)) => Bool
+-- allSatisfyInv = True
+
+class TestConstraint (a :: Nat) (b :: Nat)
+instance (MaxN a b ~ b) => TestConstraint a b
+
+allPairsSatisfy :: (AllPairsSatisfy TestConstraint
+                    (1 ** 1 :- 3 ** 1 :- 5 ** 1 :- End) (2 ** 1 :- 4 ** 1 :- 6 ** 1 :- End)) => Bool
+allPairsSatisfy = True
+
+allPairsSatisfyInv :: (AllPairsSatisfy TestConstraint (4 ** 1 :- End) (1 ** 1 :- End)) => Bool
+allPairsSatisfyInv = True
+
+allPairsSatisfy' :: (AllPairsSatisfy' TestConstraint
+                    (1 :-- 3 :-- 5 :-- None) (2 :-- 4 :-- 6 :-- None)) => Bool
+allPairsSatisfy' = True
+
+allPairsSatisfyInv' :: (AllPairsSatisfy' TestConstraint (2 :-- None) (1 :-- None)) => Bool
+allPairsSatisfyInv' = True
+
+satisfiesAll :: (SatisfiesAll '[Num, Integral, Show] Int) => Bool
+satisfiesAll = True
+
+-- Doesn't work unfortunately
+-- satisfiesAllInv :: (SatisfiesAll '[Num, Integral, Show] Bool) => Bool
+-- satisfiesAllInv = True
+
+allSatisfyAll :: (AllSatisfyAll '[Num, Show] (Double :-- Int :-- Integer :-- None)) => Bool
+allSatisfyAll = True
+
+-- allSatisfyAllInv :: (AllSatisfyAll '[Num, Show] (Bool :-- String :-- Integer :-- None)) => Bool
+-- allSatisfyAllInv = True
+
+
+
+{- MALFORMED TYPE SIGNATURES: should never typecheck
+-- (Comment out line above to expose)
+
+timesReplicateW :: (True ** 23) ~ (True :* (T :: Times 1)) => Bool
+optVectorHeadW :: (Head (True ** 4 :- End)) ~ False => Bool
+vectorHeadW :: (Head' (True :-- None)) ~ False => Bool
+optVectorLastW :: (Last (True ** 4 :- False ** 9 :- End)) ~ True => Bool
+vectorTailW :: (Tail' (True :-- False :-- None)) ~ (True :-- None) => Bool
+vectorInitW :: (Init' (True :-- False :-- None)) ~ (False :-- None) => Bool
+optVectorLengthW :: (Length (True ** 4 :- False ** 9 :- End)) ~ 12 => Bool
+vectorLengthW :: (Length' (True :-- False :-- None)) ~ 3 => Bool
+optVectorAppendW :: ((True ** 5 :- False ** 2 :- End) ++ (False ** 9 :- End))
+                  ~ (True ** 5 :- False ** 11 :- End) => Bool
+vectorAppendW :: ((2 :-- 43 :-- None) ++. None ++. (6 :-- None))
+                ~ (2 :-- 3 :-- 6 :-- None) => Bool
+snocW :: ((2 :-- 5 :-- None) :-| 6) ~ (2 :-- 5 :-- 4 :-- None) => Bool
+repeatVecW :: (True +*+ 3) ~ (True ** 4 :- End) => Bool
+matHConcatW ::
+        (  ((True ** 2 :- End :-- False ** 2 :- End :-- None)
+           +|+ (False ** 5 :- End :-- True ** 5 :- End :-- None))
+           ~ ((True ** 2 :- False ** 5 :- End :-- True ** 2 :- True ** 5 :- End :-- None))
+
+        ,  ((True ** 2 :- End :-- False ** 2 :- End :-- None)
+           +|+ (End :-- None))
+           ~ (True ** 2 :- End :-- False ** 2 :- End :-- None)
+
+        , (None +|+ None) ~ (None :-- None)
+        )
+          => Bool
+alignW ::
+          -- Right fragment
+        ( Align (True ** 2 :- False ** 2 :- End :-- None) (True ** 4 :- End :-- None)
+          ~ '(True ** 2 :- False ** 2 :- End :-- None, True ** 1 :- True ** 3 :- End :-- None)
+          -- Left fragment
+        , Align (False ** 18 :- End :-- None) (True ** 8 :- False ** 10 :- End :-- None)
+          ~ '(False ** 7 :- False ** 11 :- End :-- None, True ** 8 :- False ** 10 :- End :-- None)
+          -- No fragment
+        , Align (True ** 4 :- End :-- None) (False ** 4 :- End :-- None)
+          ~ '(True ** 4 :- End :-- None, True ** 4 :- End :-- None)
+          -- Both fragment
+        , Align (False ** 18 :- True ** 3 :- End :-- None) (True ** 8 :- False ** 13 :- End :-- None)
+          ~ '(False ** 8 :- False ** 9 :- True ** 4 :- End :-- None, True ** 8 :- False ** 10 :- False ** 3 :- End :-- None)
+        ) => Bool
+vecToColMatrixW ::
+        ( (VectorToColMatrix (True :-- False :-- None) 24)
+          ~ (False ** 24 :- End :-- False ** 24 :- End :-- None)
+        , (VectorToColMatrix None 11) ~ (True ** 11 :- End :-- None)
+        ) => Bool
+
+allSatisfyW :: (AllSatisfy Num (Int ** 1 :- Bool ** 1 :- Double ** 1 :- End)) => Bool
+
+
+timesReplicateW = True
+optVectorHeadW = True
+vectorHeadW = True
+optVectorLastW = True
+vectorTailW = True
+vectorInitW = True
+optVectorLengthW = True
+vectorLengthW = True
+optVectorAppendW = True
+vectorAppendW = True
+snocW = True
+repeatVecW = True
+matHConcatW = True
+alignW = True
+vecToColMatrixW = True
+allSatisfyW = True
+
+-- -}
diff --git a/test/TypeSpec.hs b/test/TypeSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/TypeSpec.hs
@@ -0,0 +1,79 @@
+{-# OPTIONS_GHC -fdefer-type-errors #-}
+-- {-# OPTIONS_GHC -w #-}
+{-# LANGUAGE TypeInType, TypeOperators, GADTs, MultiParamTypeClasses, FlexibleInstances #-}
+
+module TypeSpec where
+
+import Test.Hspec
+import GHC.TypeLits
+import Control.Exception (evaluate)
+import Data.Proxy
+import Test.ShouldNotTypecheck (shouldNotTypecheck)
+
+import Mezzo.Model.Types
+
+typeSpec :: Spec
+typeSpec =
+    describe "Mezzo.Model.Types" $ do
+        describe "Harmonic types" $ do
+            it "should convert roots to pitches" $ do
+                rootToPitch `shouldBe` True
+                shouldNotTypecheck rootToPitchInv
+            it "should sharpen roots" $ do
+                sharpen `shouldBe` True
+                shouldNotTypecheck sharpenInv
+            it "should flatten roots" $ do
+                flatten `shouldBe` True
+                shouldNotTypecheck flattenInv
+            it "should make intervals" $ do
+                flatten `shouldBe` True
+
+rootToPitch ::
+        ( (RootToPitch (PitchRoot (Pitch C Natural Oct3)) ~ (Pitch C Natural Oct3))
+        , (RootToPitch (DegreeRoot (Key D Flat MinorMode) IV) ~ (Pitch F Sharp Oct2))
+        ) => Bool
+rootToPitch = True
+
+rootToPitchInv :: Proxy (RootToPitch (DegreeRoot (Key D Flat MinorMode) IV))
+               -> Proxy (Pitch E Natural Oct2)
+rootToPitchInv = id
+
+sharpen :: ( (Sharpen (PitchRoot (Pitch C Natural Oct3))) ~ (PitchRoot (Pitch C Sharp Oct3))
+           , (Sharpen (PitchRoot (Pitch E Natural Oct3))) ~ (PitchRoot (Pitch F Natural Oct3))
+           , (Sharpen (PitchRoot (Pitch C Flat Oct3))) ~ (PitchRoot (Pitch C Natural Oct3))
+           , (Sharpen (PitchRoot (Pitch B Natural Oct3))) ~ (PitchRoot (Pitch C Natural Oct4))
+           , (Sharpen (DegreeRoot (Key F Sharp MinorMode) VI)) ~ (PitchRoot (Pitch D Sharp Oct3))
+           , (Sharpen (DegreeRoot (Key E Sharp MajorMode) VII)) ~ (PitchRoot (Pitch F Natural Oct3))
+           ) => Bool
+sharpen = True
+
+sharpenInv :: Proxy '(Sharpen (PitchRoot (Pitch B Flat Oct5)), Sharpen (DegreeRoot (Key C Flat MajorMode) IV))
+           -> Proxy '(PitchRoot (Pitch C Flat Oct6), PitchRoot (Pitch F Natural Oct3))
+sharpenInv = id
+
+flatten :: ( (Flatten (PitchRoot (Pitch D Natural Oct3))) ~ (PitchRoot (Pitch D Flat Oct3))
+           , (Flatten (PitchRoot (Pitch F Natural Oct3))) ~ (PitchRoot (Pitch E Natural Oct3))
+           , (Flatten (PitchRoot (Pitch C Sharp Oct3))) ~ (PitchRoot (Pitch C Natural Oct3))
+           , (Flatten (PitchRoot (Pitch C Natural Oct3))) ~ (PitchRoot (Pitch B Natural Oct2))
+           , (Flatten (DegreeRoot (Key F Sharp MinorMode) VI)) ~ (PitchRoot (Pitch D Flat Oct3))
+           , (Flatten (DegreeRoot (Key E Sharp MajorMode) VII)) ~ (PitchRoot (Pitch E Flat Oct3))
+           ) => Bool
+flatten = True
+
+flattenInv :: Proxy '(Flatten (PitchRoot (Pitch C Sharp Oct5)), Flatten (DegreeRoot (Key C Flat MajorMode) V))
+           -> Proxy '(PitchRoot (Pitch B Sharp Oct4), PitchRoot (Pitch E Natural Oct3))
+flattenInv = id
+
+makeInterval ::
+            ( (MakeInterval (Pitch C Natural Oct3) (Pitch E Natural Oct3)) ~ (Interval Maj Third)
+            , (MakeInterval (Pitch E Natural Oct3) (Pitch C Natural Oct3)) ~ (Interval Maj Third)
+            , (MakeInterval (Pitch C Natural Oct3) (Pitch B Flat Oct3)) ~ (Interval Min Seventh)
+            , (MakeInterval (Pitch E Sharp Oct3) (Pitch E Sharp Oct3)) ~ (Interval Perf Unison)
+            , (MakeInterval (Pitch E Natural Oct3) (Pitch F Flat Oct3)) ~ (Interval Perf Unison)
+            , (MakeInterval (Pitch E Sharp Oct3) (Pitch F Flat Oct3)) ~ (Interval Min Second)
+            , (MakeInterval (Pitch F Sharp Oct3) (Pitch G Flat Oct3)) ~ (Interval Perf Unison)
+            , (MakeInterval (Pitch C Natural Oct3) (Pitch C Natural Oct4)) ~ (Interval Perf Octave)
+            , (MakeInterval (Pitch E Flat Oct3) (Pitch F Flat Oct4)) ~ Compound
+            , (MakeInterval (Pitch E Sharp Oct3) (Pitch F Flat Oct4)) ~ (Interval Maj Seventh)
+            ) => Bool
+makeInterval = True