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