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   Abstractable sem =>
 190   Instantiable sem =>
 191   Equalable sem =>
 192   Eq a =>
 193   sem a ->
 194   sem a ->
 195   sem Bool
 196 (==) x y = equal .@ x .@ y
 197
 198 -- * Class 'IfThenElseable'
 199 class IfThenElseable sem where
 200   ifThenElse :: sem Bool -> sem a -> sem a -> sem a
 201   ifThenElse = liftDerived3 ifThenElse
 202   default ifThenElse ::
 203     FromDerived3 IfThenElseable sem =>
 204     sem Bool ->
 205     sem a ->
 206     sem a ->
 207     sem a
 208
 209 -- * Class 'Inferable'
 210 class Inferable a sem where
 211   infer :: sem a
 212   default infer :: FromDerived (Inferable a) sem => sem a
 213   infer = liftDerived infer
 214
 215 unit :: Inferable () sem => sem ()
 216 unit = infer
 217 bool :: Inferable Bool sem => sem Bool
 218 bool = infer
 219 char :: Inferable Char sem => sem Char
 220 char = infer
 221 int :: Inferable Int sem => sem Int
 222 int = infer
 223 natural :: Inferable Natural sem => sem Natural
 224 natural = infer
 225 string :: Inferable String sem => sem String
 226 string = infer
 227
 228 -- * Class 'Listable'
 229 class Listable sem where
 230   cons :: sem (a -> [a] -> [a])
 231   nil :: sem [a]
 232   cons = liftDerived cons
 233   nil = liftDerived nil
 234   default cons ::
 235     FromDerived Listable sem =>
 236     sem (a -> [a] -> [a])
 237   default nil ::
 238     FromDerived Listable sem =>
 239     sem [a]
 240
 241 -- * Class 'Maybeable'
 242 class Maybeable sem where
 243   nothing :: sem (Maybe a)
 244   just :: sem (a -> Maybe a)
 245   nothing = liftDerived nothing
 246   just = liftDerived just
 247   default nothing ::
 248     FromDerived Maybeable sem =>
 249     sem (Maybe a)
 250   default just ::
 251     FromDerived Maybeable sem =>
 252     sem (a -> Maybe a)
 253
 254 -- * Class 'IsoFunctor'
 255 class IsoFunctor sem where
 256   (<%>) :: Iso a b -> sem a -> sem b
 257   infixl 4 <%>
 258   (<%>) iso = liftDerived1 (iso <%>)
 259   default (<%>) ::
 260     FromDerived1 IsoFunctor sem =>
 261     Iso a b ->
 262     sem a ->
 263     sem b
 264
 265 -- ** Type 'Iso'
 266 data Iso a b = Iso {a2b :: a -> b, b2a :: b -> a}
 267 instance Cat.Category Iso where
 268   id = Iso Cat.id Cat.id
 269   f . g = Iso (a2b f Cat.. a2b g) (b2a g Cat.. b2a f)
 270
 271 -- * Class 'ProductFunctor'
 272
 273 -- | Beware that this is an @infixr@,
 274 -- not @infixl@ like 'Control.Applicative.<*>';
 275 -- this is to follow what is expected by 'ADT'.
 276 class ProductFunctor sem where
 277   (<.>) :: sem a -> sem b -> sem (a, b)
 278   infixr 4 <.>
 279   (<.>) = liftDerived2 (<.>)
 280   default (<.>) ::
 281     FromDerived2 ProductFunctor sem =>
 282     sem a ->
 283     sem b ->
 284     sem (a, b)
 285   (<.) :: sem a -> sem () -> sem a
 286   infixr 4 <.
 287   ra <. rb = Iso Tuple.fst (,()) <%> (ra <.> rb)
 288   default (<.) :: IsoFunctor sem => sem a -> sem () -> sem a
 289   (.>) :: sem () -> sem a -> sem a
 290   infixr 4 .>
 291   ra .> rb = Iso Tuple.snd ((),) <%> (ra <.> rb)
 292   default (.>) :: IsoFunctor sem => sem () -> sem a -> sem a
 293
 294 -- * Class 'SumFunctor'
 295
 296 -- | Beware that this is an @infixr@,
 297 -- not @infixl@ like 'Control.Applicative.<|>';
 298 -- this is to follow what is expected by 'ADT'.
 299 class SumFunctor sem where
 300   (<+>) :: sem a -> sem b -> sem (Either a b)
 301   infixr 3 <+>
 302   (<+>) = liftDerived2 (<+>)
 303   default (<+>) ::
 304     FromDerived2 SumFunctor sem =>
 305     sem a ->
 306     sem b ->
 307     sem (Either a b)
 308
 309 -- | Like @(,)@ but @infixr@.
 310 -- Mostly useful for clarity when using 'SumFunctor'.
 311 pattern (:!:) :: a -> b -> (a, b)
 312 pattern a :!: b <-
 313   (a, b)
 314   where
 315     a :!: b = (a, b)
 316
 317 infixr 4 :!:
 318 {-# COMPLETE (:!:) #-}
 319
 320 -- * Class 'AlternativeFunctor'
 321
 322 -- | Beware that this is an @infixr@,
 323 -- not @infixl@ like 'Control.Applicative.<|>';
 324 -- this is to follow what is expected by 'ADT'.
 325 class AlternativeFunctor sem where
 326   (<|>) :: sem a -> sem a -> sem a
 327   infixr 3 <|>
 328   (<|>) = liftDerived2 (<|>)
 329   default (<|>) ::
 330     FromDerived2 AlternativeFunctor sem =>
 331     sem a ->
 332     sem a ->
 333     sem a
 334
 335 -- * Class 'Dicurryable'
 336 class Dicurryable sem where
 337   dicurry ::
 338     CurryN args =>
 339     proxy args ->
 340     (args -..-> a) -> -- construction
 341     (a -> Tuples args) -> -- destruction
 342     sem (Tuples args) ->
 343     sem a
 344   dicurry args constr destr = liftDerived1 (dicurry args constr destr)
 345   default dicurry ::
 346     FromDerived1 Dicurryable sem =>
 347     CurryN args =>
 348     proxy args ->
 349     (args -..-> a) ->
 350     (a -> Tuples args) ->
 351     sem (Tuples args) ->
 352     sem a
 353
 354 construct ::
 355   forall args a sem.
 356   Dicurryable sem =>
 357   Generic a =>
 358   EoTOfRep a =>
 359   CurryN args =>
 360   Tuples args ~ EoT (ADT a) =>
 361   (args ~ Args (args -..-> a)) =>
 362   (args -..-> a) ->
 363   sem (Tuples args) ->
 364   sem a
 365 construct f = dicurry (Proxy :: Proxy args) f eotOfadt
 366
 367 -- * Class 'Dataable'
 368
 369 -- | Enable the contruction or deconstruction
 370 -- of an 'ADT' (algebraic data type).
 371 class Dataable a sem where
 372   dataType :: sem (EoT (ADT a)) -> sem a
 373   default dataType ::
 374     Generic a =>
 375     RepOfEoT a =>
 376     EoTOfRep a =>
 377     IsoFunctor sem =>
 378     sem (EoT (ADT a)) ->
 379     sem a
 380   dataType = (<%>) (Iso adtOfeot eotOfadt)
 381
 382 -- * Class 'IfSemantic'
 383
 384 -- | 'IfSemantic' enables to change the 'Syntax' for a specific 'Semantic'.
 385 --
 386 -- Useful when a 'Semantic' does not implement some 'Syntax'es used by other 'Semantic's.
 387 class
 388   IfSemantic
 389     (thenSyntaxes :: [Syntax])
 390     (elseSyntaxes :: [Syntax])
 391     thenSemantic
 392     elseSemantic
 393   where
 394   ifSemantic ::
 395     (Syntaxes thenSyntaxes thenSemantic => thenSemantic a) ->
 396     (Syntaxes elseSyntaxes elseSemantic => elseSemantic a) ->
 397     elseSemantic a
 398
 399 instance
 400   {-# OVERLAPPING #-}
 401   Syntaxes thenSyntaxes thenSemantic =>
 402   IfSemantic thenSyntaxes elseSyntaxes thenSemantic thenSemantic
 403   where
 404   ifSemantic thenSyntax _elseSyntax = thenSyntax
 405 instance
 406   Syntaxes elseSyntaxes elseSemantic =>
 407   IfSemantic thenSyntaxes elseSyntaxes thenSemantic elseSemantic
 408   where
 409   ifSemantic _thenSyntax elseSyntax = elseSyntax
 410
 411 -- * Class 'Monoidable'
 412 class
 413   ( Emptyable sem
 414   , Semigroupable sem
 415   ) =>
 416   Monoidable sem
 417 instance
 418   ( Emptyable sem
 419   , Semigroupable sem
 420   ) =>
 421   Monoidable sem
 422
 423 -- ** Class 'Emptyable'
 424 class Emptyable sem where
 425   empty :: sem a
 426   empty = liftDerived empty
 427   default empty ::
 428     FromDerived Emptyable sem =>
 429     sem a
 430
 431 -- ** Class 'Semigroupable'
 432 class Semigroupable sem where
 433   concat :: Semigroup a => sem (a -> a -> a)
 434   concat = liftDerived concat
 435   default concat ::
 436     FromDerived Semigroupable sem =>
 437     Semigroup a =>
 438     sem (a -> a -> a)
 439
 440 infixr 6 `concat`, <>
 441 (<>) ::
 442   Abstractable sem =>
 443   Instantiable sem =>
 444   Semigroupable sem =>
 445   Semigroup a =>
 446   sem a ->
 447   sem a ->
 448   sem a
 449 (<>) x y = concat .@ x .@ y
 450
 451 -- ** Class 'Optionable'
 452 class Optionable sem where
 453   optional :: sem a -> sem (Maybe a)
 454   optional = liftDerived1 optional
 455   default optional ::
 456     FromDerived1 Optionable sem =>
 457     sem a ->
 458     sem (Maybe a)
 459
 460 -- * Class 'Repeatable'
 461 class Repeatable sem where
 462   many0 :: sem a -> sem [a]
 463   many1 :: sem a -> sem [a]
 464   many0 = liftDerived1 many0
 465   many1 = liftDerived1 many1
 466   default many0 ::
 467     FromDerived1 Repeatable sem =>
 468     sem a ->
 469     sem [a]
 470   default many1 ::
 471     FromDerived1 Repeatable sem =>
 472     sem a ->
 473     sem [a]
 474
 475 -- | Alias to 'many0'.
 476 many :: Repeatable sem => sem a -> sem [a]
 477 many = many0
 478
 479 -- | Alias to 'many1'.
 480 some :: Repeatable sem => sem a -> sem [a]
 481 some = many1
 482
 483 -- * Class 'Permutable'
 484 class Permutable sem where
 485   -- Use @TypeFamilyDependencies@ to help type-inference infer @(sem)@.
 486   type Permutation (sem :: Semantic) = (r :: Semantic) | r -> sem
 487   type Permutation sem = Permutation (Derived sem)
 488   permutable :: Permutation sem a -> sem a
 489   perm :: sem a -> Permutation sem a
 490   noPerm :: Permutation sem ()
 491   permWithDefault :: a -> sem a -> Permutation sem a
 492   optionalPerm ::
 493     Eitherable sem =>
 494     IsoFunctor sem =>
 495     Permutable sem =>
 496     sem a ->
 497     Permutation sem (Maybe a)
 498   optionalPerm = permWithDefault Nothing Fun.. (<%>) (Iso Just fromJust)
 499
 500 (<&>) ::
 501   Permutable sem =>
 502   ProductFunctor (Permutation sem) =>
 503   sem a ->
 504   Permutation sem b ->
 505   Permutation sem (a, b)
 506 x <&> y = perm x <.> y
 507 infixr 4 <&>
 508 {-# INLINE (<&>) #-}
 509
 510 (<?&>) ::
 511   Eitherable sem =>
 512   IsoFunctor sem =>
 513   Permutable sem =>
 514   ProductFunctor (Permutation sem) =>
 515   sem a ->
 516   Permutation sem b ->
 517   Permutation sem (Maybe a, b)
 518 x <?&> y = optionalPerm x <.> y
 519 infixr 4 <?&>
 520 {-# INLINE (<?&>) #-}
 521
 522 (<*&>) ::
 523   Eitherable sem =>
 524   Repeatable sem =>
 525   IsoFunctor sem =>
 526   Permutable sem =>
 527   ProductFunctor (Permutation sem) =>
 528   sem a ->
 529   Permutation sem b ->
 530   Permutation sem ([a], b)
 531 x <*&> y = permWithDefault [] (many1 x) <.> y
 532 infixr 4 <*&>
 533 {-# INLINE (<*&>) #-}
 534
 535 (<+&>) ::
 536   Eitherable sem =>
 537   Repeatable sem =>
 538   IsoFunctor sem =>
 539   Permutable sem =>
 540   ProductFunctor (Permutation sem) =>
 541   sem a ->
 542   Permutation sem b ->
 543   Permutation sem ([a], b)
 544 x <+&> y = perm (many1 x) <.> y
 545 infixr 4 <+&>
 546 {-# INLINE (<+&>) #-}
 547
 548 -- * Class 'Voidable'
 549 class Voidable sem where
 550   -- | Useful to supply @(a)@ to a @(sem)@ consuming @(a)@,
 551   -- for example in the format of a printing interpreter.
 552   void :: a -> sem a -> sem ()
 553   void = liftDerived1 Fun.. void
 554   default void ::
 555     FromDerived1 Voidable sem =>
 556     a ->
 557     sem a ->
 558     sem ()
 559
 560 -- * Class 'Substractable'
 561 class Substractable sem where
 562   (<->) :: sem a -> sem b -> sem a
 563   infixr 3 <->
 564   (<->) = liftDerived2 (<->)
 565   default (<->) ::
 566     FromDerived2 Substractable sem =>
 567     sem a ->
 568     sem b ->
 569     sem a