blob: 34ff375b58d9f6b4e077b4d8cfdde9f48dc7b3f2 (
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
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
|
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module T15703_aux where
import Data.Kind
import Data.Type.Equality
import GHC.Generics
data family Sing :: forall k. k -> Type
data instance Sing :: forall a b. (a, b) -> Type where
STuple2 :: Sing x -> Sing y -> Sing '(x, y)
data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
type f @@ x = f `Apply` x
infixl 9 @@
newtype instance Sing (f :: k1 ~> k2) =
SLambda { applySing :: forall t. Sing t -> Sing (f @@ t) }
type SingFunction1 f = forall t. Sing t -> Sing (f @@ t)
singFun1 :: forall f. SingFunction1 f -> Sing f
singFun1 f = SLambda f
type SingFunction2 (f :: a1 ~> a2 ~> b) =
forall t1 t2. Sing t1 -> Sing t2 -> Sing (f @@ t1 @@ t2)
singFun2 :: forall f. SingFunction2 f -> Sing f
singFun2 f = SLambda (\x -> singFun1 (f x))
type SingFunction3 (f :: a1 ~> a2 ~> a3 ~> b) =
forall t1 t2 t3.
Sing t1 -> Sing t2 -> Sing t3
-> Sing (f @@ t1 @@ t2 @@ t3)
singFun3 :: forall f. SingFunction3 f -> Sing f
singFun3 f = SLambda (\x -> singFun2 (f x))
(@@) :: forall k1 k2 (f :: k1 ~> k2) (t :: k1). Sing f -> Sing t -> Sing (f @@ t)
(@@) f = applySing f
type family ((f :: b ~> c) :. (g :: a ~> b)) (x :: a) :: c where
(f :. g) x = f @@ (g @@ x)
data (.@#@$) :: forall b c a. (b ~> c) ~> (a ~> b) ~> (a ~> c)
type instance Apply (.@#@$) f = (.@#@$$) f
data (.@#@$$) :: forall b c a. (b ~> c) -> (a ~> b) ~> (a ~> c)
type instance Apply ((.@#@$$) f) g = f .@#@$$$ g
data (.@#@$$$) :: forall b c a. (b ~> c) -> (a ~> b) -> (a ~> c)
type instance Apply (f .@#@$$$ g) x = (f :. g) x
(%.) :: forall b c a (f :: b ~> c) (g :: a ~> b) (x :: a).
Sing f -> Sing g -> Sing x -> Sing ((f :. g) x)
(f %. g) x = f @@ (g @@ x)
type family Id (x :: a) :: a where
Id x = x
data IdSym0 :: forall a. a ~> a
type instance Apply IdSym0 x = Id x
sId :: forall a (x :: a). Sing x -> Sing (Id x)
sId x = x
data instance Sing :: forall i k c (p :: k). K1 i c p -> Type where
SK1 :: Sing x -> Sing ('K1 x)
data instance Sing :: forall k i (c :: Meta) (f :: k -> Type) (p :: k).
M1 i c f p -> Type where
SM1 :: Sing x -> Sing ('M1 x)
data M1Sym0 :: forall k i (c :: Meta) (f :: k -> Type) (p :: k).
f p ~> M1 i c f p
type instance Apply M1Sym0 x = 'M1 x
data instance Sing :: forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
(f :*: g) p -> Type where
(:%*:) :: Sing x -> Sing y -> Sing (x ':*: y)
data instance Sing :: forall p. Par1 p -> Type where
SPar1 :: Sing x -> Sing ('Par1 x)
class PGeneric1 (f :: k -> Type) where
type From1 (z :: f a) :: Rep1 f a
type To1 (z :: Rep1 f a) :: f a
class SGeneric1 (f :: k -> Type) where
sFrom1 :: forall (a :: k) (z :: f a). Sing z -> Sing (From1 z)
sTo1 :: forall (a :: k) (r :: Rep1 f a). Sing r -> Sing (To1 r :: f a)
class (PGeneric1 f, SGeneric1 f) => VGeneric1 (f :: k -> Type) where
sTof1 :: forall (a :: k) (z :: f a). Sing z -> To1 (From1 z) :~: z
sFot1 :: forall (a :: k) (r :: Rep1 f a). Sing r -> From1 (To1 r :: f a) :~: r
instance PGeneric1 ((,) a) where
type From1 '(x, y) = 'M1 ('M1 ('M1 ('K1 x) ':*: 'M1 ('Par1 y)))
type To1 ('M1 ('M1 ('M1 ('K1 x) ':*: 'M1 ('Par1 y)))) = '(x, y)
instance SGeneric1 ((,) a) where
sFrom1 (STuple2 x y) = SM1 (SM1 (SM1 (SK1 x) :%*: SM1 (SPar1 y)))
sTo1 (SM1 (SM1 (SM1 (SK1 x) :%*: SM1 (SPar1 y)))) = STuple2 x y
instance VGeneric1 ((,) a) where
sTof1 STuple2{} = Refl
sFot1 (SM1 (SM1 (SM1 SK1{} :%*: SM1 SPar1{}))) = Refl
class PSemigroup a where
type (x :: a) <> (y :: a) :: a
class SSemigroup a where
(%<>) :: forall (x :: a) (y :: a).
Sing x -> Sing y -> Sing (x <> y)
class (PSemigroup a, SSemigroup a) => VSemigroup a where
semigroupAssociative :: forall (x :: a) (y :: a) (z :: a).
Sing x -> Sing y -> Sing z
-> (x <> (y <> z)) :~: ((x <> y) <> z)
class PSemigroup a => PMonoid a where
type Mempty :: a
class SSemigroup a => SMonoid a where
sMempty :: Sing (Mempty :: a)
class (PMonoid a, SMonoid a, VSemigroup a) => VMonoid a where
monoidLeftIdentity :: forall (x :: a).
Sing x -> (Mempty <> x) :~: x
monoidRightIdentity :: forall (x :: a).
Sing x -> (x <> Mempty) :~: x
|
