Haskus.Utils.EGADT

Documentation

>>> :set -XDataKinds
>>> :set -XTypeApplications
>>> :set -XTypeOperators
>>> :set -XFlexibleContexts
>>> :set -XTypeFamilies
>>> :set -XPatternSynonyms
>>> :set -XDeriveFunctor
>>> :set -XGADTs
>>> :set -XPolyKinds
>>> :set -XPartialTypeSignatures
>>> 
>>> :{
>>> data LamF (ast :: Type -> Type) t where
>>> LamF :: ( ast a -> ast b ) -> LamF ast ( a -> b )
>>> 
>>> data AppF ast t where
>>> AppF :: ast ( a -> b ) -> ast a -> AppF ast b
>>> 
>>> data VarF ast t where
>>> VarF :: String -> VarF ast Int
>>> 
>>> type AST a = EGADT '[LamF,AppF,VarF] a
>>> 
>>> :}

>>> let y = VF @(AST Int) (VarF "a")
>>> :t y
y :: EGADT '[LamF, AppF, VarF] Int

>>> :{
>>> case y of
>>> VF (VarF x) -> print x
>>> _           -> putStrLn "Not a VarF"
>>> :}
"a"

>>> :{
>>> f :: AST Int -> AST Int
>>> f (VF (VarF x)) = VF (VarF "zz")
>>> f _             = error "Unhandled case"
>>> :}

>>> let z = VF (AppF (VF (LamF f)) (VF (VarF "a")))
>>> :t z
z :: EGADT '[LamF, AppF, VarF] Int

newtype EGADT fs t

An EADT with an additional type parameter

Constructors

EGADT (HVariantF fs (EGADT fs) t)

Instances

HFunctor (HVariantF xs) => HRecursive (EGADT xs :: k -> Type)

Defined in Haskus.Utils.EGADT

Methods

hproject :: HCoalgebra (HBase (EGADT xs)) (EGADT xs)

hcata :: forall (f :: k0 -> Type). HAlgebra (HBase (EGADT xs)) f -> EGADT xs ~> f

HFunctor (HVariantF xs) => HCorecursive (EGADT xs :: k -> Type)

Defined in Haskus.Utils.EGADT

Methods

hembed :: HAlgebra (HBase (EGADT xs)) (EGADT xs)

hana :: forall (f :: k0 -> Type). HCoalgebra (HBase (EGADT xs)) f -> f ~> EGADT xs

type HBase (EGADT xs :: k -> Type)

Defined in Haskus.Utils.EGADT

type HBase (EGADT xs :: k -> Type) = HVariantF xs

newtype HVariantF (fs :: [(k -> Type) -> k -> Type]) (ast :: k -> Type) (t :: k)

Constructors

HVariantF (VariantF (ApplyAll ast fs) t)

toHVariantAt :: forall i fs ast a. KnownNat i => Index i fs ast a -> VariantF (ApplyAll ast fs) a

fromHVariantAt :: forall i fs ast a. KnownNat i => VariantF (ApplyAll ast fs) a -> Maybe (Index i fs ast a)

type family f :<! fs :: Constraint where ...

Equations

f :<! fs = MemberAtIndex (IndexOf f fs) f fs

type family MemberAtIndex (i :: Nat) f fs :: Constraint where ...

Equations

MemberAtIndex i f fs = (KnownNat i, Index i fs ~ f)

type family xs :<<! ys :: Constraint where ...

Equations

'[] :<<! ys = ()

(x ': xs) :<<! ys = (x :<! ys, xs :<<! ys)

pattern VF :: forall e a f fs. (e ~ EGADT fs a, f :<! fs) => f (EGADT fs) a -> EGADT fs a

Pattern-match in an extensible GADT