]> Git — Sourcephile - haskell/symantic-base.git/blob - src/Symantic/Syntaxes/Classes.hs
iface: add many `Forall` instances
[haskell/symantic-base.git] / src / Symantic / Syntaxes / Classes.hs
1 -- For ifSemantic
2 {-# LANGUAGE AllowAmbiguousTypes #-}
3 -- For Syntax
4 {-# LANGUAGE DataKinds #-}
5 -- For (:!:)
6 {-# LANGUAGE PatternSynonyms #-}
7 -- For ifSemantic
8 {-# LANGUAGE RankNTypes #-}
9 -- For Permutation
10 {-# LANGUAGE TypeFamilyDependencies #-}
11 -- For Permutation
12 {-# LANGUAGE UndecidableInstances #-}
13
14 -- | This module gathers commonly used tagless-final combinators
15 -- (the syntax part of symantics).
16 --
17 -- Note: combinators in this module conflict with usual ones from the @Prelude@
18 -- hence they are meant to be imported either explicitely or qualified.
19 module Symantic.Syntaxes.Classes where
20
21 import Control.Category qualified as Cat
22 import Data.Bool (Bool (..))
23 import Data.Char (Char)
24 import Data.Either (Either (..))
25 import Data.Eq (Eq)
26 import Data.Function qualified as Fun
27 import Data.Int (Int)
28 import Data.Kind (Constraint)
29 import Data.Maybe (Maybe (..), fromJust)
30 import Data.Proxy (Proxy (..))
31 import Data.Semigroup (Semigroup)
32 import Data.String (String)
33 import Data.Tuple qualified as Tuple
34 import GHC.Generics (Generic)
35 import Numeric.Natural (Natural)
36
37 import Symantic.Syntaxes.CurryN
38 import Symantic.Syntaxes.Derive
39 import Symantic.Syntaxes.EithersOfTuples
40
41 -- * Type 'Syntax'
42 type Syntax = Semantic -> Constraint
43
44 -- ** Type family 'Syntaxes'
45
46 -- | Merge several 'Syntax'es into a single one.
47 --
48 -- Useful in 'IfSemantic' or 'All'.
49 type family Syntaxes (syns :: [Syntax]) (sem :: Semantic) :: Constraint where
50 Syntaxes '[] sem = (() :: Constraint)
51 Syntaxes (syn ': syns) sem = ((syn sem, Syntaxes syns sem) :: Constraint)
52
53 -- * Class 'Abstractable'
54 class Abstractable sem where
55 -- | Lambda term abstraction, in HOAS (Higher-Order Abstract Syntax) style.
56 lam :: (sem a -> sem b) -> sem (a -> b)
57 lam f = liftDerived (lam (derive Fun.. f Fun.. liftDerived))
58 default lam ::
59 FromDerived Abstractable sem =>
60 Derivable sem =>
61 (sem a -> sem b) ->
62 sem (a -> b)
63
64 -- ** Class 'Abstractable1'
65 class Abstractable1 sem where
66 -- | Like 'lam' but whose argument must be used only once,
67 -- hence safe to beta-reduce (inline) without duplicating work.
68 lam1 :: (sem a -> sem b) -> sem (a -> b)
69 lam1 f = liftDerived (lam1 (derive Fun.. f Fun.. liftDerived))
70 default lam1 ::
71 FromDerived Abstractable1 sem =>
72 Derivable sem =>
73 (sem a -> sem b) ->
74 sem (a -> b)
75
76 -- ** Class 'Varable'
77 class Varable sem where
78 -- | Mark the use of a variable.
79 var :: sem a -> sem a
80 var = liftDerived1 var
81 default var :: FromDerived1 Varable sem => sem a -> sem a
82
83 -- ** Class 'Instantiable'
84 class Instantiable sem where
85 -- | Instantiate.
86 (.@) :: sem (a -> b) -> sem a -> sem b
87
88 infixl 9 .@
89 (.@) = liftDerived2 (.@)
90 default (.@) ::
91 FromDerived2 Instantiable sem =>
92 sem (a -> b) ->
93 sem a ->
94 sem b
95
96 -- ** Class 'Unabstractable'
97 -- | All operations in lambda calculus can be encoded
98 -- via abstraction elimination into the SK calculus
99 -- as binary trees whose leaves are one
100 -- of the three symbols S ('ap') and K ('const').
101 class Unabstractable sem where
102 -- | S
103 ap :: sem ((a -> b -> c) -> (a -> b) -> a -> c)
104 -- | K
105 const :: sem (a -> b -> a)
106 -- | I
107 id :: sem (a -> a)
108 -- | B
109 (.) :: sem ((b -> c) -> (a -> b) -> a -> c)
110 infixr 9 .
111 -- | C
112 flip :: sem ((a -> b -> c) -> b -> a -> c)
113 ($) :: sem ((a -> b) -> a -> b)
114 infixr 0 $
115
116 ap = liftDerived ap
117 const = liftDerived const
118 id = liftDerived id
119 (.) = liftDerived (.)
120 flip = liftDerived flip
121 ($) = liftDerived ($)
122
123 default ap ::
124 FromDerived Unabstractable sem =>
125 sem ((a -> b -> c) -> (a -> b) -> a -> c)
126 default const ::
127 FromDerived Unabstractable sem =>
128 sem (a -> b -> a)
129 default id ::
130 FromDerived Unabstractable sem =>
131 sem (a -> a)
132 default (.) ::
133 FromDerived Unabstractable sem =>
134 sem ((b -> c) -> (a -> b) -> a -> c)
135 default flip ::
136 FromDerived Unabstractable sem =>
137 sem ((a -> b -> c) -> b -> a -> c)
138 default ($) ::
139 FromDerived Unabstractable sem =>
140 sem ((a -> b) -> a -> b)
141
142 -- * Class 'Anythingable'
143 class Anythingable sem where
144 anything :: sem a -> sem a
145 anything = Fun.id
146
147 -- * Class 'Bottomable'
148 class Bottomable sem where
149 bottom :: sem a
150
151 -- * Class 'Constantable'
152 class Constantable c sem where
153 constant :: c -> sem c
154 constant = liftDerived Fun.. constant
155 default constant ::
156 FromDerived (Constantable c) sem =>
157 c ->
158 sem c
159
160 -- * Class 'Eitherable'
161 class Eitherable sem where
162 either :: sem ((l -> a) -> (r -> a) -> Either l r -> a)
163 left :: sem (l -> Either l r)
164 right :: sem (r -> Either l r)
165 either = liftDerived either
166 left = liftDerived left
167 right = liftDerived right
168 default either ::
169 FromDerived Eitherable sem =>
170 sem ((l -> a) -> (r -> a) -> Either l r -> a)
171 default left ::
172 FromDerived Eitherable sem =>
173 sem (l -> Either l r)
174 default right ::
175 FromDerived Eitherable sem =>
176 sem (r -> Either l r)
177
178 -- * Class 'Equalable'
179 class Equalable sem where
180 equal :: Eq a => sem (a -> a -> Bool)
181 equal = liftDerived equal
182 default equal ::
183 FromDerived Equalable sem =>
184 Eq a =>
185 sem (a -> a -> Bool)
186
187 infix 4 `equal`, ==
188 (==) ::
189 Instantiable sem =>
190 Equalable sem =>
191 Eq a =>
192 sem a ->
193 sem a ->
194 sem Bool
195 (==) x y = equal .@ x .@ y
196
197 -- * Class 'IfThenElseable'
198 class IfThenElseable sem where
199 ifThenElse :: sem Bool -> sem a -> sem a -> sem a
200 ifThenElse = liftDerived3 ifThenElse
201 default ifThenElse ::
202 FromDerived3 IfThenElseable sem =>
203 sem Bool ->
204 sem a ->
205 sem a ->
206 sem a
207
208 -- * Class 'Inferable'
209 class Inferable a sem where
210 infer :: sem a
211 default infer :: FromDerived (Inferable a) sem => sem a
212 infer = liftDerived infer
213
214 unit :: Inferable () sem => sem ()
215 unit = infer
216 bool :: Inferable Bool sem => sem Bool
217 bool = infer
218 char :: Inferable Char sem => sem Char
219 char = infer
220 int :: Inferable Int sem => sem Int
221 int = infer
222 natural :: Inferable Natural sem => sem Natural
223 natural = infer
224 string :: Inferable String sem => sem String
225 string = infer
226
227 -- * Class 'Listable'
228 class Listable sem where
229 cons :: sem (a -> [a] -> [a])
230 nil :: sem [a]
231 cons = liftDerived cons
232 nil = liftDerived nil
233 default cons ::
234 FromDerived Listable sem =>
235 sem (a -> [a] -> [a])
236 default nil ::
237 FromDerived Listable sem =>
238 sem [a]
239
240 -- * Class 'Maybeable'
241 class Maybeable sem where
242 nothing :: sem (Maybe a)
243 just :: sem (a -> Maybe a)
244 nothing = liftDerived nothing
245 just = liftDerived just
246 default nothing ::
247 FromDerived Maybeable sem =>
248 sem (Maybe a)
249 default just ::
250 FromDerived Maybeable sem =>
251 sem (a -> Maybe a)
252
253 -- * Class 'IsoFunctor'
254 class IsoFunctor sem where
255 (<%>) :: Iso a b -> sem a -> sem b
256 infixl 4 <%>
257 (<%>) iso = liftDerived1 (iso <%>)
258 default (<%>) ::
259 FromDerived1 IsoFunctor sem =>
260 Iso a b ->
261 sem a ->
262 sem b
263
264 -- ** Type 'Iso'
265 data Iso a b = Iso {a2b :: a -> b, b2a :: b -> a}
266 instance Cat.Category Iso where
267 id = Iso Cat.id Cat.id
268 f . g = Iso (a2b f Cat.. a2b g) (b2a g Cat.. b2a f)
269
270 -- * Class 'ProductFunctor'
271
272 -- | Beware that this is an @infixr@,
273 -- not @infixl@ like 'Control.Applicative.<*>';
274 -- this is to follow what is expected by 'ADT'.
275 class ProductFunctor sem where
276 (<.>) :: sem a -> sem b -> sem (a, b)
277 infixr 4 <.>
278 (<.>) = liftDerived2 (<.>)
279 default (<.>) ::
280 FromDerived2 ProductFunctor sem =>
281 sem a ->
282 sem b ->
283 sem (a, b)
284 (<.) :: sem a -> sem () -> sem a
285 infixr 4 <.
286 ra <. rb = Iso Tuple.fst (,()) <%> (ra <.> rb)
287 default (<.) :: IsoFunctor sem => sem a -> sem () -> sem a
288 (.>) :: sem () -> sem a -> sem a
289 infixr 4 .>
290 ra .> rb = Iso Tuple.snd ((),) <%> (ra <.> rb)
291 default (.>) :: IsoFunctor sem => sem () -> sem a -> sem a
292
293 -- * Class 'SumFunctor'
294
295 -- | Beware that this is an @infixr@,
296 -- not @infixl@ like 'Control.Applicative.<|>';
297 -- this is to follow what is expected by 'ADT'.
298 class SumFunctor sem where
299 (<+>) :: sem a -> sem b -> sem (Either a b)
300 infixr 3 <+>
301 (<+>) = liftDerived2 (<+>)
302 default (<+>) ::
303 FromDerived2 SumFunctor sem =>
304 sem a ->
305 sem b ->
306 sem (Either a b)
307
308 -- | Like @(,)@ but @infixr@.
309 -- Mostly useful for clarity when using 'SumFunctor'.
310 pattern (:!:) :: a -> b -> (a, b)
311 pattern a :!: b <-
312 (a, b)
313 where
314 a :!: b = (a, b)
315
316 infixr 4 :!:
317 {-# COMPLETE (:!:) #-}
318
319 -- * Class 'AlternativeFunctor'
320
321 -- | Beware that this is an @infixr@,
322 -- not @infixl@ like 'Control.Applicative.<|>';
323 -- this is to follow what is expected by 'ADT'.
324 class AlternativeFunctor sem where
325 (<|>) :: sem a -> sem a -> sem a
326 infixr 3 <|>
327 (<|>) = liftDerived2 (<|>)
328 default (<|>) ::
329 FromDerived2 AlternativeFunctor sem =>
330 sem a ->
331 sem a ->
332 sem a
333
334 -- * Class 'Dicurryable'
335 class Dicurryable sem where
336 dicurry ::
337 CurryN args =>
338 proxy args ->
339 (args -..-> a) -> -- construction
340 (a -> Tuples args) -> -- destruction
341 sem (Tuples args) ->
342 sem a
343 dicurry args constr destr = liftDerived1 (dicurry args constr destr)
344 default dicurry ::
345 FromDerived1 Dicurryable sem =>
346 CurryN args =>
347 proxy args ->
348 (args -..-> a) ->
349 (a -> Tuples args) ->
350 sem (Tuples args) ->
351 sem a
352
353 construct ::
354 forall args a sem.
355 Dicurryable sem =>
356 Generic a =>
357 EoTOfRep a =>
358 CurryN args =>
359 Tuples args ~ EoT (ADT a) =>
360 (args ~ Args (args -..-> a)) =>
361 (args -..-> a) ->
362 sem (Tuples args) ->
363 sem a
364 construct f = dicurry (Proxy :: Proxy args) f eotOfadt
365
366 -- * Class 'Dataable'
367
368 -- | Enable the contruction or deconstruction
369 -- of an 'ADT' (algebraic data type).
370 class Dataable a sem where
371 dataType :: sem (EoT (ADT a)) -> sem a
372 default dataType ::
373 Generic a =>
374 RepOfEoT a =>
375 EoTOfRep a =>
376 IsoFunctor sem =>
377 sem (EoT (ADT a)) ->
378 sem a
379 dataType = (<%>) (Iso adtOfeot eotOfadt)
380
381 -- * Class 'IfSemantic'
382
383 -- | 'IfSemantic' enables to change the 'Syntax' for a specific 'Semantic'.
384 --
385 -- Useful when a 'Semantic' does not implement some 'Syntax'es used by other 'Semantic's.
386 class
387 IfSemantic
388 (thenSyntaxes :: [Syntax])
389 (elseSyntaxes :: [Syntax])
390 thenSemantic
391 elseSemantic
392 where
393 ifSemantic ::
394 (Syntaxes thenSyntaxes thenSemantic => thenSemantic a) ->
395 (Syntaxes elseSyntaxes elseSemantic => elseSemantic a) ->
396 elseSemantic a
397
398 instance
399 {-# OVERLAPPING #-}
400 Syntaxes thenSyntaxes thenSemantic =>
401 IfSemantic thenSyntaxes elseSyntaxes thenSemantic thenSemantic
402 where
403 ifSemantic thenSyntax _elseSyntax = thenSyntax
404 instance
405 Syntaxes elseSyntaxes elseSemantic =>
406 IfSemantic thenSyntaxes elseSyntaxes thenSemantic elseSemantic
407 where
408 ifSemantic _thenSyntax elseSyntax = elseSyntax
409
410 -- * Class 'Monoidable'
411 class
412 ( Emptyable sem
413 , Semigroupable sem
414 ) =>
415 Monoidable sem
416 instance
417 ( Emptyable sem
418 , Semigroupable sem
419 ) =>
420 Monoidable sem
421
422 -- ** Class 'Emptyable'
423 class Emptyable sem where
424 empty :: sem a
425 empty = liftDerived empty
426 default empty ::
427 FromDerived Emptyable sem =>
428 sem a
429
430 -- ** Class 'Semigroupable'
431 class Semigroupable sem where
432 concat :: Semigroup a => sem (a -> a -> a)
433 concat = liftDerived concat
434 default concat ::
435 FromDerived Semigroupable sem =>
436 Semigroup a =>
437 sem (a -> a -> a)
438
439 infixr 6 `concat`, <>
440 (<>) ::
441 Instantiable sem =>
442 Semigroupable sem =>
443 Semigroup a =>
444 sem a ->
445 sem a ->
446 sem a
447 (<>) x y = concat .@ x .@ y
448
449 -- ** Class 'Optionable'
450 class Optionable sem where
451 optional :: sem a -> sem (Maybe a)
452 optional = liftDerived1 optional
453 default optional ::
454 FromDerived1 Optionable sem =>
455 sem a ->
456 sem (Maybe a)
457
458 -- * Class 'Repeatable'
459 class Repeatable sem where
460 many0 :: sem a -> sem [a]
461 many1 :: sem a -> sem [a]
462 many0 = liftDerived1 many0
463 many1 = liftDerived1 many1
464 default many0 ::
465 FromDerived1 Repeatable sem =>
466 sem a ->
467 sem [a]
468 default many1 ::
469 FromDerived1 Repeatable sem =>
470 sem a ->
471 sem [a]
472
473 -- | Alias to 'many0'.
474 many :: Repeatable sem => sem a -> sem [a]
475 many = many0
476
477 -- | Alias to 'many1'.
478 some :: Repeatable sem => sem a -> sem [a]
479 some = many1
480
481 -- * Class 'Permutable'
482 class Permutable sem where
483 -- Use @TypeFamilyDependencies@ to help type-inference infer @(sem)@.
484 type Permutation (sem :: Semantic) = (r :: Semantic) | r -> sem
485 type Permutation sem = Permutation (Derived sem)
486 permutable :: Permutation sem a -> sem a
487 perm :: sem a -> Permutation sem a
488 noPerm :: Permutation sem ()
489 permWithDefault :: a -> sem a -> Permutation sem a
490 optionalPerm ::
491 Eitherable sem =>
492 IsoFunctor sem =>
493 Permutable sem =>
494 sem a ->
495 Permutation sem (Maybe a)
496 optionalPerm = permWithDefault Nothing Fun.. (<%>) (Iso Just fromJust)
497
498 (<&>) ::
499 Permutable sem =>
500 ProductFunctor (Permutation sem) =>
501 sem a ->
502 Permutation sem b ->
503 Permutation sem (a, b)
504 x <&> y = perm x <.> y
505 infixr 4 <&>
506 {-# INLINE (<&>) #-}
507
508 (<?&>) ::
509 Eitherable sem =>
510 IsoFunctor sem =>
511 Permutable sem =>
512 ProductFunctor (Permutation sem) =>
513 sem a ->
514 Permutation sem b ->
515 Permutation sem (Maybe a, b)
516 x <?&> y = optionalPerm x <.> y
517 infixr 4 <?&>
518 {-# INLINE (<?&>) #-}
519
520 (<*&>) ::
521 Eitherable sem =>
522 Repeatable sem =>
523 IsoFunctor sem =>
524 Permutable sem =>
525 ProductFunctor (Permutation sem) =>
526 sem a ->
527 Permutation sem b ->
528 Permutation sem ([a], b)
529 x <*&> y = permWithDefault [] (many1 x) <.> y
530 infixr 4 <*&>
531 {-# INLINE (<*&>) #-}
532
533 (<+&>) ::
534 Eitherable sem =>
535 Repeatable sem =>
536 IsoFunctor sem =>
537 Permutable sem =>
538 ProductFunctor (Permutation sem) =>
539 sem a ->
540 Permutation sem b ->
541 Permutation sem ([a], b)
542 x <+&> y = perm (many1 x) <.> y
543 infixr 4 <+&>
544 {-# INLINE (<+&>) #-}
545
546 -- * Class 'Voidable'
547 class Voidable sem where
548 -- | Useful to supply @(a)@ to a @(sem)@ consuming @(a)@,
549 -- for example in the format of a printing interpreter.
550 void :: a -> sem a -> sem ()
551 void = liftDerived1 Fun.. void
552 default void ::
553 FromDerived1 Voidable sem =>
554 a ->
555 sem a ->
556 sem ()
557
558 -- * Class 'Substractable'
559 class Substractable sem where
560 (<->) :: sem a -> sem b -> sem a
561 infixr 3 <->
562 (<->) = liftDerived2 (<->)
563 default (<->) ::
564 FromDerived2 Substractable sem =>
565 sem a ->
566 sem b ->
567 sem a