some type-level stuff

FinVecs.hs

{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}


module FinVec where

-- simple representation of naturals
-- DataKinds lifts this to the type-level
data Nat = Z | S Nat


-- a FinVec is a list with maximal n items that currently has i items
data FinVec (n :: Nat) (i :: Nat) a where
  Empty :: FinVec n Z a
  Cons  :: a -> FinVec n i a -> FinVec (S n) (S i) a

instance Show a => Show (FinVec n i a) where
  show Empty = "[]"
  show (Cons x xs) = show x ++ " : " ++ show xs


----------------------------------------------------------------------
-- Examples : first one type checks the secons wont

type Three = S (S (S Z))
-- 3 Elements in a List limited to 3max:

threeOfThree :: FinVec Three _ Int
threeOfThree = 1 `Cons` (2 `Cons` (3 `Cons` Empty))

-- one more and it won't TypeCheck
fourOfThree :: FinVec Three _ Int
fourOfThree = 0 `Cons` threeOfThree