haskus-utils-variant-3.3: Variant and EADT
Safe HaskellNone
LanguageHaskell2010

Haskus.Utils.EGADT

Synopsis

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 Source #

An EADT with an additional type parameter

Constructors

EGADT (HVariantF fs (EGADT fs) t) 

Instances

Instances details
HFunctor (HVariantF xs) => HRecursive (EGADT xs :: k -> Type) Source # 
Instance details

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) Source # 
Instance details

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) Source # 
Instance details

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) Source #

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 Source #

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

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

Equations

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

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

Equations

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

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

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 Source #

Pattern-match in an extensible GADT