ghc type nats

Matrix.hs

{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE DeriveFunctor       #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE KindSignatures      #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications    #-}
{-# LANGUAGE TypeOperators       #-}
module MadLit where
import GHC.TypeNats
import Prelude hiding (Nat, length)
import           Data.Proxy


data List a = Nil | Cons a (List a) deriving Functor

length Nil = 0
length (Cons _ xs) = 1 + length xs

-- Indexed List
data SafeList (n :: Nat) a = MkList { getList :: List a}

mkList :: forall n a. KnownNat n => List a -> SafeList n a -- could use Maybe to fail gracefulls
mkList xs | length xs == fromIntegral (natVal (Proxy @n)) = MkList xs
mkList _ = undefined


test :: SafeList 3 Int
test = mkList (Cons 1 (Cons 2 (Cons 3 Nil)))

-- Indexed Matrix 

data SafeMat (n :: Nat) (m :: Nat) a = MkMat {getMat :: List (List a)}

mkSafeMat :: forall n m a. (KnownNat n, KnownNat m) => SafeList n (SafeList m a) -> SafeMat n m a
mkSafeMat mat = MkMat $ fmap getList (getList mat)


sr1 :: SafeList 3 Int
sr1 = mkList $ Cons 1 $ Cons 2 $ Cons 3 Nil
sr2 :: SafeList 3 Int
sr2 = mkList $ Cons 4 $ Cons 5 $ Cons 6 Nil

mat :: SafeMat 2 3 Int
mat = mkSafeMat $ mkList $ Cons sr1 $ Cons sr2 Nil