blob: 9a0b2fdad047423982fa621887b82fa414e528c0 (
plain)
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
|
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilyDependencies #-}
data family Sing (a :: k)
data SomeSing k where
SomeSing :: Sing (a :: k) -> SomeSing k
withSomeSing :: SomeSing k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing (SomeSing s) f = f s
class SingKind k where
type Demote k = r | r -> k
toSing :: Demote k -> SomeSing k
fromSing :: Sing (a :: k) -> Demote k
data instance Sing (a :: Bool) where
STrue :: Sing 'True
SFalse :: Sing 'False
instance SingKind Bool where
type Demote Bool = Bool
toSing True = SomeSing STrue
toSing False = SomeSing SFalse
fromSing STrue = True
fromSing SFalse = False
class SingI (a :: k) where
sing :: Sing a
instance SingI 'True where
sing = STrue
instance SingI 'False where
sing = SFalse
data instance Sing (a :: Maybe k) where
SJust :: Sing (a :: k) -> Sing ('Just a)
SNothing :: Sing 'Nothing
instance SingI a => SingI ('Just a) where
sing = SJust sing
instance SingI 'Nothing where
sing = SNothing
instance (k ~ Demote k, SingKind k) => SingKind (Maybe k) where
type Demote (Maybe k) = Maybe k
toSing (Just a) = withSomeSing (toSing a) $ SomeSing . SJust
toSing Nothing = SomeSing SNothing
fromSing (SJust a) = Just $ fromSing a
fromSing SNothing = Nothing
data instance Sing (a :: [k]) where
SNil :: Sing '[]
SCons :: Sing (h :: k) -> Sing (t :: [k]) -> Sing (h ': t)
-- Exercise 15.3-i
-- Provide instances of `SingI` for lists.
instance (SingI h, SingI t) => SingI (h ': t) where
sing = SCons sing sing
instance SingI '[] where
sing = SNil
instance (k ~ Demote k, SingKind k) => SingKind [k] where
type Demote [k] = [k]
toSing [] = SomeSing SNil
toSing (h : t) =
withSomeSing (toSing h) $ \sh ->
withSomeSing (toSing t) $ \st ->
SomeSing $ SCons sh st
fromSing SNil = []
fromSing (SCons h t) = fromSing h : fromSing t
|
