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.ADT
  35 import Symantic.Syntaxes.CurryN
  36 import Symantic.Syntaxes.Derive
  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 -- * Class 'AlternativeFunctor'
 288
 289 -- | Beware that this is an @infixr@,
 290 -- not @infixl@ like 'Control.Applicative.<|>';
 291 -- this is to follow what is expected by 'ADT'.
 292 class AlternativeFunctor sem where
 293   (<|>) :: sem a -> sem a -> sem a
 294   infixr 3 <|>
 295   (<|>) = liftDerived2 (<|>)
 296   default (<|>) ::
 297     FromDerived2 AlternativeFunctor sem =>
 298     sem a ->
 299     sem a ->
 300     sem a
 301
 302 -- * Class 'Dicurryable'
 303 class Dicurryable sem where
 304   dicurry ::
 305     CurryN args =>
 306     proxy args ->
 307     (args -..-> a) -> -- construction
 308     (a -> Tuples args) -> -- destruction
 309     sem (Tuples args) ->
 310     sem a
 311   dicurry args constr destr = liftDerived1 (dicurry args constr destr)
 312   default dicurry ::
 313     FromDerived1 Dicurryable sem =>
 314     CurryN args =>
 315     proxy args ->
 316     (args -..-> a) ->
 317     (a -> Tuples args) ->
 318     sem (Tuples args) ->
 319     sem a
 320
 321 construct ::
 322   forall args a sem.
 323   Dicurryable sem =>
 324   Generic a =>
 325   EoTOfRep a =>
 326   CurryN args =>
 327   Tuples args ~ EoT (ADT a) =>
 328   (args ~ Args (args -..-> a)) =>
 329   (args -..-> a) ->
 330   sem (Tuples args) ->
 331   sem a
 332 construct f = dicurry (Proxy :: Proxy args) f eotOfadt
 333
 334 adt ::
 335   forall adt sem.
 336   IsoFunctor sem =>
 337   Generic adt =>
 338   RepOfEoT adt =>
 339   EoTOfRep adt =>
 340   sem (EoT (ADT adt)) ->
 341   sem adt
 342 adt = (<%>) (Iso adtOfeot eotOfadt)
 343
 344 -- * Class 'IfSemantic'
 345
 346 -- | 'IfSemantic' enables to change the 'Syntax' for a specific 'Semantic'.
 347 --
 348 -- Useful when a 'Semantic' does not implement some 'Syntax'es used by other 'Semantic's.
 349 class
 350   IfSemantic
 351     (thenSyntaxes :: [Syntax])
 352     (elseSyntaxes :: [Syntax])
 353     thenSemantic
 354     elseSemantic
 355   where
 356   ifSemantic ::
 357     (Syntaxes thenSyntaxes thenSemantic => thenSemantic a) ->
 358     (Syntaxes elseSyntaxes elseSemantic => elseSemantic a) ->
 359     elseSemantic a
 360
 361 instance
 362   {-# OVERLAPPING #-}
 363   Syntaxes thenSyntaxes thenSemantic =>
 364   IfSemantic thenSyntaxes elseSyntaxes thenSemantic thenSemantic
 365   where
 366   ifSemantic thenSyntax _elseSyntax = thenSyntax
 367 instance
 368   Syntaxes elseSyntaxes elseSemantic =>
 369   IfSemantic thenSyntaxes elseSyntaxes thenSemantic elseSemantic
 370   where
 371   ifSemantic _thenSyntax elseSyntax = elseSyntax
 372
 373 -- * Class 'Monoidable'
 374 class
 375   ( Emptyable sem
 376   , Semigroupable sem
 377   ) =>
 378   Monoidable sem
 379 instance
 380   ( Emptyable sem
 381   , Semigroupable sem
 382   ) =>
 383   Monoidable sem
 384
 385 -- ** Class 'Emptyable'
 386 class Emptyable sem where
 387   empty :: sem a
 388   empty = liftDerived empty
 389   default empty ::
 390     FromDerived Emptyable sem =>
 391     sem a
 392
 393 -- ** Class 'Semigroupable'
 394 class Semigroupable sem where
 395   concat :: Semigroup a => sem (a -> a -> a)
 396   concat = liftDerived concat
 397   default concat ::
 398     FromDerived Semigroupable sem =>
 399     Semigroup a =>
 400     sem (a -> a -> a)
 401
 402 infixr 6 `concat`, <>
 403 (<>) ::
 404   Abstractable sem =>
 405   Semigroupable sem =>
 406   Semigroup a =>
 407   sem a ->
 408   sem a ->
 409   sem a
 410 (<>) x y = concat .@ x .@ y
 411
 412 -- ** Class 'Optionable'
 413 class Optionable sem where
 414   optional :: sem a -> sem (Maybe a)
 415   optional = liftDerived1 optional
 416   default optional ::
 417     FromDerived1 Optionable sem =>
 418     sem a ->
 419     sem (Maybe a)
 420
 421 -- * Class 'Repeatable'
 422 class Repeatable sem where
 423   many0 :: sem a -> sem [a]
 424   many1 :: sem a -> sem [a]
 425   many0 = liftDerived1 many0
 426   many1 = liftDerived1 many1
 427   default many0 ::
 428     FromDerived1 Repeatable sem =>
 429     sem a ->
 430     sem [a]
 431   default many1 ::
 432     FromDerived1 Repeatable sem =>
 433     sem a ->
 434     sem [a]
 435
 436 -- | Alias to 'many0'.
 437 many :: Repeatable sem => sem a -> sem [a]
 438 many = many0
 439
 440 -- | Alias to 'many1'.
 441 some :: Repeatable sem => sem a -> sem [a]
 442 some = many1
 443
 444 -- * Class 'Permutable'
 445 class Permutable sem where
 446   -- Use @TypeFamilyDependencies@ to help type-inference infer @(sem)@.
 447   type Permutation (sem :: Semantic) = (r :: Semantic) | r -> sem
 448   type Permutation sem = Permutation (Derived sem)
 449   permutable :: Permutation sem a -> sem a
 450   perm :: sem a -> Permutation sem a
 451   noPerm :: Permutation sem ()
 452   permWithDefault :: a -> sem a -> Permutation sem a
 453   optionalPerm ::
 454     Eitherable sem =>
 455     IsoFunctor sem =>
 456     Permutable sem =>
 457     sem a ->
 458     Permutation sem (Maybe a)
 459   optionalPerm = permWithDefault Nothing Fun.. (<%>) (Iso Just fromJust)
 460
 461 (<&>) ::
 462   Permutable sem =>
 463   ProductFunctor (Permutation sem) =>
 464   sem a ->
 465   Permutation sem b ->
 466   Permutation sem (a, b)
 467 x <&> y = perm x <.> y
 468 infixr 4 <&>
 469 {-# INLINE (<&>) #-}
 470
 471 (<?&>) ::
 472   Eitherable sem =>
 473   IsoFunctor sem =>
 474   Permutable sem =>
 475   ProductFunctor (Permutation sem) =>
 476   sem a ->
 477   Permutation sem b ->
 478   Permutation sem (Maybe a, b)
 479 x <?&> y = optionalPerm x <.> y
 480 infixr 4 <?&>
 481 {-# INLINE (<?&>) #-}
 482
 483 (<*&>) ::
 484   Eitherable sem =>
 485   Repeatable sem =>
 486   IsoFunctor sem =>
 487   Permutable sem =>
 488   ProductFunctor (Permutation sem) =>
 489   sem a ->
 490   Permutation sem b ->
 491   Permutation sem ([a], b)
 492 x <*&> y = permWithDefault [] (many1 x) <.> y
 493 infixr 4 <*&>
 494 {-# INLINE (<*&>) #-}
 495
 496 (<+&>) ::
 497   Eitherable sem =>
 498   Repeatable sem =>
 499   IsoFunctor sem =>
 500   Permutable sem =>
 501   ProductFunctor (Permutation sem) =>
 502   sem a ->
 503   Permutation sem b ->
 504   Permutation sem ([a], b)
 505 x <+&> y = perm (many1 x) <.> y
 506 infixr 4 <+&>
 507 {-# INLINE (<+&>) #-}
 508
 509 -- * Class 'Routable'
 510 class Routable sem where
 511   (<!>) :: sem a -> sem b -> sem (a, b)
 512   infixr 4 <!>
 513   (<!>) = liftDerived2 (<!>)
 514   default (<!>) ::
 515     FromDerived2 Routable sem =>
 516     sem a ->
 517     sem b ->
 518     sem (a, b)
 519
 520 -- | Like @(,)@ but @infixr@.
 521 -- Mostly useful for clarity when using 'Routable'.
 522 pattern (:!:) :: a -> b -> (a, b)
 523 pattern a :!: b <-
 524   (a, b)
 525   where
 526     a :!: b = (a, b)
 527
 528 infixr 4 :!:
 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