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