blob: 4904234524ab7f3397c5fac36fefb8cbae3adffc (
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
75
76
77
78
79
80
81
82
|
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module T18747A where
import Data.Kind
import Data.Type.Equality
type family Sing :: k -> Type
data SomeSing :: Type -> Type where
SomeSing :: Sing (a :: k) -> SomeSing k
data SList :: forall a. [a] -> Type where
SNil :: SList '[]
SCons :: Sing x -> Sing xs -> SList (x:xs)
type instance Sing = SList
data Univ = U1 | K1 Type | Sum Univ Univ | Product Univ Univ
data SUniv :: Univ -> Type where
SU1 :: SUniv U1
SK1 :: Sing c -> SUniv (K1 c)
SSum :: Sing a -> Sing b -> SUniv (Sum a b)
SProduct :: Sing a -> Sing b -> SUniv (Product a b)
type instance Sing = SUniv
data In :: Univ -> Type where
MkU1 :: In U1
MkK1 :: c -> In (K1 c)
L1 :: In a -> In (Sum a b)
R1 :: In b -> In (Sum a b)
MkProduct :: In a -> In b -> In (Product a b)
data SIn :: forall u. In u -> Type where
SMkU1 :: SIn MkU1
SMkK1 :: Sing c -> SIn (MkK1 c)
SL1 :: Sing a -> SIn (L1 a)
SR1 :: Sing b -> SIn (R1 b)
SMkProduct :: Sing a -> Sing b -> SIn (MkProduct a b)
type instance Sing = SIn
class Generic (a :: Type) where
type Rep a :: Univ
from :: a -> In (Rep a)
to :: In (Rep a) -> a
class PGeneric (a :: Type) where
type PFrom (x :: a) :: In (Rep a)
type PTo (x :: In (Rep a)) :: a
class SGeneric k where
sFrom :: forall (a :: k). Sing a -> Sing (PFrom a)
sTo :: forall (a :: In (Rep k)). Sing a -> Sing (PTo a :: k)
sTof :: forall (a :: k). Sing a -> PTo (PFrom a) :~: a
sFot :: forall (a :: In (Rep k)). Sing a -> PFrom (PTo a :: k) :~: a
instance Generic [a] where
type Rep [a] = Sum U1 (Product (K1 a) (K1 [a]))
from [] = L1 MkU1
from (x:xs) = R1 (MkProduct (MkK1 x) (MkK1 xs))
to (L1 MkU1) = []
to (R1 (MkProduct (MkK1 x) (MkK1 xs))) = x:xs
instance PGeneric [a] where
type PFrom '[] = L1 MkU1
type PFrom (x:xs) = R1 (MkProduct (MkK1 x) (MkK1 xs))
type PTo (L1 MkU1) = '[]
type PTo (R1 (MkProduct (MkK1 x) (MkK1 xs))) = x:xs
instance SGeneric [a] where
sFrom SNil = SL1 SMkU1
sFrom (SCons x xs) = SR1 (SMkProduct (SMkK1 x) (SMkK1 xs))
sTo (SL1 SMkU1) = SNil
sTo (SR1 (SMkProduct (SMkK1 x) (SMkK1 xs))) = SCons x xs
sTof SNil = Refl
sTof SCons{} = Refl
sFot (SL1 SMkU1) = Refl
sFot (SR1 (SMkProduct SMkK1{} SMkK1{})) = Refl
|
