22>module Playground where
33
44GADTS
5+ 56>data Expr a where
67> Add :: Num a => Expr a -> Expr a -> Expr a
78> Eq :: Eq a => Expr a -> Expr a -> Expr Bool
89
910We can use GADT's to provide run-time information about whether or not the list is empty
1011If the list contains 'Z' we know it is empty
12+ 1113>data Z
1214>data S n
13- 1415>data List a n where
1516> Nil :: List a Z
1617> Cons :: a -> List a b -> List a (S b )
@@ -19,6 +20,7 @@ By using the fact that the list must be non-empty we can get the help of the typ
1920let emptylist = Nil
2021safeHead emptyList
2122This will return a type error as 'List a Z' will not match the expected 'List a (S n)'
23+ 2224>safeHead :: List a (S n) -> a
2325>safeHead (Cons a _ ) = a
2426
@@ -33,28 +35,28 @@ Existential Quantification
3335
3436Useless
3537We dont know anything about the types, so we cannot perform any computations
38+ 3639>data HList = HNil
3740> . HCons a HList
41+ 3842Useful
3943Constrain it to the class Showable, which provides useful functions that can used accross all types in the list
44+ 4045>data HList1 = HNil1
4146> . Show a => HCons1 a HList1
4247
4348>printList1 :: HList1 -> IO ()
4449>printList1 HNil1 = return ()
45- >printList1 (HCons1 x xs) = do
46- > putStrLn $ show x
47- >
50+ >printList1 (HCons1 x xs) = putStrLn (show x) >> printList1 xs
4851
4952Package our own functions up with the list
53+ 5054>data HList2 = HNil2
5155> . HCons2 (a,a -> String ) HList2
5256
5357>printList2 :: HList2 -> IO ()
5458>printList2 HNil2 = return ()
55- >printList (HCons2 (x,s) xs) = do
56- > putStrLn $ s x
57- >
59+ >printList (HCons2 (x,s) xs) = putStrLn (s x) >> printList2 xs
5860
5961Phantom Types
6062data Ptr a = MkPtr Addr
0 commit comments