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