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 -- | 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 adt ::
 345   forall adt sem.
 346   IsoFunctor sem =>
 347   Generic adt =>
 348   RepOfEoT adt =>
 349   EoTOfRep adt =>
 350   sem (EoT (ADT adt)) ->
 351   sem adt
 352 adt = (<%>) (Iso adtOfeot eotOfadt)
 353
 354 -- * Class 'IfSemantic'
 355
 356 -- | 'IfSemantic' enables to change the 'Syntax' for a specific 'Semantic'.
 357 --
 358 -- Useful when a 'Semantic' does not implement some 'Syntax'es used by other 'Semantic's.
 359 class
 360   IfSemantic
 361     (thenSyntaxes :: [Syntax])
 362     (elseSyntaxes :: [Syntax])
 363     thenSemantic
 364     elseSemantic
 365   where
 366   ifSemantic ::
 367     (Syntaxes thenSyntaxes thenSemantic => thenSemantic a) ->
 368     (Syntaxes elseSyntaxes elseSemantic => elseSemantic a) ->
 369     elseSemantic a
 370
 371 instance
 372   {-# OVERLAPPING #-}
 373   Syntaxes thenSyntaxes thenSemantic =>
 374   IfSemantic thenSyntaxes elseSyntaxes thenSemantic thenSemantic
 375   where
 376   ifSemantic thenSyntax _elseSyntax = thenSyntax
 377 instance
 378   Syntaxes elseSyntaxes elseSemantic =>
 379   IfSemantic thenSyntaxes elseSyntaxes thenSemantic elseSemantic
 380   where
 381   ifSemantic _thenSyntax elseSyntax = elseSyntax
 382
 383 -- * Class 'Monoidable'
 384 class
 385   ( Emptyable sem
 386   , Semigroupable sem
 387   ) =>
 388   Monoidable sem
 389 instance
 390   ( Emptyable sem
 391   , Semigroupable sem
 392   ) =>
 393   Monoidable sem
 394
 395 -- ** Class 'Emptyable'
 396 class Emptyable sem where
 397   empty :: sem a
 398   empty = liftDerived empty
 399   default empty ::
 400     FromDerived Emptyable sem =>
 401     sem a
 402
 403 -- ** Class 'Semigroupable'
 404 class Semigroupable sem where
 405   concat :: Semigroup a => sem (a -> a -> a)
 406   concat = liftDerived concat
 407   default concat ::
 408     FromDerived Semigroupable sem =>
 409     Semigroup a =>
 410     sem (a -> a -> a)
 411
 412 infixr 6 `concat`, <>
 413 (<>) ::
 414   Abstractable sem =>
 415   Semigroupable sem =>
 416   Semigroup a =>
 417   sem a ->
 418   sem a ->
 419   sem a
 420 (<>) x y = concat .@ x .@ y
 421
 422 -- ** Class 'Optionable'
 423 class Optionable sem where
 424   optional :: sem a -> sem (Maybe a)
 425   optional = liftDerived1 optional
 426   default optional ::
 427     FromDerived1 Optionable sem =>
 428     sem a ->
 429     sem (Maybe a)
 430
 431 -- * Class 'Repeatable'
 432 class Repeatable sem where
 433   many0 :: sem a -> sem [a]
 434   many1 :: sem a -> sem [a]
 435   many0 = liftDerived1 many0
 436   many1 = liftDerived1 many1
 437   default many0 ::
 438     FromDerived1 Repeatable sem =>
 439     sem a ->
 440     sem [a]
 441   default many1 ::
 442     FromDerived1 Repeatable sem =>
 443     sem a ->
 444     sem [a]
 445
 446 -- | Alias to 'many0'.
 447 many :: Repeatable sem => sem a -> sem [a]
 448 many = many0
 449
 450 -- | Alias to 'many1'.
 451 some :: Repeatable sem => sem a -> sem [a]
 452 some = many1
 453
 454 -- * Class 'Permutable'
 455 class Permutable sem where
 456   -- Use @TypeFamilyDependencies@ to help type-inference infer @(sem)@.
 457   type Permutation (sem :: Semantic) = (r :: Semantic) | r -> sem
 458   type Permutation sem = Permutation (Derived sem)
 459   permutable :: Permutation sem a -> sem a
 460   perm :: sem a -> Permutation sem a
 461   noPerm :: Permutation sem ()
 462   permWithDefault :: a -> sem a -> Permutation sem a
 463   optionalPerm ::
 464     Eitherable sem =>
 465     IsoFunctor sem =>
 466     Permutable sem =>
 467     sem a ->
 468     Permutation sem (Maybe a)
 469   optionalPerm = permWithDefault Nothing Fun.. (<%>) (Iso Just fromJust)
 470
 471 (<&>) ::
 472   Permutable sem =>
 473   ProductFunctor (Permutation sem) =>
 474   sem a ->
 475   Permutation sem b ->
 476   Permutation sem (a, b)
 477 x <&> y = perm x <.> y
 478 infixr 4 <&>
 479 {-# INLINE (<&>) #-}
 480
 481 (<?&>) ::
 482   Eitherable sem =>
 483   IsoFunctor sem =>
 484   Permutable sem =>
 485   ProductFunctor (Permutation sem) =>
 486   sem a ->
 487   Permutation sem b ->
 488   Permutation sem (Maybe a, b)
 489 x <?&> y = optionalPerm x <.> y
 490 infixr 4 <?&>
 491 {-# INLINE (<?&>) #-}
 492
 493 (<*&>) ::
 494   Eitherable sem =>
 495   Repeatable sem =>
 496   IsoFunctor sem =>
 497   Permutable sem =>
 498   ProductFunctor (Permutation sem) =>
 499   sem a ->
 500   Permutation sem b ->
 501   Permutation sem ([a], b)
 502 x <*&> y = permWithDefault [] (many1 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 = perm (many1 x) <.> y
 516 infixr 4 <+&>
 517 {-# INLINE (<+&>) #-}
 518
 519 -- * Class 'Voidable'
 520 class Voidable sem where
 521   -- | Useful to supply @(a)@ to a @(sem)@ consuming @(a)@,
 522   -- for example in the format of a printing interpreter.
 523   void :: a -> sem a -> sem ()
 524   void = liftDerived1 Fun.. void
 525   default void ::
 526     FromDerived1 Voidable sem =>
 527     a ->
 528     sem a ->
 529     sem ()
 530
 531 -- * Class 'Substractable'
 532 class Substractable sem where
 533   (<->) :: sem a -> sem b -> sem a
 534   infixr 3 <->
 535   (<->) = liftDerived2 (<->)
 536   default (<->) ::
 537     FromDerived2 Substractable sem =>
 538     sem a ->
 539     sem b ->
 540     sem a