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
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
|
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE DataKinds #-}
module Main where
import Data.Kind
-- Type-level peano naturals (value-level too, but we don't use those)
data Nat = Ze | Su Nat
type T0 = Ze
type T1 = Su T0
type T2 = Su T1
-- (!) at the type level
type family El (n :: Nat) (l :: [Type]) :: Type
type instance El Ze (h ': t) = h
type instance El (Su n) (h ': t) = El n t
{-
-- The following might be useful, but are not used at the moment
-- ($) at the type level (well, not quite ($), in fact...)
class Apply (fs :: [Type]) (es :: [Type]) where
type ApplyT (fs :: [Type]) (es :: [Type]) :: [Type]
apply :: ListV fs -> ListV es -> ListV (ApplyT fs es)
instance Apply '[] '[] where
type ApplyT '[] '[] = '[]
apply NilV NilV = NilV
instance (Apply fs es) => Apply ((e1 -> e2) ': fs) (e1 ': es) where
type ApplyT ((e1 -> e2) ': fs) (e1 ': es) = e2 ': ApplyT fs es
apply (ConsV f fs) (ConsV e es) = ConsV (f e) (apply fs es)
-}
-- Value mirror for the list kind
data ListV :: [Type] -> Type where
NilV :: ListV '[]
ConsV :: a -> ListV t -> ListV (a ': t)
data ListV2 :: [[Type]] -> Type where
NilV2 :: ListV2 '[]
ConsV2 :: ListV a -> ListV2 t -> ListV2 (a ': t)
listv1 :: ListV (Int ': '[])
listv1 = ConsV 3 NilV
listv2 :: ListV2 ((Int ': '[]) ': '[])
listv2 = ConsV2 listv1 NilV2
--data ListVX :: Maybe -> Type where
data TripleV :: (Type, Type -> Type, Type) -> Type where
TripleV :: a -> c -> TripleV '(a, [], c)
-- Value mirror for the Nat kind
data NatV :: Nat -> Type where
ZeW :: NatV Ze
SuW :: NatV n -> NatV (Su n)
-- Generic universe
data MultiP x = UNIT
| KK x -- wish I could just write Type instead of x
| SUM (MultiP x) (MultiP x)
| PROD (MultiP x) (MultiP x)
| PAR Nat
| REC
-- Universe interpretation
data Interprt :: MultiP Type -> [Type] -> Type -> Type where
Unit :: Interprt UNIT lp r
K :: x -> Interprt (KK x) lp r
L :: Interprt a lp r -> Interprt (SUM a b) lp r
R :: Interprt b lp r -> Interprt (SUM a b) lp r
Prod :: Interprt a lp r -> Interprt b lp r -> Interprt (PROD a b) lp r
Par :: NatV n -> El n lp -> Interprt (PAR n) lp r
Rec :: r -> Interprt REC lp r
-- Embedding values into the universe
class Generic a where
type Rep a :: MultiP Type
type Es a :: [Type]
from :: a -> Interprt (Rep a) (Es a) a
to :: Interprt (Rep a) (Es a) a -> a
-- Parameter map over the universe
class PMap (rep :: MultiP Type) where
pmap :: (forall n. NatV n -> El n lp1 -> El n lp2)
-> (r -> s) -> Interprt rep lp1 r -> Interprt rep lp2 s
instance PMap UNIT where
pmap _ _ Unit = Unit
instance PMap (KK x) where
pmap _ _ (K x) = K x
instance (PMap a, PMap b) => PMap (SUM a b) where
pmap f g (L x) = L (pmap f g x)
pmap f g (R x) = R (pmap f g x)
instance (PMap a, PMap b) => PMap (PROD a b) where
pmap f g (Prod x y) = Prod (pmap f g x) (pmap f g y)
instance PMap (PAR p) where
pmap f _ (Par n p) = Par n (f n p)
instance PMap REC where
pmap _ g (Rec p) = Rec (g p)
-- User-facing function
pmapu :: (Generic a, Generic b, PMap (Rep a), Rep a ~ Rep b)
=> (forall n. NatV n -> El n (Es a)-> El n (Es b)) -> a -> b
pmapu f = to . pmap f (pmapu f). from
-- Example: lists
instance Generic [a] where
type Rep [a] = SUM UNIT (PROD (PAR T0) REC)
type Es [a] = a ': '[]
from [] = L Unit
from (h:t) = R (Prod (Par ZeW h) (Rec t))
to (L Unit) = []
to (R (Prod (Par ZeW h) (Rec t))) = h:t
-- Map on lists: we can define an auxiliary function with the usual type...
pmapList :: forall a b. (a -> b) -> [a] -> [b]
pmapList f l = pmapu g l where
g :: forall n. NatV n -> El n (Es [a]) -> El n (Es [b])
g ZeW x = f x
-- ... or use pmapu directly
pmapExample1 :: [String]
pmapExample1 = pmapu f [1..10::Int] where
f :: forall n. NatV n -> El n (Es [Int]) -> El n (Es [String])
f ZeW = show
-- Example: Either
instance Generic (Either a b) where
type Rep (Either a b) = SUM (PAR T0) (PAR T1)
type Es (Either a b) = a ': b ': '[]
from (Left a) = L (Par ZeW a)
from (Right b) = R (Par (SuW ZeW) b)
to (L (Par ZeW a)) = Left a
to (R (Par (SuW ZeW) b)) = Right b
pmapEither :: forall a1 a2 b1 b2.
(a1 -> a2) -> (b1 -> b2) -> Either a1 b1 -> Either a2 b2
pmapEither f g = pmapu h where
h :: forall n. NatV n -> El n (Es (Either a1 b1)) -> El n (Es (Either a2 b2))
h ZeW = f
h (SuW ZeW) = g
main = print pmapExample1
|
