1- >{-# LANGUAGE GADTs, ExistentialQuantification#-}
1+ >{-# LANGUAGE GADTs, ExistentialQuantification, DataKinds, KindSignatures, TypeFamilies #-}
22>module Playground where
33
44GADTS
@@ -76,6 +76,10 @@ Package our own functions up with the list
7676>printList (HCons2 (x,s) xs) = putStrLn (s x) >> printList2 xs
7777
7878Phantom Types
79+ 80+ >newtype Lis a = Lis [Int]
81+ 82+ 7983data Ptr a = MkPtr Addr
8084Say we had the following functions
8185peek :: Ptr a -> IO a
@@ -86,3 +90,48 @@ The compiler will protect us from the following
8690 poke ptr (42 :: Int)
8791 f :: Float <- peek ptr
8892
93+ Data Kinds
94+ 95+ Tells us how many paramters a function takes
96+ Int :: *
97+ fmap :: (* -> *) -> * -> *
98+ 99+ >data Nat where
100+ > Zero :: Nat
101+ > Succ :: Nat -> Nat
102+ 103+ Lets us encode the length of a vector into its type
104+ 105+ >data Vec a (l :: Nat) where
106+ > VNil :: Vec a Zero
107+ > VCons :: a -> Vec a n -> Vec a (Succ n )
108+ 109+ for example this wont work
110+ vecL :: Vec Int (Succ (Succ Zero))
111+ vecL = VCons 1 $ VCons 2 $
112+ 113+ This will
114+ 115+ >vecL :: Vec Int (Succ (Succ Zero))
116+ >vecL = VCons 1 $ VCons 2 VNil
117+
118+ Now in order to write useful functions we need the help of the TypeFamilies extension.
119+ Lets write an append function that actually works.
120+
121+ First we declare `Add` which is a `Type Family` or in other words type-level operation
122+
123+ >type family Add (x :: Nat) (y :: Nat) :: Nat
124+ >type instance Add Zero y = y
125+ >type instance Add (Succ x) y = Succ (Add x y)
126+
127+ We now use this Add to increase the kind of Vec to the size of both the Vectors
128+
129+ >append :: Vec a x -> Vec a y -> Vec a (Add x y)
130+ >append (VCons x xs) ys = VCons x $ append xs ys
131+ >append VNil ys = ys
132+ 133+ :t append vecL vecL
134+ append vecL vecL :: Vec Int ('Succ ('Succ ('Succ ('Succ 'Zero))))
135+ 136+ 137+
0 commit comments