Embrace -XTypeInType, add -XStarIsType
[ghc.git] / testsuite / tests / polykinds / PolyKinds10.hs
1 {-# LANGUAGE KindSignatures #-}
2 {-# LANGUAGE TypeOperators #-}
3 {-# LANGUAGE GADTs #-}
4 {-# LANGUAGE TypeFamilies #-}
5 {-# LANGUAGE RankNTypes #-}
6 {-# LANGUAGE ScopedTypeVariables #-}
7 {-# LANGUAGE FlexibleContexts #-}
8 {-# LANGUAGE DataKinds #-}
9
10 module Main where
11
12 import Data.Kind
13
14 -- Type-level peano naturals (value-level too, but we don't use those)
15 data Nat = Ze | Su Nat
16
17 type T0 = Ze
18 type T1 = Su T0
19 type T2 = Su T1
20
21 -- (!) at the type level
22 type family El (n :: Nat) (l :: [Type]) :: Type
23 type instance El Ze (h ': t) = h
24 type instance El (Su n) (h ': t) = El n t
25
26 {-
27 -- The following might be useful, but are not used at the moment
28 -- ($) at the type level (well, not quite ($), in fact...)
29 class Apply (fs :: [Type]) (es :: [Type]) where
30 type ApplyT (fs :: [Type]) (es :: [Type]) :: [Type]
31 apply :: ListV fs -> ListV es -> ListV (ApplyT fs es)
32
33 instance Apply '[] '[] where
34 type ApplyT '[] '[] = '[]
35 apply NilV NilV = NilV
36
37 instance (Apply fs es) => Apply ((e1 -> e2) ': fs) (e1 ': es) where
38 type ApplyT ((e1 -> e2) ': fs) (e1 ': es) = e2 ': ApplyT fs es
39 apply (ConsV f fs) (ConsV e es) = ConsV (f e) (apply fs es)
40 -}
41
42 -- Value mirror for the list kind
43 data ListV :: [Type] -> Type where
44 NilV :: ListV '[]
45 ConsV :: a -> ListV t -> ListV (a ': t)
46
47 data ListV2 :: [[Type]] -> Type where
48 NilV2 :: ListV2 '[]
49 ConsV2 :: ListV a -> ListV2 t -> ListV2 (a ': t)
50
51 listv1 :: ListV (Int ': '[])
52 listv1 = ConsV 3 NilV
53
54 listv2 :: ListV2 ((Int ': '[]) ': '[])
55 listv2 = ConsV2 listv1 NilV2
56
57 --data ListVX :: Maybe -> Type where
58
59 data TripleV :: (Type, Type -> Type, Type) -> Type where
60 TripleV :: a -> c -> TripleV '(a, [], c)
61
62 -- Value mirror for the Nat kind
63 data NatV :: Nat -> Type where
64 ZeW :: NatV Ze
65 SuW :: NatV n -> NatV (Su n)
66
67 -- Generic universe
68 data MultiP x = UNIT
69 | KK x -- wish I could just write Type instead of x
70 | SUM (MultiP x) (MultiP x)
71 | PROD (MultiP x) (MultiP x)
72 | PAR Nat
73 | REC
74
75 -- Universe interpretation
76 data Interprt :: MultiP Type -> [Type] -> Type -> Type where
77 Unit :: Interprt UNIT lp r
78 K :: x -> Interprt (KK x) lp r
79 L :: Interprt a lp r -> Interprt (SUM a b) lp r
80 R :: Interprt b lp r -> Interprt (SUM a b) lp r
81 Prod :: Interprt a lp r -> Interprt b lp r -> Interprt (PROD a b) lp r
82 Par :: NatV n -> El n lp -> Interprt (PAR n) lp r
83 Rec :: r -> Interprt REC lp r
84
85 -- Embedding values into the universe
86 class Generic a where
87 type Rep a :: MultiP Type
88 type Es a :: [Type]
89 from :: a -> Interprt (Rep a) (Es a) a
90 to :: Interprt (Rep a) (Es a) a -> a
91
92 -- Parameter map over the universe
93 class PMap (rep :: MultiP Type) where
94 pmap :: (forall n. NatV n -> El n lp1 -> El n lp2)
95 -> (r -> s) -> Interprt rep lp1 r -> Interprt rep lp2 s
96
97 instance PMap UNIT where
98 pmap _ _ Unit = Unit
99
100 instance PMap (KK x) where
101 pmap _ _ (K x) = K x
102
103 instance (PMap a, PMap b) => PMap (SUM a b) where
104 pmap f g (L x) = L (pmap f g x)
105 pmap f g (R x) = R (pmap f g x)
106
107 instance (PMap a, PMap b) => PMap (PROD a b) where
108 pmap f g (Prod x y) = Prod (pmap f g x) (pmap f g y)
109
110 instance PMap (PAR p) where
111 pmap f _ (Par n p) = Par n (f n p)
112
113 instance PMap REC where
114 pmap _ g (Rec p) = Rec (g p)
115
116 -- User-facing function
117 pmapu :: (Generic a, Generic b, PMap (Rep a), Rep a ~ Rep b)
118 => (forall n. NatV n -> El n (Es a)-> El n (Es b)) -> a -> b
119 pmapu f = to . pmap f (pmapu f). from
120
121
122 -- Example: lists
123 instance Generic [a] where
124 type Rep [a] = SUM UNIT (PROD (PAR T0) REC)
125 type Es [a] = a ': '[]
126 from [] = L Unit
127 from (h:t) = R (Prod (Par ZeW h) (Rec t))
128 to (L Unit) = []
129 to (R (Prod (Par ZeW h) (Rec t))) = h:t
130
131 -- Map on lists: we can define an auxiliary function with the usual type...
132 pmapList :: forall a b. (a -> b) -> [a] -> [b]
133 pmapList f l = pmapu g l where
134 g :: forall n. NatV n -> El n (Es [a]) -> El n (Es [b])
135 g ZeW x = f x
136
137 -- ... or use pmapu directly
138 pmapExample1 :: [String]
139 pmapExample1 = pmapu f [1..10::Int] where
140 f :: forall n. NatV n -> El n (Es [Int]) -> El n (Es [String])
141 f ZeW = show
142
143 -- Example: Either
144 instance Generic (Either a b) where
145 type Rep (Either a b) = SUM (PAR T0) (PAR T1)
146 type Es (Either a b) = a ': b ': '[]
147 from (Left a) = L (Par ZeW a)
148 from (Right b) = R (Par (SuW ZeW) b)
149 to (L (Par ZeW a)) = Left a
150 to (R (Par (SuW ZeW) b)) = Right b
151
152 pmapEither :: forall a1 a2 b1 b2.
153 (a1 -> a2) -> (b1 -> b2) -> Either a1 b1 -> Either a2 b2
154 pmapEither f g = pmapu h where
155 h :: forall n. NatV n -> El n (Es (Either a1 b1)) -> El n (Es (Either a2 b2))
156 h ZeW = f
157 h (SuW ZeW) = g
158
159
160 main = print pmapExample1