-- For ifSemantic {-# LANGUAGE AllowAmbiguousTypes #-} -- For Syntax {-# LANGUAGE DataKinds #-} -- For (:!:) {-# LANGUAGE PatternSynonyms #-} -- For ifSemantic {-# LANGUAGE RankNTypes #-} -- For Permutation {-# LANGUAGE TypeFamilyDependencies #-} -- For Permutation {-# LANGUAGE UndecidableInstances #-} -- | This module gathers commonly used tagless-final combinators -- (the syntax part of symantics). -- -- Note: combinators in this module conflict with usual ones from the @Prelude@ -- hence they are meant to be imported either explicitely or qualified. module Symantic.Syntaxes.Classes where import Control.Category qualified as Cat import Data.Bool (Bool (..)) import Data.Char (Char) import Data.Either (Either (..)) import Data.Eq (Eq) import Data.Function qualified as Fun import Data.Int (Int) import Data.Kind (Constraint) import Data.Maybe (Maybe (..), fromJust) import Data.Proxy (Proxy (..)) import Data.Semigroup (Semigroup) import Data.String (String) import Data.Tuple qualified as Tuple import GHC.Generics (Generic) import Numeric.Natural (Natural) import Symantic.Syntaxes.CurryN import Symantic.Syntaxes.Derive import Symantic.Syntaxes.EithersOfTuples -- * Type 'Syntax' type Syntax = Semantic -> Constraint -- ** Type family 'Syntaxes' -- | Merge several 'Syntax'es into a single one. -- -- Useful in 'IfSemantic' or 'All'. type family Syntaxes (syns :: [Syntax]) (sem :: Semantic) :: Constraint where Syntaxes '[] sem = (() :: Constraint) Syntaxes (syn ': syns) sem = ((syn sem, Syntaxes syns sem) :: Constraint) -- * Class 'Abstractable' class Abstractable sem where -- | Lambda term abstraction, in HOAS (Higher-Order Abstract Syntax) style. lam :: (sem a -> sem b) -> sem (a -> b) lam f = liftDerived (lam (derive Fun.. f Fun.. liftDerived)) default lam :: FromDerived Abstractable sem => Derivable sem => (sem a -> sem b) -> sem (a -> b) -- ** Class 'Abstractable1' class Abstractable1 sem where -- | Like 'lam' but whose argument must be used only once, -- hence safe to beta-reduce (inline) without duplicating work. lam1 :: (sem a -> sem b) -> sem (a -> b) lam1 f = liftDerived (lam1 (derive Fun.. f Fun.. liftDerived)) default lam1 :: FromDerived Abstractable1 sem => Derivable sem => (sem a -> sem b) -> sem (a -> b) -- ** Class 'Varable' class Varable sem where -- | Mark the use of a variable. var :: sem a -> sem a var = liftDerived1 var default var :: FromDerived1 Varable sem => sem a -> sem a -- ** Class 'Instantiable' class Instantiable sem where -- | Instantiate. (.@) :: sem (a -> b) -> sem a -> sem b infixl 9 .@ (.@) = liftDerived2 (.@) default (.@) :: FromDerived2 Instantiable sem => sem (a -> b) -> sem a -> sem b -- ** Class 'Unabstractable' -- | All operations in lambda calculus can be encoded -- via abstraction elimination into the SK calculus -- as binary trees whose leaves are one -- of the three symbols S ('ap') and K ('const'). class Unabstractable sem where -- | S ap :: sem ((a -> b -> c) -> (a -> b) -> a -> c) -- | K const :: sem (a -> b -> a) -- | I id :: sem (a -> a) -- | B (.) :: sem ((b -> c) -> (a -> b) -> a -> c) infixr 9 . -- | C flip :: sem ((a -> b -> c) -> b -> a -> c) ($) :: sem ((a -> b) -> a -> b) infixr 0 $ ap = liftDerived ap const = liftDerived const id = liftDerived id (.) = liftDerived (.) flip = liftDerived flip ($) = liftDerived ($) default ap :: FromDerived Unabstractable sem => sem ((a -> b -> c) -> (a -> b) -> a -> c) default const :: FromDerived Unabstractable sem => sem (a -> b -> a) default id :: FromDerived Unabstractable sem => sem (a -> a) default (.) :: FromDerived Unabstractable sem => sem ((b -> c) -> (a -> b) -> a -> c) default flip :: FromDerived Unabstractable sem => sem ((a -> b -> c) -> b -> a -> c) default ($) :: FromDerived Unabstractable sem => sem ((a -> b) -> a -> b) -- * Class 'Anythingable' class Anythingable sem where anything :: sem a -> sem a anything = Fun.id -- * Class 'Bottomable' class Bottomable sem where bottom :: sem a -- * Class 'Constantable' class Constantable c sem where constant :: c -> sem c constant = liftDerived Fun.. constant default constant :: FromDerived (Constantable c) sem => c -> sem c -- * Class 'Eitherable' class Eitherable sem where either :: sem ((l -> a) -> (r -> a) -> Either l r -> a) left :: sem (l -> Either l r) right :: sem (r -> Either l r) either = liftDerived either left = liftDerived left right = liftDerived right default either :: FromDerived Eitherable sem => sem ((l -> a) -> (r -> a) -> Either l r -> a) default left :: FromDerived Eitherable sem => sem (l -> Either l r) default right :: FromDerived Eitherable sem => sem (r -> Either l r) -- * Class 'Equalable' class Equalable sem where equal :: Eq a => sem (a -> a -> Bool) equal = liftDerived equal default equal :: FromDerived Equalable sem => Eq a => sem (a -> a -> Bool) infix 4 `equal`, == (==) :: Instantiable sem => Equalable sem => Eq a => sem a -> sem a -> sem Bool (==) x y = equal .@ x .@ y -- * Class 'IfThenElseable' class IfThenElseable sem where ifThenElse :: sem Bool -> sem a -> sem a -> sem a ifThenElse = liftDerived3 ifThenElse default ifThenElse :: FromDerived3 IfThenElseable sem => sem Bool -> sem a -> sem a -> sem a -- * Class 'Inferable' class Inferable a sem where infer :: sem a default infer :: FromDerived (Inferable a) sem => sem a infer = liftDerived infer unit :: Inferable () sem => sem () unit = infer bool :: Inferable Bool sem => sem Bool bool = infer char :: Inferable Char sem => sem Char char = infer int :: Inferable Int sem => sem Int int = infer natural :: Inferable Natural sem => sem Natural natural = infer string :: Inferable String sem => sem String string = infer -- * Class 'Listable' class Listable sem where cons :: sem (a -> [a] -> [a]) nil :: sem [a] cons = liftDerived cons nil = liftDerived nil default cons :: FromDerived Listable sem => sem (a -> [a] -> [a]) default nil :: FromDerived Listable sem => sem [a] -- * Class 'Maybeable' class Maybeable sem where nothing :: sem (Maybe a) just :: sem (a -> Maybe a) nothing = liftDerived nothing just = liftDerived just default nothing :: FromDerived Maybeable sem => sem (Maybe a) default just :: FromDerived Maybeable sem => sem (a -> Maybe a) -- * Class 'IsoFunctor' class IsoFunctor sem where (<%>) :: Iso a b -> sem a -> sem b infixl 4 <%> (<%>) iso = liftDerived1 (iso <%>) default (<%>) :: FromDerived1 IsoFunctor sem => Iso a b -> sem a -> sem b -- ** Type 'Iso' data Iso a b = Iso {a2b :: a -> b, b2a :: b -> a} instance Cat.Category Iso where id = Iso Cat.id Cat.id f . g = Iso (a2b f Cat.. a2b g) (b2a g Cat.. b2a f) -- * Class 'ProductFunctor' -- | Beware that this is an @infixr@, -- not @infixl@ like 'Control.Applicative.<*>'; -- this is to follow what is expected by 'ADT'. class ProductFunctor sem where (<.>) :: sem a -> sem b -> sem (a, b) infixr 4 <.> (<.>) = liftDerived2 (<.>) default (<.>) :: FromDerived2 ProductFunctor sem => sem a -> sem b -> sem (a, b) (<.) :: sem a -> sem () -> sem a infixr 4 <. ra <. rb = Iso Tuple.fst (,()) <%> (ra <.> rb) default (<.) :: IsoFunctor sem => sem a -> sem () -> sem a (.>) :: sem () -> sem a -> sem a infixr 4 .> ra .> rb = Iso Tuple.snd ((),) <%> (ra <.> rb) default (.>) :: IsoFunctor sem => sem () -> sem a -> sem a -- * Class 'SumFunctor' -- | Beware that this is an @infixr@, -- not @infixl@ like 'Control.Applicative.<|>'; -- this is to follow what is expected by 'ADT'. class SumFunctor sem where (<+>) :: sem a -> sem b -> sem (Either a b) infixr 3 <+> (<+>) = liftDerived2 (<+>) default (<+>) :: FromDerived2 SumFunctor sem => sem a -> sem b -> sem (Either a b) -- | Like @(,)@ but @infixr@. -- Mostly useful for clarity when using 'SumFunctor'. pattern (:!:) :: a -> b -> (a, b) pattern a :!: b <- (a, b) where a :!: b = (a, b) infixr 4 :!: {-# COMPLETE (:!:) #-} -- * Class 'AlternativeFunctor' -- | Beware that this is an @infixr@, -- not @infixl@ like 'Control.Applicative.<|>'; -- this is to follow what is expected by 'ADT'. class AlternativeFunctor sem where (<|>) :: sem a -> sem a -> sem a infixr 3 <|> (<|>) = liftDerived2 (<|>) default (<|>) :: FromDerived2 AlternativeFunctor sem => sem a -> sem a -> sem a -- * Class 'Dicurryable' class Dicurryable sem where dicurry :: CurryN args => proxy args -> (args -..-> a) -> -- construction (a -> Tuples args) -> -- destruction sem (Tuples args) -> sem a dicurry args constr destr = liftDerived1 (dicurry args constr destr) default dicurry :: FromDerived1 Dicurryable sem => CurryN args => proxy args -> (args -..-> a) -> (a -> Tuples args) -> sem (Tuples args) -> sem a construct :: forall args a sem. Dicurryable sem => Generic a => EoTOfRep a => CurryN args => Tuples args ~ EoT (ADT a) => (args ~ Args (args -..-> a)) => (args -..-> a) -> sem (Tuples args) -> sem a construct f = dicurry (Proxy :: Proxy args) f eotOfadt -- * Class 'Dataable' -- | Enable the contruction or deconstruction -- of an 'ADT' (algebraic data type). class Dataable a sem where dataType :: sem (EoT (ADT a)) -> sem a default dataType :: Generic a => RepOfEoT a => EoTOfRep a => IsoFunctor sem => sem (EoT (ADT a)) -> sem a dataType = (<%>) (Iso adtOfeot eotOfadt) -- * Class 'IfSemantic' -- | 'IfSemantic' enables to change the 'Syntax' for a specific 'Semantic'. -- -- Useful when a 'Semantic' does not implement some 'Syntax'es used by other 'Semantic's. class IfSemantic (thenSyntaxes :: [Syntax]) (elseSyntaxes :: [Syntax]) thenSemantic elseSemantic where ifSemantic :: (Syntaxes thenSyntaxes thenSemantic => thenSemantic a) -> (Syntaxes elseSyntaxes elseSemantic => elseSemantic a) -> elseSemantic a instance {-# OVERLAPPING #-} Syntaxes thenSyntaxes thenSemantic => IfSemantic thenSyntaxes elseSyntaxes thenSemantic thenSemantic where ifSemantic thenSyntax _elseSyntax = thenSyntax instance Syntaxes elseSyntaxes elseSemantic => IfSemantic thenSyntaxes elseSyntaxes thenSemantic elseSemantic where ifSemantic _thenSyntax elseSyntax = elseSyntax -- * Class 'Monoidable' class ( Emptyable sem , Semigroupable sem ) => Monoidable sem instance ( Emptyable sem , Semigroupable sem ) => Monoidable sem -- ** Class 'Emptyable' class Emptyable sem where empty :: sem a empty = liftDerived empty default empty :: FromDerived Emptyable sem => sem a -- ** Class 'Semigroupable' class Semigroupable sem where concat :: Semigroup a => sem (a -> a -> a) concat = liftDerived concat default concat :: FromDerived Semigroupable sem => Semigroup a => sem (a -> a -> a) infixr 6 `concat`, <> (<>) :: Instantiable sem => Semigroupable sem => Semigroup a => sem a -> sem a -> sem a (<>) x y = concat .@ x .@ y -- ** Class 'Optionable' class Optionable sem where optional :: sem a -> sem (Maybe a) optional = liftDerived1 optional default optional :: FromDerived1 Optionable sem => sem a -> sem (Maybe a) -- * Class 'Repeatable' class Repeatable sem where many0 :: sem a -> sem [a] many1 :: sem a -> sem [a] many0 = liftDerived1 many0 many1 = liftDerived1 many1 default many0 :: FromDerived1 Repeatable sem => sem a -> sem [a] default many1 :: FromDerived1 Repeatable sem => sem a -> sem [a] -- | Alias to 'many0'. many :: Repeatable sem => sem a -> sem [a] many = many0 -- | Alias to 'many1'. some :: Repeatable sem => sem a -> sem [a] some = many1 -- * Class 'Permutable' class Permutable sem where -- Use @TypeFamilyDependencies@ to help type-inference infer @(sem)@. type Permutation (sem :: Semantic) = (r :: Semantic) | r -> sem type Permutation sem = Permutation (Derived sem) permutable :: Permutation sem a -> sem a perm :: sem a -> Permutation sem a noPerm :: Permutation sem () permWithDefault :: a -> sem a -> Permutation sem a optionalPerm :: Eitherable sem => IsoFunctor sem => Permutable sem => sem a -> Permutation sem (Maybe a) optionalPerm = permWithDefault Nothing Fun.. (<%>) (Iso Just fromJust) (<&>) :: Permutable sem => ProductFunctor (Permutation sem) => sem a -> Permutation sem b -> Permutation sem (a, b) x <&> y = perm x <.> y infixr 4 <&> {-# INLINE (<&>) #-} () :: Eitherable sem => IsoFunctor sem => Permutable sem => ProductFunctor (Permutation sem) => sem a -> Permutation sem b -> Permutation sem (Maybe a, b) x y = optionalPerm x <.> y infixr 4 {-# INLINE () #-} (<*&>) :: Eitherable sem => Repeatable sem => IsoFunctor sem => Permutable sem => ProductFunctor (Permutation sem) => sem a -> Permutation sem b -> Permutation sem ([a], b) x <*&> y = permWithDefault [] (many1 x) <.> y infixr 4 <*&> {-# INLINE (<*&>) #-} (<+&>) :: Eitherable sem => Repeatable sem => IsoFunctor sem => Permutable sem => ProductFunctor (Permutation sem) => sem a -> Permutation sem b -> Permutation sem ([a], b) x <+&> y = perm (many1 x) <.> y infixr 4 <+&> {-# INLINE (<+&>) #-} -- * Class 'Voidable' class Voidable sem where -- | Useful to supply @(a)@ to a @(sem)@ consuming @(a)@, -- for example in the format of a printing interpreter. void :: a -> sem a -> sem () void = liftDerived1 Fun.. void default void :: FromDerived1 Voidable sem => a -> sem a -> sem () -- * Class 'Substractable' class Substractable sem where (<->) :: sem a -> sem b -> sem a infixr 3 <-> (<->) = liftDerived2 (<->) default (<->) :: FromDerived2 Substractable sem => sem a -> sem b -> sem a