From: Julien Moutinho Date: Wed, 27 Sep 2023 23:48:22 +0000 (+0200) Subject: iface: add many `Forall` instances X-Git-Url: https://git.sourcephile.fr/haskell/symantic-base.git/commitdiff_plain iface: add many `Forall` instances --- diff --git a/src/Symantic/Semantics/Forall.hs b/src/Symantic/Semantics/Forall.hs index c959c5f..ae64ac3 100644 --- a/src/Symantic/Semantics/Forall.hs +++ b/src/Symantic/Semantics/Forall.hs @@ -16,32 +16,58 @@ import Control.Applicative (Applicative (..)) import Control.Monad (Monad (..)) import Data.Bool (Bool (..)) import Data.Eq (Eq (..)) +import Data.Eq qualified as Eq +import Data.Function qualified as Fun import Data.Functor (Functor (..)) import Data.Kind (Type) +import Data.Tuple qualified as Tuple import Text.Show (Show (..)) import Unsafe.Coerce (unsafeCoerce) -import qualified Data.Function as Fun -import Symantic.Syntaxes.Classes (Abstractable (..), Syntax, Syntaxes, Instantiable (..), Unabstractable (..)) +import Symantic.Syntaxes.Classes -- * Type 'Forall' newtype Forall (syns :: [Syntax]) (a :: Type) = Forall (forall sem. Syntaxes syns sem => sem a) +{-# INLINE forall1 #-} +forall1 :: + (forall sem. Syntaxes syns sem => sem a -> sem b) -> + Forall syns a -> Forall syns b +forall1 f (Forall a) = Forall (f a) + +{-# INLINE forall2 #-} +forall2 :: + (forall sem. Syntaxes syns sem => sem a -> sem b -> sem c) -> + Forall syns a -> Forall syns b -> Forall syns c +forall2 f (Forall a) (Forall b) = Forall (f a b) + +{-# INLINE forall3 #-} +forall3 :: + (forall sem. Syntaxes syns sem => sem a -> sem b -> sem c -> sem d) -> + Forall syns a -> Forall syns b -> Forall syns c -> Forall syns d +forall3 f (Forall a) (Forall b) (Forall c) = Forall (f a b c) + +{-# INLINE forall4 #-} +forall4 :: + (forall sem. Syntaxes syns sem => sem a -> sem b -> sem c -> sem d -> sem e) -> + Forall syns a -> Forall syns b -> Forall syns c -> Forall syns d -> Forall syns e +forall4 f (Forall a) (Forall b) (Forall c) (Forall d) = Forall (f a b c d) + instance ( forall sem. Syntaxes syns sem => Functor sem ) => Functor (Forall syns) where - fmap f (Forall sem) = Forall (fmap f sem) - a <$ (Forall sem) = Forall (a <$ sem) + fmap f = forall1 (fmap f) + (<$) a = forall1 (a <$) instance ( forall sem. Syntaxes syns sem => Applicative sem , Functor (Forall syns) ) => Applicative (Forall syns) where pure a = Forall (pure a) - liftA2 f (Forall a) (Forall b) = Forall (liftA2 f a b) - (<*>) (Forall f) (Forall a) = Forall ((<*>) f a) - (<*) (Forall f) (Forall a) = Forall ((<*) f a) - (*>) (Forall f) (Forall a) = Forall ((*>) f a) + liftA2 f = forall2 (liftA2 f) + (<*>) = forall2 (<*>) + (<*) = forall2 (<*) + (*>) = forall2 (*>) instance ( forall sem. Syntaxes syns sem => Monad sem , Applicative (Forall syns) @@ -49,11 +75,15 @@ instance (>>=) (Forall sa) f = Forall (sa >>= \a -> case f a of Forall sb -> sb) return = pure (>>) = (*>) +instance + ( forall sem. Syntaxes syns sem => Varable sem + ) => Varable (Forall syns) where + var = forall1 var instance (forall sem. Syntaxes syns sem => Instantiable sem) => Instantiable (Forall syns) where - Forall a2b .@ Forall a = Forall (a2b .@ a) + (.@) = forall2 (.@) instance ( forall sem. Syntaxes syns sem => Abstractable sem , forall sem. Syntaxes syns sem => Instantiable sem @@ -72,6 +102,87 @@ instance (.) = Forall (.) flip = Forall flip ($) = Forall ($) +instance + ( forall sem. Syntaxes syns sem => Constantable c sem + ) => Constantable c (Forall syns) where + constant c = Forall (constant c) +instance + ( forall sem. Syntaxes syns sem => Eitherable sem + ) => Eitherable (Forall syns) where + either = Forall either + left = Forall left + right = Forall right +instance + ( forall sem. Syntaxes syns sem => Equalable sem + ) => Equalable (Forall syns) where + equal = Forall equal +instance + ( forall sem. Syntaxes syns sem => IfThenElseable sem + ) => IfThenElseable (Forall syns) where + ifThenElse = forall3 ifThenElse +instance + ( forall sem. Syntaxes syns sem => Inferable c sem + ) => Inferable c (Forall syns) where + infer = Forall infer +instance + ( forall sem. Syntaxes syns sem => Listable sem + ) => Listable (Forall syns) where + cons = Forall cons + nil = Forall nil +instance + ( forall sem. Syntaxes syns sem => Maybeable sem + ) => Maybeable (Forall syns) where + just = Forall just + nothing = Forall nothing +instance + ( forall sem. Syntaxes syns sem => IsoFunctor sem + ) => IsoFunctor (Forall syns) where + (<%>) iso = forall1 (iso <%>) +instance + ( forall sem. Syntaxes syns sem => ProductFunctor sem + , forall sem. Syntaxes syns sem => IsoFunctor sem + , Syntaxes syns (Forall syns) + ) => ProductFunctor (Forall syns) where + (<.>) = forall2 (<.>) + ra <. rb = Iso Tuple.fst (,()) <%> (ra <.> rb) + ra .> rb = Iso Tuple.snd ((),) <%> (ra <.> rb) +instance + ( forall sem. Syntaxes syns sem => SumFunctor sem + ) => SumFunctor (Forall syns) where + (<+>) = forall2 (<+>) +instance + ( forall sem. Syntaxes syns sem => AlternativeFunctor sem + ) => AlternativeFunctor (Forall syns) where + (<|>) = forall2 (<|>) +instance + ( forall sem. Syntaxes syns sem => Dicurryable sem + ) => Dicurryable (Forall syns) where + dicurry args constr destr = forall1 (dicurry args constr destr) +instance + ( forall sem. Syntaxes syns sem => Emptyable sem + ) => Emptyable (Forall syns) where + empty = Forall empty +instance + ( forall sem. Syntaxes syns sem => Semigroupable sem + ) => Semigroupable (Forall syns) where + concat = Forall concat +instance + ( forall sem. Syntaxes syns sem => Optionable sem + ) => Optionable (Forall syns) where + optional = forall1 optional +instance + ( forall sem. Syntaxes syns sem => Repeatable sem + ) => Repeatable (Forall syns) where + many0 = forall1 many0 + many1 = forall1 many1 +instance + ( forall sem. Syntaxes syns sem => Substractable sem + ) => Substractable (Forall syns) where + (<->) = forall2 (<->) +instance + ( forall sem. Syntaxes syns sem => Voidable sem + ) => Voidable (Forall syns) where + void a = forall1 (void a) -- * Type 'PerSyntax' data PerSyntax :: [Syntax] -> (Syntax -> Type) -> Type where @@ -86,8 +197,8 @@ instance ) => Eq (PerSyntax (syn ': syns) a) where - PerSyntaxZ x == PerSyntaxZ y = x == y - PerSyntaxS x == PerSyntaxS y = x == y + PerSyntaxZ x == PerSyntaxZ y = x Eq.== y + PerSyntaxS x == PerSyntaxS y = x Eq.== y _ == _ = False instance Show (PerSyntax '[] a) where