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   Abstractable sem =>
 442   Instantiable sem =>
 443   Semigroupable sem =>
 444   Semigroup a =>
 445   sem a ->
 446   sem a ->
 447   sem a
 448 (<>) x y = concat .@ x .@ y
 449
 450 -- ** Class 'Optionable'
 451 class Optionable sem where
 452   optional :: sem a -> sem (Maybe a)
 453   optional = liftDerived1 optional
 454   default optional ::
 455     FromDerived1 Optionable sem =>
 456     sem a ->
 457     sem (Maybe a)
 458
 459 -- * Class 'Repeatable'
 460 class Repeatable sem where
 461   many0 :: sem a -> sem [a]
 462   many1 :: sem a -> sem [a]
 463   many0 = liftDerived1 many0
 464   many1 = liftDerived1 many1
 465   default many0 ::
 466     FromDerived1 Repeatable sem =>
 467     sem a ->
 468     sem [a]
 469   default many1 ::
 470     FromDerived1 Repeatable sem =>
 471     sem a ->
 472     sem [a]
 473
 474 -- | Alias to 'many0'.
 475 many :: Repeatable sem => sem a -> sem [a]
 476 many = many0
 477
 478 -- | Alias to 'many1'.
 479 some :: Repeatable sem => sem a -> sem [a]
 480 some = many1
 481
 482 -- * Class 'Permutable'
 483 class Permutable sem where
 484   -- Use @TypeFamilyDependencies@ to help type-inference infer @(sem)@.
 485   type Permutation (sem :: Semantic) = (r :: Semantic) | r -> sem
 486   type Permutation sem = Permutation (Derived sem)
 487   permutable :: Permutation sem a -> sem a
 488   perm :: sem a -> Permutation sem a
 489   noPerm :: Permutation sem ()
 490   permWithDefault :: a -> sem a -> Permutation sem a
 491   optionalPerm ::
 492     Eitherable sem =>
 493     IsoFunctor sem =>
 494     Permutable sem =>
 495     sem a ->
 496     Permutation sem (Maybe a)
 497   optionalPerm = permWithDefault Nothing Fun.. (<%>) (Iso Just fromJust)
 498
 499 (<&>) ::
 500   Permutable sem =>
 501   ProductFunctor (Permutation sem) =>
 502   sem a ->
 503   Permutation sem b ->
 504   Permutation sem (a, b)
 505 x <&> y = perm x <.> y
 506 infixr 4 <&>
 507 {-# INLINE (<&>) #-}
 508
 509 (<?&>) ::
 510   Eitherable sem =>
 511   IsoFunctor sem =>
 512   Permutable sem =>
 513   ProductFunctor (Permutation sem) =>
 514   sem a ->
 515   Permutation sem b ->
 516   Permutation sem (Maybe a, b)
 517 x <?&> y = optionalPerm x <.> y
 518 infixr 4 <?&>
 519 {-# INLINE (<?&>) #-}
 520
 521 (<*&>) ::
 522   Eitherable sem =>
 523   Repeatable sem =>
 524   IsoFunctor sem =>
 525   Permutable sem =>
 526   ProductFunctor (Permutation sem) =>
 527   sem a ->
 528   Permutation sem b ->
 529   Permutation sem ([a], b)
 530 x <*&> y = permWithDefault [] (many1 x) <.> y
 531 infixr 4 <*&>
 532 {-# INLINE (<*&>) #-}
 533
 534 (<+&>) ::
 535   Eitherable sem =>
 536   Repeatable sem =>
 537   IsoFunctor sem =>
 538   Permutable sem =>
 539   ProductFunctor (Permutation sem) =>
 540   sem a ->
 541   Permutation sem b ->
 542   Permutation sem ([a], b)
 543 x <+&> y = perm (many1 x) <.> y
 544 infixr 4 <+&>
 545 {-# INLINE (<+&>) #-}
 546
 547 -- * Class 'Voidable'
 548 class Voidable sem where
 549   -- | Useful to supply @(a)@ to a @(sem)@ consuming @(a)@,
 550   -- for example in the format of a printing interpreter.
 551   void :: a -> sem a -> sem ()
 552   void = liftDerived1 Fun.. void
 553   default void ::
 554     FromDerived1 Voidable sem =>
 555     a ->
 556     sem a ->
 557     sem ()
 558
 559 -- * Class 'Substractable'
 560 class Substractable sem where
 561   (<->) :: sem a -> sem b -> sem a
 562   infixr 3 <->
 563   (<->) = liftDerived2 (<->)
 564   default (<->) ::
 565     FromDerived2 Substractable sem =>
 566     sem a ->
 567     sem b ->
 568     sem a