1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
|
{-# LANGUAGE DataKinds, PolyKinds, GADTs, TypeOperators, TypeFamilies,
TypeInType #-}
{-# OPTIONS_GHC -fwarn-unticked-promoted-constructors #-}
module RaeBlogPost where
import Data.Kind
-- a Proxy type with an explicit kind
data Proxy k (a :: k) = P
prox :: Proxy * Bool
prox = P
prox2 :: Proxy Bool 'True
prox2 = P
-- implicit kinds still work
data A
data B :: A -> *
data C :: B a -> *
data D :: C b -> *
data E :: D c -> *
-- note that E :: forall (a :: A) (b :: B a) (c :: C b). D c -> *
-- a kind-indexed GADT
data TypeRep (a :: k) where
TInt :: TypeRep Int
TMaybe :: TypeRep Maybe
TApp :: TypeRep a -> TypeRep b -> TypeRep (a b)
zero :: TypeRep a -> a
zero TInt = 0
zero (TApp TMaybe _) = Nothing
data Nat = Zero | Succ Nat
type family a + b where
'Zero + b = b
('Succ a) + b = 'Succ (a + b)
data Vec :: * -> Nat -> * where
Nil :: Vec a 'Zero
(:>) :: a -> Vec a n -> Vec a ('Succ n)
infixr 5 :>
-- promoted GADT, and using + as a "kind family":
type family (x :: Vec a n) ++ (y :: Vec a m) :: Vec a (n + m) where
'Nil ++ y = y
(h ':> t) ++ y = h ':> (t ++ y)
-- datatype that mentions *
data U = Star (*)
| Bool Bool
-- kind synonym
type Monadish = * -> *
class MonadTrans (t :: Monadish -> Monadish) where
lift :: Monad m => m a -> t m a
data Free :: Monadish where
Return :: a -> Free a
Bind :: Free a -> (a -> Free b) -> Free b
-- yes, * really does have type *.
type Star = (* :: (* :: (* :: *)))
|
