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