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 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   data_ :: Generic a => RepOfEoT 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 => 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