]> Git — Sourcephile - haskell/symantic-base.git/blob - src/Symantic/ADT.hs
impl: fix deprecated `StarIsType`
[haskell/symantic-base.git] / src / Symantic / ADT.hs
1 {-# LANGUAGE AllowAmbiguousTypes #-}
2 {-# LANGUAGE DataKinds #-}
3 {-# LANGUAGE ConstraintKinds #-}
4 {-# LANGUAGE EmptyCase #-}
5 {-# LANGUAGE PolyKinds #-}
6 {-# LANGUAGE UndecidableInstances #-}
7 -- | EOT (Either of Tuples) to/from ADT (Algebraic Data Type).
8 -- to produce or consume custom ADT with @('<:>')@ and @('<+>')@.
9 --
10 -- This is like what is done in @generic-sop@:
11 -- https://hackage.haskell.org/package/generics-sop-0.5.1.0/docs/src/Generics.SOP.GGP.html#gSumFrom
12 -- but using directly 'Either' and 'Tuples'
13 -- instead of passing by the intermediary GADTs @NP@ and @NS@.
14 module Symantic.ADT where
15
16 import Data.Either (Either(..))
17 import Data.Void (Void, absurd)
18 import Data.Function (($), (.), id, const)
19 import GHC.Generics as Generics
20
21 -- * Type family 'EoT'
22 -- Return an 'Either' of 'Tuples' from the given 'ADT',
23 -- matching the nesting occuring when using @('<:>')@ and ('<+>')@
24 -- and their associativity and precedence,
25 -- with no parenthesis messing around.
26 type family EoT (adt :: [[*]]) :: * where
27 -- This is 'absurd'
28 EoT '[] = Void
29 -- There Is No Alternative
30 EoT '[ ps ] = Tuples ps
31 -- The right associativity of @('<+>')@
32 -- puts leaves on 'Left' and nodes on 'Right'
33 EoT (ps ': ss) = Either (Tuples ps) (EoT ss)
34
35 -- * Type family 'Tuples'
36 -- | Return the type of 'snd'-nested 2-tuples
37 -- from the given list of types.
38 type family Tuples (as :: [*]) :: (r :: *) where
39 Tuples '[] = ()
40 Tuples '[a] = a
41 Tuples (a ': rest) = (a, Tuples rest)
42
43 -- * Type 'ADT'
44 -- | Normalized type-level representation of an Algebraic Data Type.
45 type ADT (adt :: *) = ListOfRepSums (Rep adt) '[]
46
47 -- ** Type family 'ListOfRepSums'
48 -- | Collect the alternatives in a continuation passing-style.
49 type family ListOfRepSums (a :: * -> *) (ss :: [[*]]) :: [[*]]
50 type instance ListOfRepSums (a:+:b) ss = ListOfRepSums a (ListOfRepSums b ss)
51 -- | Meta-information for datatypes
52 type instance ListOfRepSums (M1 D _c a) ss = ListOfRepSums a ss
53 -- | Meta-information for constructors
54 type instance ListOfRepSums (M1 C _c a) ss = ListOfRepProducts a '[] ': ss
55 -- | Empty datatypes
56 type instance ListOfRepSums V1 ss = ss
57
58 -- ** Type family 'ListOfRepProducts'
59 -- | Collect the records in a continuation passing-style.
60 type family ListOfRepProducts (a :: * -> *) (ps :: [*]) :: [*]
61 type instance ListOfRepProducts (a:*:b) ps = ListOfRepProducts a (ListOfRepProducts b ps)
62 -- | Meta-information for record selectors
63 type instance ListOfRepProducts (M1 S _c a) ps = TypeOfRepField a ': ps
64 -- | Constructor without fields
65 type instance ListOfRepProducts U1 ps = ps
66
67 -- ** Type family 'TypeOfRepField'
68 type family TypeOfRepField (a :: * -> *) :: *
69 type instance TypeOfRepField (K1 _i a) = a
70
71 -- * Class 'RepOfEoT'
72 type RepOfEoT a = RepOfEithers (Rep a) '[]
73
74 -- | Morph the 'Either' of 'Tuples' corresponding to an 'ADT'
75 -- into a constructor of this 'ADT'.
76 -- This is the reverse of 'eotOfadt'.
77 adtOfeot :: Generic a => RepOfEoT a => EoT (ADT a) -> a
78 adtOfeot eot = Generics.to $ repOfEithers @_ @'[] eot id absurd
79
80 -- ** Class 'RepOfEithers'
81 class RepOfEithers (a :: * -> *) ss where
82 -- | Parse the 'Either' (list-like) binary tree of 'EoT'
83 -- into the @(':+:')@ (balanced) binary tree of 'Rep',
84 -- using continuation passing-style for performance.
85 repOfEithers ::
86 EoT (ListOfRepSums a ss) ->
87 -- the 'a' 'Rep' is the current alternative in the 'EoT'
88 (a x -> r) ->
89 -- the 'a' 'Rep' is a following alternative in the 'EoT'
90 (EoT ss -> r) ->
91 r
92 instance (RepOfEithers a (ListOfRepSums b ss), RepOfEithers b ss) => RepOfEithers (a:+:b) ss where
93 repOfEithers eot ok ko =
94 -- try to parse 'a' on the current 'eot'
95 repOfEithers @a @(ListOfRepSums b ss) eot
96 (ok . L1)
97 (\next ->
98 -- parsing 'a' failed
99 -- try to parse 'b' on the 'Right' of the current 'eot'
100 repOfEithers @b @ss next
101 (ok . R1)
102 ko -- parsing 'b' failed: backtrack
103 )
104 instance RepOfEithers a ss => RepOfEithers (M1 D c a) ss where
105 repOfEithers eot ok = repOfEithers @a @ss eot (ok . M1)
106 instance RepOfTuples a '[] => RepOfEithers (M1 C c a) (ps ': ss) where
107 repOfEithers eot ok ko =
108 case eot of
109 -- 'EoT' is a leaf, and 'Rep' too: parsing succeeds
110 Left ts -> ok $ M1 $ repOfTuples @a @'[] ts const
111 -- 'EoT' is a node, but 'Rep' is a leaf: parsing fails
112 Right ss -> ko ss
113 instance RepOfTuples a '[] => RepOfEithers (M1 C c a) '[] where
114 repOfEithers eot ok _ko = ok $ M1 $ repOfTuples @_ @'[] eot const
115 instance RepOfEithers V1 ss where
116 repOfEithers eot _ok ko = ko eot
117
118 -- ** Class 'RepOfTuples'
119 class RepOfTuples (a :: * -> *) (xs::[*]) where
120 -- | Parse the 'Tuples' (list-like) binary tree of 'EoT'
121 -- into the @(':*:')@ (balanced) binary tree of 'Rep',
122 -- using continuation passing-style for performance.
123 repOfTuples ::
124 Tuples (ListOfRepProducts a xs) ->
125 (a x -> Tuples xs -> r) -> r
126 instance (RepOfTuples a (ListOfRepProducts b ps), RepOfTuples b ps) => RepOfTuples (a:*:b) ps where
127 repOfTuples ts k =
128 -- uncons 'a'
129 repOfTuples @a @(ListOfRepProducts b ps) ts
130 (\a ts' ->
131 -- uncons 'b'
132 repOfTuples @b @ps ts'
133 (\b -> k (a:*:b)))
134 instance RepOfField a => RepOfTuples (M1 S c a) (p ': ps) where
135 repOfTuples (a, ts) k = k (M1 (repOfField a)) ts
136 instance RepOfField a => RepOfTuples (M1 S c a) '[] where
137 repOfTuples a k = k (M1 (repOfField a)) ()
138 instance RepOfTuples U1 ps where
139 repOfTuples ts k = k U1 ts
140
141 -- ** Class 'RepOfField'
142 class RepOfField (a :: * -> *) where
143 repOfField :: TypeOfRepField a -> a x
144 instance RepOfField (K1 i a) where
145 repOfField = K1
146
147 -- * Class 'EoTOfRep'
148 type EoTOfRep a = EithersOfRep (Rep a) '[]
149
150 -- | Morph the constructor of an 'ADT'
151 -- into the corresponding 'Either' of 'Tuples' of this 'ADT'.
152 -- This is the reverse of 'adtOfeot'.
153 eotOfadt :: Generic a => EoTOfRep a => a -> EoT (ADT a)
154 eotOfadt = eithersOfRepL @_ @'[] . Generics.from
155
156 -- ** Class 'EithersOfRep'
157 class EithersOfRep (a :: * -> *) ss where
158 eithersOfRepL :: a x -> EoT (ListOfRepSums a ss)
159 eithersOfRepR :: EoT ss -> EoT (ListOfRepSums a ss)
160 instance (EithersOfRep a (ListOfRepSums b ss), EithersOfRep b ss) =>
161 EithersOfRep (a:+:b) ss where
162 eithersOfRepL = \case
163 L1 a -> eithersOfRepL @a @(ListOfRepSums b ss) a
164 R1 b -> eithersOfRepR @a @(ListOfRepSums b ss) (eithersOfRepL @b @ss b)
165 eithersOfRepR ss = eithersOfRepR @a @(ListOfRepSums b ss) (eithersOfRepR @b @ss ss)
166 instance EithersOfRep a ss => EithersOfRep (M1 D c a) ss where
167 eithersOfRepL (M1 a) = eithersOfRepL @a @ss a
168 eithersOfRepR = eithersOfRepR @a @ss
169 instance TuplesOfRep a '[] => EithersOfRep (M1 C c a) '[] where
170 eithersOfRepL (M1 a) = tuplesOfRep @_ @'[] a ()
171 eithersOfRepR = absurd
172 instance TuplesOfRep a '[] => EithersOfRep (M1 C c a) (ps ': ss) where
173 eithersOfRepL (M1 a) = Left $ tuplesOfRep @_ @'[] a ()
174 eithersOfRepR = Right
175 instance EithersOfRep V1 ss where
176 eithersOfRepL = \case {}
177 eithersOfRepR = id
178
179 -- ** Class 'TuplesOfRep'
180 class TuplesOfRep (a :: * -> *) (ps::[*]) where
181 tuplesOfRep :: a x -> Tuples ps -> Tuples (ListOfRepProducts a ps)
182 instance (TuplesOfRep a (ListOfRepProducts b ps), TuplesOfRep b ps) => TuplesOfRep (a:*:b) ps where
183 tuplesOfRep (a:*:b) ps =
184 tuplesOfRep @a @(ListOfRepProducts b ps) a
185 (tuplesOfRep @b @ps b ps)
186 instance TuplesOfRep U1 ps where
187 tuplesOfRep U1 xs = xs
188 instance FieldOfRep a => TuplesOfRep (M1 S c a) (x ': ps) where
189 tuplesOfRep (M1 a) xs = (fieldOfRep a, xs)
190 instance FieldOfRep a => TuplesOfRep (M1 S c a) '[] where
191 tuplesOfRep (M1 a) _xs = fieldOfRep a
192
193 -- ** Class 'FieldOfRep'
194 class FieldOfRep (a :: * -> *) where
195 fieldOfRep :: a x -> TypeOfRepField a
196 instance FieldOfRep (K1 i a) where
197 fieldOfRep (K1 a) = a