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