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