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   left :: sem (l -> Either l r)
 142   right :: sem (r -> Either l r)
 143   left = liftDerived left
 144   right = liftDerived right
 145   default left ::
 146     FromDerived Eitherable sem =>
 147     sem (l -> Either l r)
 148   default right ::
 149     FromDerived Eitherable sem =>
 150     sem (r -> Either l r)
 151
 152 -- * Class 'Equalable'
 153 class Equalable sem where
 154   equal :: Eq a => sem (a -> a -> Bool)
 155   equal = liftDerived equal
 156   default equal ::
 157     FromDerived Equalable sem =>
 158     Eq a =>
 159     sem (a -> a -> Bool)
 160
 161 infix 4 `equal`, ==
 162 (==) ::
 163   Abstractable sem =>
 164   Equalable sem =>
 165   Eq a =>
 166   sem a ->
 167   sem a ->
 168   sem Bool
 169 (==) x y = equal .@ x .@ y
 170
 171 -- * Class 'IfThenElseable'
 172 class IfThenElseable sem where
 173   ifThenElse :: sem Bool -> sem a -> sem a -> sem a
 174   ifThenElse = liftDerived3 ifThenElse
 175   default ifThenElse ::
 176     FromDerived3 IfThenElseable sem =>
 177     sem Bool ->
 178     sem a ->
 179     sem a ->
 180     sem a
 181
 182 -- * Class 'Inferable'
 183 class Inferable a sem where
 184   infer :: sem a
 185   default infer :: FromDerived (Inferable a) sem => sem a
 186   infer = liftDerived infer
 187
 188 unit :: Inferable () sem => sem ()
 189 unit = infer
 190 bool :: Inferable Bool sem => sem Bool
 191 bool = infer
 192 char :: Inferable Char sem => sem Char
 193 char = infer
 194 int :: Inferable Int sem => sem Int
 195 int = infer
 196 natural :: Inferable Natural sem => sem Natural
 197 natural = infer
 198 string :: Inferable String sem => sem String
 199 string = infer
 200
 201 -- * Class 'Listable'
 202 class Listable sem where
 203   cons :: sem (a -> [a] -> [a])
 204   nil :: sem [a]
 205   cons = liftDerived cons
 206   nil = liftDerived nil
 207   default cons ::
 208     FromDerived Listable sem =>
 209     sem (a -> [a] -> [a])
 210   default nil ::
 211     FromDerived Listable sem =>
 212     sem [a]
 213
 214 -- * Class 'Maybeable'
 215 class Maybeable sem where
 216   nothing :: sem (Maybe a)
 217   just :: sem (a -> Maybe a)
 218   nothing = liftDerived nothing
 219   just = liftDerived just
 220   default nothing ::
 221     FromDerived Maybeable sem =>
 222     sem (Maybe a)
 223   default just ::
 224     FromDerived Maybeable sem =>
 225     sem (a -> Maybe a)
 226
 227 -- * Class 'IsoFunctor'
 228 class IsoFunctor sem where
 229   (<%>) :: Iso a b -> sem a -> sem b
 230   infixl 4 <%>
 231   (<%>) iso = liftDerived1 (iso <%>)
 232   default (<%>) ::
 233     FromDerived1 IsoFunctor sem =>
 234     Iso a b ->
 235     sem a ->
 236     sem b
 237
 238 -- ** Type 'Iso'
 239 data Iso a b = Iso {a2b :: a -> b, b2a :: b -> a}
 240 instance Cat.Category Iso where
 241   id = Iso Cat.id Cat.id
 242   f . g = Iso (a2b f Cat.. a2b g) (b2a g Cat.. b2a f)
 243
 244 -- * Class 'ProductFunctor'
 245
 246 -- | Beware that this is an @infixr@,
 247 -- not @infixl@ like 'Control.Applicative.<*>';
 248 -- this is to follow what is expected by 'ADT'.
 249 class ProductFunctor sem where
 250   (<.>) :: sem a -> sem b -> sem (a, b)
 251   infixr 4 <.>
 252   (<.>) = liftDerived2 (<.>)
 253   default (<.>) ::
 254     FromDerived2 ProductFunctor sem =>
 255     sem a ->
 256     sem b ->
 257     sem (a, b)
 258   (<.) :: sem a -> sem () -> sem a
 259   infixr 4 <.
 260   ra <. rb = Iso Tuple.fst (,()) <%> (ra <.> rb)
 261   default (<.) :: IsoFunctor sem => sem a -> sem () -> sem a
 262   (.>) :: sem () -> sem a -> sem a
 263   infixr 4 .>
 264   ra .> rb = Iso Tuple.snd ((),) <%> (ra <.> rb)
 265   default (.>) :: IsoFunctor sem => sem () -> sem a -> sem a
 266
 267 -- * Class 'SumFunctor'
 268
 269 -- | Beware that this is an @infixr@,
 270 -- not @infixl@ like 'Control.Applicative.<|>';
 271 -- this is to follow what is expected by 'ADT'.
 272 class SumFunctor sem where
 273   (<+>) :: sem a -> sem b -> sem (Either a b)
 274   infixr 3 <+>
 275   (<+>) = liftDerived2 (<+>)
 276   default (<+>) ::
 277     FromDerived2 SumFunctor sem =>
 278     sem a ->
 279     sem b ->
 280     sem (Either a b)
 281
 282 -- * Class 'AlternativeFunctor'
 283
 284 -- | Beware that this is an @infixr@,
 285 -- not @infixl@ like 'Control.Applicative.<|>';
 286 -- this is to follow what is expected by 'ADT'.
 287 class AlternativeFunctor sem where
 288   (<|>) :: sem a -> sem a -> sem a
 289   infixr 3 <|>
 290   (<|>) = liftDerived2 (<|>)
 291   default (<|>) ::
 292     FromDerived2 AlternativeFunctor sem =>
 293     sem a ->
 294     sem a ->
 295     sem a
 296
 297 -- * Class 'Dicurryable'
 298 class Dicurryable sem where
 299   dicurry ::
 300     CurryN args =>
 301     proxy args ->
 302     (args -..-> a) -> -- construction
 303     (a -> Tuples args) -> -- destruction
 304     sem (Tuples args) ->
 305     sem a
 306   dicurry args constr destr = liftDerived1 (dicurry args constr destr)
 307   default dicurry ::
 308     FromDerived1 Dicurryable sem =>
 309     CurryN args =>
 310     proxy args ->
 311     (args -..-> a) ->
 312     (a -> Tuples args) ->
 313     sem (Tuples args) ->
 314     sem a
 315
 316 construct ::
 317   forall args a sem.
 318   Dicurryable sem =>
 319   Generic a =>
 320   EoTOfRep a =>
 321   CurryN args =>
 322   Tuples args ~ EoT (ADT a) =>
 323   (args ~ Args (args -..-> a)) =>
 324   (args -..-> a) ->
 325   sem (Tuples args) ->
 326   sem a
 327 construct f = dicurry (Proxy :: Proxy args) f eotOfadt
 328
 329 adt ::
 330   forall adt sem.
 331   IsoFunctor sem =>
 332   Generic adt =>
 333   RepOfEoT adt =>
 334   EoTOfRep adt =>
 335   sem (EoT (ADT adt)) ->
 336   sem adt
 337 adt = (<%>) (Iso adtOfeot eotOfadt)
 338
 339 -- * Class 'IfSemantic'
 340
 341 -- | 'IfSemantic' enables to change the 'Syntax' for a specific 'Semantic'.
 342 --
 343 -- Useful when a 'Semantic' does not implement some 'Syntax'es used by other 'Semantic's.
 344 class
 345   IfSemantic
 346     (thenSyntaxes :: [Syntax])
 347     (elseSyntaxes :: [Syntax])
 348     thenSemantic
 349     elseSemantic
 350   where
 351   ifSemantic ::
 352     (Syntaxes thenSyntaxes thenSemantic => thenSemantic a) ->
 353     (Syntaxes elseSyntaxes elseSemantic => elseSemantic a) ->
 354     elseSemantic a
 355
 356 instance
 357   {-# OVERLAPPING #-}
 358   Syntaxes thenSyntaxes thenSemantic =>
 359   IfSemantic thenSyntaxes elseSyntaxes thenSemantic thenSemantic
 360   where
 361   ifSemantic thenSyntax _elseSyntax = thenSyntax
 362 instance
 363   Syntaxes elseSyntaxes elseSemantic =>
 364   IfSemantic thenSyntaxes elseSyntaxes thenSemantic elseSemantic
 365   where
 366   ifSemantic _thenSyntax elseSyntax = elseSyntax
 367
 368 -- * Class 'Monoidable'
 369 class
 370   ( Emptyable sem
 371   , Semigroupable sem
 372   ) =>
 373   Monoidable sem
 374 instance
 375   ( Emptyable sem
 376   , Semigroupable sem
 377   ) =>
 378   Monoidable sem
 379
 380 -- ** Class 'Emptyable'
 381 class Emptyable sem where
 382   empty :: sem a
 383   empty = liftDerived empty
 384   default empty ::
 385     FromDerived Emptyable sem =>
 386     sem a
 387
 388 -- ** Class 'Semigroupable'
 389 class Semigroupable sem where
 390   concat :: Semigroup a => sem (a -> a -> a)
 391   concat = liftDerived concat
 392   default concat ::
 393     FromDerived Semigroupable sem =>
 394     Semigroup a =>
 395     sem (a -> a -> a)
 396
 397 infixr 6 `concat`, <>
 398 (<>) ::
 399   Abstractable sem =>
 400   Semigroupable sem =>
 401   Semigroup a =>
 402   sem a ->
 403   sem a ->
 404   sem a
 405 (<>) x y = concat .@ x .@ y
 406
 407 -- ** Class 'Optionable'
 408 class Optionable sem where
 409   optional :: sem a -> sem (Maybe a)
 410   optional = liftDerived1 optional
 411   default optional ::
 412     FromDerived1 Optionable sem =>
 413     sem a ->
 414     sem (Maybe a)
 415
 416 -- * Class 'Repeatable'
 417 class Repeatable sem where
 418   many0 :: sem a -> sem [a]
 419   many1 :: sem a -> sem [a]
 420   many0 = liftDerived1 many0
 421   many1 = liftDerived1 many1
 422   default many0 ::
 423     FromDerived1 Repeatable sem =>
 424     sem a ->
 425     sem [a]
 426   default many1 ::
 427     FromDerived1 Repeatable sem =>
 428     sem a ->
 429     sem [a]
 430
 431 -- | Alias to 'many0'.
 432 many :: Repeatable sem => sem a -> sem [a]
 433 many = many0
 434
 435 -- | Alias to 'many1'.
 436 some :: Repeatable sem => sem a -> sem [a]
 437 some = many1
 438
 439 -- * Class 'Permutable'
 440 class Permutable sem where
 441   -- Use @TypeFamilyDependencies@ to help type-inference infer @(sem)@.
 442   type Permutation (sem :: Semantic) = (r :: Semantic) | r -> sem
 443   type Permutation sem = Permutation (Derived sem)
 444   permutable :: Permutation sem a -> sem a
 445   perm :: sem a -> Permutation sem a
 446   noPerm :: Permutation sem ()
 447   permWithDefault :: a -> sem a -> Permutation sem a
 448   optionalPerm ::
 449     Eitherable sem =>
 450     IsoFunctor sem =>
 451     Permutable sem =>
 452     sem a ->
 453     Permutation sem (Maybe a)
 454   optionalPerm = permWithDefault Nothing Fun.. (<%>) (Iso Just fromJust)
 455
 456 (<&>) ::
 457   Permutable sem =>
 458   ProductFunctor (Permutation sem) =>
 459   sem a ->
 460   Permutation sem b ->
 461   Permutation sem (a, b)
 462 x <&> y = perm x <.> y
 463 infixr 4 <&>
 464 {-# INLINE (<&>) #-}
 465
 466 (<?&>) ::
 467   Eitherable sem =>
 468   IsoFunctor sem =>
 469   Permutable sem =>
 470   ProductFunctor (Permutation sem) =>
 471   sem a ->
 472   Permutation sem b ->
 473   Permutation sem (Maybe a, b)
 474 x <?&> y = optionalPerm x <.> y
 475 infixr 4 <?&>
 476 {-# INLINE (<?&>) #-}
 477
 478 (<*&>) ::
 479   Eitherable sem =>
 480   Repeatable sem =>
 481   IsoFunctor sem =>
 482   Permutable sem =>
 483   ProductFunctor (Permutation sem) =>
 484   sem a ->
 485   Permutation sem b ->
 486   Permutation sem ([a], b)
 487 x <*&> y = permWithDefault [] (many1 x) <.> y
 488 infixr 4 <*&>
 489 {-# INLINE (<*&>) #-}
 490
 491 (<+&>) ::
 492   Eitherable sem =>
 493   Repeatable sem =>
 494   IsoFunctor sem =>
 495   Permutable sem =>
 496   ProductFunctor (Permutation sem) =>
 497   sem a ->
 498   Permutation sem b ->
 499   Permutation sem ([a], b)
 500 x <+&> y = perm (many1 x) <.> y
 501 infixr 4 <+&>
 502 {-# INLINE (<+&>) #-}
 503
 504 -- * Class 'Routable'
 505 class Routable sem where
 506   (<!>) :: sem a -> sem b -> sem (a, b)
 507   infixr 4 <!>
 508   (<!>) = liftDerived2 (<!>)
 509   default (<!>) ::
 510     FromDerived2 Routable sem =>
 511     sem a ->
 512     sem b ->
 513     sem (a, b)
 514
 515 -- | Like @(,)@ but @infixr@.
 516 -- Mostly useful for clarity when using 'Routable'.
 517 pattern (:!:) :: a -> b -> (a, b)
 518 pattern a :!: b <-
 519   (a, b)
 520   where
 521     a :!: b = (a, b)
 522
 523 infixr 4 :!:
 524
 525 -- * Class 'Voidable'
 526 class Voidable sem where
 527   -- | Useful to supply @(a)@ to a @(sem)@ consuming @(a)@,
 528   -- for example in the format of a printing interpreter.
 529   void :: a -> sem a -> sem ()
 530   void = liftDerived1 Fun.. void
 531   default void ::
 532     FromDerived1 Voidable sem =>
 533     a ->
 534     sem a ->
 535     sem ()
 536
 537 -- * Class 'Substractable'
 538 class Substractable sem where
 539   (<->) :: sem a -> sem b -> sem a
 540   infixr 3 <->
 541   (<->) = liftDerived2 (<->)
 542   default (<->) ::
 543     FromDerived2 Substractable sem =>
 544     sem a ->
 545     sem b ->
 546     sem a