]> Git — Sourcephile - haskell/symantic-base.git/blob - src/Symantic/Semantics/Data.hs
iface: add interpreter `LetInserter`
[haskell/symantic-base.git] / src / Symantic / Semantics / Data.hs
1 {-# LANGUAGE ConstraintKinds #-}
2 -- For Semantic
3 {-# LANGUAGE DataKinds #-}
4 {-# LANGUAGE GADTs #-}
5 {-# LANGUAGE PatternSynonyms #-}
6 {-# LANGUAGE RankNTypes #-}
7 {-# LANGUAGE ViewPatterns #-}
8
9 -- | This module provides the intermediate semantic 'SomeData'
10 -- which interprets combinators as data constructors.
11 -- This enables to pattern-match on combinators
12 -- while keeping their extensibility.
13 module Symantic.Semantics.Data where
14
15 import Data.Bool (Bool)
16 import Data.Either (Either)
17 import Data.Eq qualified as Eq
18 import Data.Function qualified as Fun
19 import Data.Maybe (Maybe)
20 import Data.Maybe qualified as Maybe
21 import Data.Semigroup (Semigroup)
22 import Type.Reflection (Typeable, eqTypeRep, typeRep, (:~~:) (..))
23
24 import Symantic.Syntaxes.Classes
25 import Symantic.Syntaxes.Derive
26
27 -- * Type 'SomeData'
28 data SomeData sem a
29 = forall syn.
30 ( Derivable (Data syn sem)
31 , Typeable syn
32 ) =>
33 SomeData (Data syn sem a)
34
35 type instance Derived (SomeData sem) = sem
36 instance Derivable (SomeData sem) where
37 derive (SomeData x) = derive x
38
39 -- ** Type 'Data'
40
41 -- TODO: neither data families nor data instances
42 -- can have phantom roles with GHC-9's RoleAnnotations,
43 -- hence 'Data.Coerce.coerce' cannot be used on them for now.
44 -- https://gitlab.haskell.org/ghc/ghc/-/issues/8177
45 -- https://gitlab.haskell.org/ghc/ghc/-/wikis/roles#proposal-roles-for-type-families
46 data family Data (syn :: Syntax) :: Semantic -> Semantic
47 type instance Derived (Data syn sem) = sem
48
49 -- | Convenient utility to pattern-match a 'SomeData'.
50 pattern Data :: Typeable syn => Data syn sem a -> SomeData sem a
51 pattern Data x <- (unSomeData -> Maybe.Just x)
52
53 -- | @(unSomeData sd :: 'Maybe' ('Data' syn sem a))@
54 -- extract the data-constructor from the given 'SomeData' @(sd)@
55 -- iif. it belongs to the @('Data' syn sem a)@ data-instance.
56 unSomeData ::
57 forall syn sem a.
58 Typeable syn =>
59 SomeData sem a ->
60 Maybe (Data syn sem a)
61 unSomeData (SomeData (constr :: Data actualSyn sem a)) =
62 case typeRep @syn `eqTypeRep` typeRep @actualSyn of
63 Maybe.Just HRefl -> Maybe.Just constr
64 Maybe.Nothing -> Maybe.Nothing
65
66 -- Abstractable
67 data instance Data Abstractable sem a where
68 Lam :: (SomeData sem a -> SomeData sem b) -> Data Abstractable sem (a -> b)
69 instance (Abstractable sem, Varable sem) => Derivable (Data Abstractable sem) where
70 derive = \case
71 Lam f -> lam (\x -> derive (f (SomeData (Var x))))
72 instance (Abstractable sem, Varable sem) => Abstractable (SomeData sem) where
73 lam f = SomeData (Lam f)
74
75 -- Abstractable1
76 data instance Data Abstractable1 sem a where
77 Lam1 :: (SomeData sem a -> SomeData sem b) -> Data Abstractable1 sem (a -> b)
78 instance (Abstractable1 sem, Varable sem) => Derivable (Data Abstractable1 sem) where
79 derive = \case
80 Lam1 f -> lam1 (\x -> derive (f (SomeData (Var x))))
81 instance (Abstractable1 sem, Varable sem) => Abstractable1 (SomeData sem) where
82 lam1 f = SomeData (Lam1 f)
83
84 -- Varable
85 data instance Data Varable sem a where
86 Var :: sem a -> Data Varable sem a
87 instance Varable sem => Derivable (Data Varable sem) where
88 derive = \case
89 Var x -> var x
90 instance Varable sem => Varable (SomeData sem) where
91 var = Fun.id
92
93 -- | Beta-reduce the left-most outer-most lambda abstraction (aka. normal-order reduction),
94 -- but to avoid duplication of work, only those manually marked
95 -- as using their variable at most once.
96 --
97 -- DOC: Demonstrating Lambda Calculus Reduction, Peter Sestoft, 2001,
98 -- https://www.itu.dk/people/sestoft/papers/sestoft-lamreduce.pdf
99 normalOrderReduction ::
100 forall sem a.
101 Abstractable sem =>
102 Abstractable1 sem =>
103 Instantiable sem =>
104 Varable sem =>
105 IfThenElseable sem =>
106 SomeData sem a ->
107 SomeData sem a
108 normalOrderReduction = nor
109 where
110 nor :: SomeData sem b -> SomeData sem b
111 nor = expand Fun.$ \case
112 Data (Lam f) -> lam (nor Fun.. f)
113 Data (Lam1 f) -> lam1 (nor Fun.. f)
114 Data (x :@ y) -> case whnf x of
115 Data (Lam1 f) -> nor (f y)
116 x' -> nor x' .@ nor y
117 x -> x
118
119 whnf :: SomeData sem b -> SomeData sem b
120 whnf = expand Fun.$ \case
121 Data (x :@ y) -> case whnf x of
122 Data (Lam1 f) -> whnf (f y)
123 x' -> x' .@ y
124 x -> x
125
126 expand :: (SomeData sem b -> SomeData sem b) -> SomeData sem b -> SomeData sem b
127 expand fct sd = fct Fun.$ case unSomeData sd of
128 Maybe.Just d -> case d of
129 Ap -> lam1 (\abc -> lam1 (\ab -> lam1 (\a -> abc .@ a .@ (ab .@ a))))
130 Const -> lam1 (\x -> lam1 (\_y -> x))
131 Id -> lam1 Fun.id
132 (:.) -> lam1 (\f -> lam1 (\g -> lam1 (\x -> f .@ (g .@ x))))
133 Flip -> lam1 (\f -> lam1 (\x -> lam1 (\y -> f .@ y .@ x)))
134 (:$) -> lam1 (\f -> lam1 (f .@))
135 Maybe.Nothing ->
136 case sd of
137 Data (IfThenElse test ok ko) ->
138 case nor test of
139 Data (Constant b :: Data (Constantable Bool) sem Bool) ->
140 if b then nor ok else nor ko
141 tst -> ifThenElse tst (nor ok) (nor ko)
142 _ -> sd
143
144 -- Instantiable
145 data instance Data Instantiable sem a where
146 (:@) :: SomeData sem (a -> b) -> SomeData sem a -> Data Instantiable sem b
147 instance Instantiable sem => Derivable (Data Instantiable sem) where
148 derive = \case
149 f :@ x -> derive f .@ derive x
150 instance Instantiable sem => Instantiable (SomeData sem) where
151 f .@ x = SomeData (f :@ x)
152
153 -- Unabstractable
154 data instance Data Unabstractable sem a where
155 Ap :: Data Unabstractable sem ((a -> b -> c) -> (a -> b) -> a -> c)
156 Const :: Data Unabstractable sem (a -> b -> a)
157 Id :: Data Unabstractable sem (a -> a)
158 (:.) :: Data Unabstractable sem ((b -> c) -> (a -> b) -> a -> c)
159 Flip :: Data Unabstractable sem ((a -> b -> c) -> b -> a -> c)
160 (:$) :: Data Unabstractable sem ((a -> b) -> a -> b)
161 instance Unabstractable sem => Derivable (Data Unabstractable sem) where
162 derive = \case
163 Ap -> ap
164 Const -> const
165 Id -> id
166 (:.) -> (.)
167 Flip -> flip
168 (:$) -> ($)
169 instance Unabstractable sem => Unabstractable (SomeData sem) where
170 ap = SomeData Ap
171 const = SomeData Const
172 id = SomeData Id
173 (.) = SomeData (:.)
174 flip = SomeData Flip
175 ($) = SomeData (:$)
176
177 -- Anythingable
178 data instance Data Anythingable sem a where
179 Anything :: sem a -> Data Anythingable sem a
180 instance
181 ( Anythingable sem
182 ) =>
183 Derivable (Data Anythingable sem)
184 where
185 derive = \case
186 Anything x -> anything x
187 instance Anythingable (SomeData sem)
188 instance Anythingable (Data Anythingable sem)
189
190 -- Bottomable
191 data instance Data Bottomable sem a where
192 Bottom :: Data Bottomable sem a
193 instance Bottomable sem => Derivable (Data Bottomable sem) where
194 derive Bottom{} = bottom
195
196 -- Constantable
197 data instance Data (Constantable c) sem a where
198 Constant {-Typeable c =>-} :: c -> Data (Constantable c) sem c
199 instance Constantable c sem => Derivable (Data (Constantable c) sem) where
200 derive = \case
201 Constant x -> constant x
202 instance
203 ( Constantable c sem
204 , Typeable c
205 ) =>
206 Constantable c (SomeData sem)
207 where
208 constant c = SomeData (Constant c)
209 instance{-Typeable c =>-} Constantable c (Data (Constantable c) sem) where
210 constant = Constant
211
212 -- Eitherable
213 data instance Data Eitherable sem a where
214 Either :: Data Eitherable sem ((l -> a) -> (r -> a) -> Either l r -> a)
215 Left :: Data Eitherable sem (l -> Either l r)
216 Right :: Data Eitherable sem (r -> Either l r)
217 instance Eitherable sem => Derivable (Data Eitherable sem) where
218 derive = \case
219 Either -> either
220 Left -> left
221 Right -> right
222 instance Eitherable sem => Eitherable (SomeData sem) where
223 either = SomeData Either
224 left = SomeData Left
225 right = SomeData Right
226 instance Eitherable (Data Eitherable sem) where
227 either = Either
228 left = Left
229 right = Right
230
231 -- Equalable
232 data instance Data Equalable sem a where
233 Equal :: Eq.Eq a => Data Equalable sem (a -> a -> Bool)
234 instance Equalable sem => Derivable (Data Equalable sem) where
235 derive = \case
236 Equal -> equal
237 instance
238 ( Equalable sem
239 ) =>
240 Equalable (SomeData sem)
241 where
242 equal = SomeData Equal
243 instance Equalable (Data Equalable sem) where
244 equal = Equal
245
246 -- Emptyable
247 data instance Data Emptyable sem a where
248 Empty :: Data Emptyable sem a
249 instance Emptyable sem => Derivable (Data Emptyable sem) where
250 derive = \case
251 Empty -> empty
252 instance
253 ( Emptyable sem
254 ) =>
255 Emptyable (SomeData sem)
256 where
257 empty = SomeData Empty
258 instance Emptyable (Data Emptyable sem) where
259 empty = Empty
260
261 -- Semigroupable
262 data instance Data Semigroupable sem a where
263 Concat :: Semigroup a => Data Semigroupable sem (a -> a -> a)
264 infixr 4 `Concat`
265 instance Semigroupable sem => Derivable (Data Semigroupable sem) where
266 derive = \case
267 Concat -> concat
268 instance
269 ( Semigroupable sem
270 ) =>
271 Semigroupable (SomeData sem)
272 where
273 concat = SomeData Concat
274 instance Semigroupable (Data Semigroupable sem) where
275 concat = Concat
276
277 -- IfThenElseable
278 data instance Data IfThenElseable sem a where
279 IfThenElse ::
280 SomeData sem Bool ->
281 SomeData sem a ->
282 SomeData sem a ->
283 Data IfThenElseable sem a
284 instance IfThenElseable sem => Derivable (Data IfThenElseable sem) where
285 derive = \case
286 IfThenElse test ok ko -> ifThenElse (derive test) (derive ok) (derive ko)
287 instance
288 ( IfThenElseable sem
289 ) =>
290 IfThenElseable (SomeData sem)
291 where
292 ifThenElse test ok ko = SomeData (IfThenElse test ok ko)
293 instance IfThenElseable sem => IfThenElseable (Data IfThenElseable sem) where
294 ifThenElse test ok ko = IfThenElse (SomeData test) (SomeData ok) (SomeData ko)
295
296 -- Inferable
297 data instance Data (Inferable c) sem a where
298 Infer :: Data (Inferable c) sem c
299 instance Inferable c sem => Derivable (Data (Inferable c) sem) where
300 derive = \case
301 Infer -> infer
302 instance
303 ( Inferable c sem
304 , Typeable c
305 ) =>
306 Inferable c (SomeData sem)
307 where
308 infer = SomeData Infer
309 instance Inferable c (Data (Inferable c) sem) where
310 infer = Infer
311
312 -- Listable
313 data instance Data Listable sem a where
314 Cons :: Data Listable sem (a -> [a] -> [a])
315 Nil :: Data Listable sem [a]
316 infixr 4 `Cons`
317 instance Listable sem => Derivable (Data Listable sem) where
318 derive = \case
319 Cons -> cons
320 Nil -> nil
321 instance
322 ( Listable sem
323 ) =>
324 Listable (SomeData sem)
325 where
326 cons = SomeData Cons
327 nil = SomeData Nil
328 instance Listable (Data Listable sem) where
329 cons = Cons
330 nil = Nil
331
332 -- Maybeable
333 data instance Data Maybeable sem a where
334 Nothing :: Data Maybeable sem (Maybe a)
335 Just :: Data Maybeable sem (a -> Maybe a)
336 instance Maybeable sem => Derivable (Data Maybeable sem) where
337 derive = \case
338 Nothing -> nothing
339 Just -> just
340 instance
341 ( Maybeable sem
342 ) =>
343 Maybeable (SomeData sem)
344 where
345 nothing = SomeData Nothing
346 just = SomeData Just
347 instance Maybeable (Data Maybeable sem) where
348 nothing = Nothing
349 just = Just