Haskell Type Level Nats

Matrix.hs

{-# LANGUAGE GADTs #-}
module Mat where
--import GHC.TypeLits

data Z = Z
data S a = S a

type Zero = Z
type One = S Zero
type Two = S One
type Three = S Two
type Four = S Three

data List s a where
    Nil :: List Z a
    Cons :: a -> List s a -> List (S s) a

ex :: List Four Char
ex = Cons 'a' $ Cons 'b' $ Cons 'c' $ Cons 'd' Nil

append :: List n a -> List m a -> List (m + n) -- 
append = undefined


-- s row, s' col
data Mat s s' a where
    Empty :: Mat Z Z a
    R :: List s (List s' a) -> Mat s s' a

r1 = Cons 1 $ Cons 2 $ Cons 3 Nil
r2 = Cons 4 $ Cons 5 $ Cons 6 Nil

mat :: Mat Two Three Int
mat = R $ Cons r1 $ Cons r2 Nil