packages feed

variant 1.0.2 → 1.0.3

raw patch · 7 files changed

+1401/−264 lines, 7 files

Files

changelog.md view
@@ -1,3 +1,7 @@+## 1.0.3++- Migrated more documentation (EADT, EGADT)+ ## 1.0.2  - Migrated documentation from the old independent user manual into Haddocks
src/lib/Data/Variant.hs view
@@ -303,6 +303,35 @@ types and performs nothing at runtime; prepending only increases the tag value at runtime by a constant number. +The 'Concat' type family lets us write generic functions that extend an input+variant with a fixed set of additional types. For instance, here is a function+that turns specific 'Int' values into dedicated error constructors and forwards+everything else by appending the new error types to the input variant type:++> data Error0 = Error0 deriving Show+> data Error1 = Error1 deriving Show+>+> checkErr ::+>    ( Int :< is+>    , os ~ Concat is [Error0, Error1]+>    , Error0 :< os+>    , Error1 :< os+>    ) => V is -> V os+> checkErr = \case+>    V (0 :: Int) -> V Error0+>    V (1 :: Int) -> V Error1+>    v            -> appendVariant @[Error0, Error1] v+>+> > checkErr (V @Int 0 :: V [Float,Int])+> V @Error0 Error0+>+> > checkErr (V @Float 5.0 :: V [Float,Int])+> V @Float 5.0+>+> > :t checkErr (V @Float 5.0 :: V [Float,Int,String,Double])+> checkErr (V @Float 5.0 :: V [Float,Int,String,Double])+>    :: V [Float, Int, String, Double, Error0, Error1]+ === Variant lifting (extending and reordering)  We can extend and reorder the value types of a variant with 'liftVariant':
src/lib/Data/Variant/EADT.hs view
@@ -15,170 +15,1183 @@ {-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} --- | Extensible ADT-module Data.Variant.EADT-   ( EADT (..)-   , (:<:)-   , (:<<:)-   , pattern VF-   , appendEADT-   , liftEADT-   , popEADT-   , contToEADT-   , contToEADTM-   , EADTShow (..)-   , eadtShow-   -- * Reexport-   , module Data.Variant.Functor-   , module Data.Variant.VariantF-   )-where--import Data.Variant-import Data.Variant.VariantF-import Data.Variant.Types-import Data.Variant.ContFlow-import Data.Variant.Functor--import GHC.TypeLits---- $setup--- >>> :seti -XDataKinds--- >>> :seti -XTypeApplications--- >>> :seti -XTypeOperators--- >>> :seti -XFlexibleContexts--- >>> :seti -XTypeFamilies--- >>> :seti -XPatternSynonyms--- >>> :seti -XDeriveFunctor--- >>>--- >>> import Data.Functor.Classes--- >>>--- >>> data ConsF a e = ConsF a e deriving (Eq,Ord,Show,Functor)--- >>> data NilF    e = NilF      deriving (Eq,Ord,Show,Functor)--- >>>--- >>> instance Eq a => Eq1 (ConsF a) where liftEq cmp (ConsF a e1) (ConsF b e2) = a == b && cmp e1 e2--- >>> instance Eq1 NilF where liftEq _ _ _ = True--- >>>--- >>> :{--- >>> pattern Cons :: ConsF a :<: xs => a -> EADT xs -> EADT xs--- >>> pattern Cons a l = VF (ConsF a l)--- >>> pattern Nil :: NilF :<: xs => EADT xs--- >>> pattern Nil = VF NilF--- >>> type ListF a = VariantF '[NilF, ConsF a]--- >>> type List a = EADT '[NilF, ConsF a]--- >>> :}------ >>>--- >>> let a = Cons "Hello" (Cons "World" Nil) :: List String--- >>> let b = Cons "Bonjour" (Cons "Monde" Nil) :: List String--- >>> a == b--- False--- >>> a == a--- True----- | An extensible ADT-newtype EADT fs-   = EADT (VariantF fs (EADT fs))--type instance Base (EADT fs) = VariantF fs--instance Functor (VariantF fs) => Recursive (EADT fs) where-   project (EADT a) = a--instance Functor (VariantF fs) => Corecursive (EADT fs) where-   embed = EADT--instance Eq1 (VariantF fs) => Eq (EADT fs) where-  EADT a == EADT b = eq1 a b--instance Ord1 (VariantF fs) => Ord (EADT fs) where-  compare (EADT a) (EADT b) = compare1 a b--instance Show1 (VariantF fs) => Show (EADT fs) where-  showsPrec d (EADT a) =-    showParen (d >= 11)-      $ showString "EADT "-      . showsPrec1 11 a---- | Constructor `f` is in `xs`-type family f :<: xs where-   f :<: xs = EADTF' f (EADT xs) xs---- | Forall `x` in `xs`, `x :<: ys`-type family (:<<:) xs ys :: Constraint where-   '[] :<<: ys       = ()-   (x ': xs) :<<: ys = (x :<: ys, xs :<<: ys)--type EADTF' f e cs =-   ( Member f cs-   , Index (IndexOf (f e) (ApplyAll e cs)) (ApplyAll e cs) ~ f e-   , PopVariant (f e) (ApplyAll e cs)-   , KnownNat (IndexOf (f e) (ApplyAll e cs))-   , Remove (f e) (ApplyAll e cs) ~ ApplyAll e (Remove f cs)-   )---- | Pattern-match in an extensible ADT-pattern VF :: forall e f cs.-   ( e ~ EADT cs  -- allow easy use of TypeApplication to set the EADT type-   , f :<: cs     -- constraint synonym ensuring `f` is in `cs`-   ) => f (EADT cs) -> EADT cs-pattern VF x = EADT (VariantF (VSilent x))-   -- `VSilent` matches a variant value without checking the membership: we-   -- already do it with :<:---- | Append new "constructors" to the EADT-appendEADT :: forall ys xs zs.-   ( zs ~ Concat xs ys-   , ApplyAll (EADT zs) zs ~ Concat (ApplyAll (EADT zs) xs) (ApplyAll (EADT zs) ys)-   , Functor (VariantF xs)-   ) => EADT xs -> EADT zs-appendEADT (EADT v) = EADT (appendVariantF @ys (fmap (appendEADT @ys) v))---- | Lift an EADT into another-liftEADT :: forall e as bs.-   ( e ~ EADT bs-   , LiftVariantF as bs e-   , Functor (VariantF as)-   ) => EADT as -> EADT bs-liftEADT = cata (EADT . liftVariantF)---- | Pop an EADT value-popEADT :: forall f xs e.-   ( f :<: xs-   , e ~ EADT xs-   , f e :< ApplyAll e xs-   ) => EADT xs -> Either (VariantF (Remove f xs) (EADT xs)) (f (EADT xs))-popEADT (EADT v) = popVariantF v---- | MultiCont instance------ >>> let f x = toCont x >::> (const "[]", \(ConsF u us) -> u ++ ":" ++ f us)--- >>> f a--- "Hello:World:[]"-instance (Functor (VariantF xs), ContVariant (ApplyAll (EADT xs) xs)) => MultiCont (EADT xs) where-   type MultiContTypes (EADT xs) = ApplyAll (EADT xs) xs-   toCont  (EADT v) = variantFToCont v-   toContM f        = variantFToContM (project <$> f)---- | Convert a multi-continuation into an EADT-contToEADT ::-   ( ContVariant (ApplyAll (EADT xs) xs)-   ) => ContFlow (ApplyAll (EADT xs) xs)-                 (V (ApplyAll (EADT xs) xs))-     -> EADT xs-contToEADT c = EADT (contToVariantF c)---- | Convert a multi-continuation into an EADT-contToEADTM ::-   ( ContVariant (ApplyAll (EADT xs) xs)-   , Monad f-   ) => ContFlow (ApplyAll (EADT xs) xs)-                 (f (V (ApplyAll (EADT xs) xs)))-     -> f (EADT xs)-contToEADTM f = EADT <$> contToVariantFM f--+{- | Extensible ADT (EADT)++EADTs are \"extensible algebraic data types\": they can be transformed (by+adding or removing constructors) and their constructors are not tied to a+specific EADT type, hence we can use them as constructors of different EADTs.++EADT constructors and operations can be defined independently (even in+different modules) allowing a great modularity. As such they are an answer to+the \"expression problem\" (see __Background on EADTs__ at the bottom of this+page).++== Motivating example++Suppose we want to encode lambda-calculus using an ADT. We could use the+following one:++> data Expr n -- "n" represents a variable name+>    = Lambda n (Expr n)+>    | Var n+>    | App (Expr n) (Expr n)++We can define a pretty-print operation:++> prettyPrint :: Show n => Expr n -> String+> prettyPrint = \case+>    Var n      -> show n+>    Lambda n e -> mconcat ["\\",show n,".",prettyPrint e]+>    App e1 e2  -> mconcat ["(",prettyPrint e1,") (",prettyPrint e2,")"]++And we can test on an example:++> sampleDouble :: Expr String+> sampleDouble = Lambda "x" (Var "+" `App` Var "x" `App` Var "x")+>+> > putStrLn (prettyPrint sampleDouble)+> \"x".(("+") ("x")) ("x")++Now suppose that we want to add support for annotations. We can define a new+expression ADT with an additional constructor:++> data AExpr a n -- "n" represents a variable name, "a" represents an annotation+>    = ALambda n (AExpr a n)+>    | AVar n+>    | AApp (AExpr a n) (AExpr a n)+>    | Ann a (AExpr a n)++But now we need to rewrite our operations and expressions (such as+@prettyPrint@ and @sampleDouble@) to handle and to use the constructors of the+new expression ADT:++> prettyPrintA :: (Show n, Show a) => AExpr a n -> String+> prettyPrintA = \case+>    AVar n      -> show n+>    ALambda n e -> mconcat ["\\",show n,".",prettyPrintA e]+>    AApp e1 e2  -> mconcat ["(",prettyPrintA e1,") (",prettyPrintA e2,")"]+>    Ann a e     -> mconcat ["{",show a,"} ", prettyPrintA e]+>+> sampleDoubleA :: AExpr a String+> sampleDoubleA = ALambda "x" (AVar "+" `AApp` AVar "x" `AApp` AVar "x")+>+> sampleAnnA :: AExpr String String+> sampleAnnA = Ann "Double its input" sampleDoubleA++Now the problem is that we have two totally independent expression types+(@Expr@ and @AExpr@) with different operations (@prettyPrint@ vs+@prettyPrintA@) which can't be easily mixed. Moreover to define+@prettyPrintA@ we had to copy-paste @prettyPrint@ just to add a single case+alternative. Now suppose that we want to add a new function (e.g. to compute+free variables of an expression): should we implement it for @Expr@, for+@AExpr@, for both?++Finally suppose that we want to add some other constructors: we either get a+combinatorial explosion of ADTs and functions, or we give up on static checking+and use the \"largest\" ADT (which contains a superset of the constructors of+the others) with some conventions, e.g. comments and runtime assertions such as+\"at this point this expression shouldn't contain any annotation\" that are not+enforced by the compiler.++=== Motivating example with EADTs++The same example with EADTs would be written as follows. First we define the+EADTs:++> import Data.Variant.EADT+> import Data.Variant.EADT.TH+>+> data AbsF n e = AbsF n e deriving Functor+> data VarF n e = VarF n   deriving Functor+> data AppF   e = AppF e e deriving Functor+> data AnnF a e = AnnF a e deriving Functor+>+> eadtPattern 'AbsF "Abs"+> eadtPattern 'VarF "Var"+> eadtPattern 'AppF "App"+> eadtPattern 'AnnF "Ann"+>+> type Expr    n = EADT [AbsF n, VarF n, AppF]+> type AExpr a n = EADT [AbsF n, VarF n, AppF, AnnF a]++Then we define the @prettyPrint@ operation by using type classes:++> class PrettyPrint f where+>    prettyPrintF :: f String -> String+>+> instance Show n => PrettyPrint (VarF n) where+>    prettyPrintF (VarF n) = show n+>+> instance Show n => PrettyPrint (AbsF n) where+>    prettyPrintF (AbsF n e) = mconcat ["\\",show n,".",e]+>+> instance PrettyPrint AppF where+>    prettyPrintF (AppF e1 e2) = mconcat ["(",e1,") (",e2,")"]+>+> instance Show a => PrettyPrint (AnnF a) where+>    prettyPrintF (AnnF a e) = mconcat ["{",show a,"} ",e]+>+> prettyPrint :: BottomUpF PrettyPrint xs => EADT xs -> String+> prettyPrint e = bottomUp (toBottomUp @PrettyPrint prettyPrintF) e++We can test it with:++> sampleDouble :: Expr String+> sampleDouble = Abs "x" (Var "+" `App` Var "x" `App` Var "x")+>+> sampleAnn :: AExpr String String+> sampleAnn = Ann "Double its input" (liftEADT sampleDouble)+>+> > putStrLn (prettyPrint sampleDouble)+> \"x".(("+") ("x")) ("x")+>+> > putStrLn (prettyPrint sampleAnn)+> {"Double its input"} \"x".(("+") ("x")) ("x")++== EADT basics++EADTs are exposed by this module. The Template-Haskell helpers used to derive+pattern synonyms are in "Data.Variant.EADT.TH":++> import Data.Variant.EADT+> import Data.Variant.EADT.TH -- template-haskell helpers++=== Defining constructors++EADT constructors are data types that must have a 'Functor' type-class+instance. Fortunately defining such data types is easy thanks to the+@DeriveFunctor@ extension that automatically generates the 'Functor' instance+for us.++For instance, let's define the constructors for a list:++> {-# LANGUAGE DeriveFunctor #-}+>+> data ConsF a e = ConsF a e deriving (Functor)+> data NilF    e = NilF      deriving (Functor)++Note that __both__ data types are parameterised by @e@ even if @e@ isn't used+in the @NilF@ definition.++=== Defining pattern synonyms++We can match EADT values with the 'VF' pattern synonym (\"VF\" stands for+\"Variant Functor\"). To make the use of EADTs more pleasant, it is highly+recommended to define an additional pattern synonym for each constructor:++> pattern Cons :: ConsF a :<: xs => a -> EADT xs -> EADT xs+> pattern Cons a l = VF (ConsF a l)+>+> pattern Nil :: NilF :<: xs => EADT xs+> pattern Nil = VF NilF++These patterns hide the use of the 'VF' pattern and make the code much easier+to work with.++As this code is very straightforward to write, we provide Template-Haskell+helpers ('Data.Variant.EADT.TH.eadtPattern' and friends) to generate them+automatically. The previous patterns can be generated with:++> {-# LANGUAGE TemplateHaskell #-}+>+> import Data.Variant.EADT.TH+>+> eadtPattern 'ConsF "Cons"+> eadtPattern 'NilF  "Nil"++=== Defining the EADT++An EADT is just a type alias as in the following @List@ EADT example:++> type List a = EADT [ConsF a, NilF]++=== Creating values++Thanks to the pattern synonyms defined above, we can define values as we would+with a normal ADT:++> strList :: List String+> strList = Cons "How" (Cons "are" (Cons "you?" Nil))++In some cases we have to help the type-checker to determine some types. For+instance, in the following example it can't infer the @a@ type in @ConsF a@,+hence we have to use type ascriptions:++> intList :: List Int+> intList = Cons (10 :: Int) $ Cons (20 :: Int) $ Cons (30 :: Int) Nil++This is because the code is generic enough that the same pattern synonyms could+be used to build a heterogeneous list. For instance containing both @Int@ and+@Float@:++> mixedList :: EADT [ConsF Int, ConsF Float, NilF]+> mixedList = Cons (10 :: Int) $ Cons (5.0 :: Float) $ Cons (30 :: Int) Nil++We could also easily define another pattern synonym when we work on @List@ to+help the inference algorithm:++> -- pattern for a specific EADT: List a+> pattern ConsList :: a -> List a -> List a+> pattern ConsList a l = Cons a l++We can see that when we use it we don't need type ascriptions because the+@Int@ type is propagated:++> intList :: List Int+> intList = ConsList 10 $ ConsList 20 $ ConsList 30 Nil++The 'Data.Variant.EADT.TH.eadtPatternT' Template Haskell helper generates such+type-specialised patterns.++=== Matching values++It is easy and tempting to use the same pattern synonyms to match EADT values.+And indeed this works pretty well:++> showEADTList :: Show a => List a -> String+> showEADTList = \case+>    ConsList a l -> show a ++ " : " ++ showEADTList l+>    Nil          -> "Nil"+>    _            -> undefined+>+> > putStrLn (showEADTList strList)+> "How" : "are" : "you?" : Nil+>+> > putStrLn (showEADTList intList)+> 10 : 20 : 30 : Nil++However this approach is unsatisfactory for two reasons:++1. The pattern matching isn't safe: for now the compiler cannot use the EADT+   constructor type list to infer that the pattern-match is complete. Hence we+   need the wildcard match to avoid a warning and to use @ConsList@ to help the+   type inference. A better alternative is presented in the __Safe pattern+   matching__ section below.++2. The function isn't generic: if we would like to write a @showEADTList@+   function that also works on the heterogeneous @mixedList@ above or on any+   future EADT provided its constructors can be handled, we need to use+   another approach based on type-classes. This is presented in the+   following sections.++== Explicit recursive traversal++When we need to traverse a data structure, we can either use predefined+traversal functions (e.g., @map@, @fold@, etc.) or write the recursive function+explicitly. EADTs are no different in this regard.++In this section we explain how to write explicitly recursive functions for+EADTs: similarly to usual ADTs, it's better to use them only when generic+traversal functions (presented in following sections) don't fit the bill.++=== Traversal example++If we were to write a @show@ function for a list ADT, we could do it like this:++> data List a = Cons a (List a) | Nil+>+> showList :: Show a => List a -> String+> showList = \case+>    Nil      -> "Nil"+>    Cons a l -> show a ++ " : " ++ showList l++In @showList@ we can pattern match on the constructors of @List a@ because the+constructor list is closed. With EADTs the list of constructors isn't closed+and we want to be able to use the same code even with EADTs extended with more+constructors. To support this, we use type-classes to build the equivalent of+the @case@ in @showList@ above.++Let's define a class @MyShow@ that is very much like 'Show' and that we will+use to print any EADT value:++> class MyShow e where+>    myShow :: e -> String++We can define instances for the @List@ constructors defined above:++> instance MyShow (NilF e) where+>    myShow _ = "Nil"+>+> instance (MyShow e, Show a) => MyShow (ConsF a e) where+>    myShow (ConsF a l) = show a ++ " : " ++ myShow l++Note how each instance corresponds to an alternative in @showList@.++It also requires some additional instances to traverse the 'VariantF'+combinator datatype and the 'EADT' recursion-handling datatype:++> {-# LANGUAGE UndecidableInstances #-}+> {-# LANGUAGE FlexibleInstances #-}+>+> instance MyShow (VariantF f (EADT f)) => MyShow (EADT f) where+>    {-# INLINE myShow #-}+>    myShow (EADT e) = myShow e+>+> instance MyShow (VariantF [] e) where+>    {-# INLINE myShow #-}+>    myShow = undefined+>+> instance+>       ( MyShow (f e)+>       , MyShow (VariantF fs e)+>       ) => MyShow (VariantF (f ': fs) e)+>    where+>       {-# INLINE myShow #-}+>       myShow v = case popVariantFHead v of+>          Right u -> myShow u+>          Left  w -> myShow w++Note: this boilerplate code (hopefully always very similar and straightforward)+is the main reason you should strive to use predefined recursion schemes+instead of the explicit approach presented here.++Note: the @INLINE@ pragmas are used to ensure that in the generated code we+get the equivalent of the @case@ expression in @showList@.++Now we can test it:++> strList :: List String+> strList = Cons "How" (Cons "are" (Cons "you?" Nil))+>+> intList :: List Int+> intList = Cons (10 :: Int) $ Cons (20 :: Int) $ Cons (30 :: Int) Nil+>+> mixedList :: EADT [ConsF Int, ConsF Float, NilF]+> mixedList = Cons (10 :: Int) $ Cons (5.0 :: Float) $ Cons (30 :: Int) Nil+>+> > putStrLn (myShow strList)+> "How" : "are" : "you?" : Nil+>+> > putStrLn (myShow intList)+> 10 : 20 : 30 : Nil+>+> > putStrLn (myShow mixedList)+> 10 : 5.0 : 30 : Nil++=== Extension example++If we add a new constructor, such as @NodeF@ to build binary trees:++> data NodeF a e = NodeF a e e deriving (Functor)+>+> eadtPattern 'NodeF "Node"++We can also add a @MyShow@ instance for @NodeF@:++> instance (MyShow e, Show a) => MyShow (NodeF a e) where+>    myShow (NodeF a l1 l2) = show a ++ "\n|- " ++ indent (myShow l1)+>                                    ++ "|- " ++ indent (myShow l2)+>       where+>          indent' []     = []+>          indent' (x:xs) = x : fmap ("   "++) xs+>          indent = unlines . indent' . lines++Now we can show binary trees as well as lists:++> tree :: EADT [NodeF Int, NilF]+> tree = Node (10 :: Int)+>          (Node (5 :: Int) Nil Nil)+>          (Node (30 :: Int) Nil Nil)+>+> > putStrLn (myShow tree)+> 10+> |- 5+>    |- Nil+>    |- Nil+> |- 30+>    |- Nil+>    |- Nil++We can also mix up trees and lists by using @ConsF@ and @NodeF@ in the same+EADT:++> mixedTree :: EADT [NodeF Int, ConsF Int, NilF]+> mixedTree = Node (10 :: Int)+>          (Cons (5 :: Int) $ Cons (6 :: Int) $ Cons (7 :: Int) Nil)+>          (Node (30 :: Int) Nil Nil)+>+> > putStrLn (myShow mixedTree)+> 10+> |- 5 : 6 : 7 : Nil+> |- 30+>    |- Nil+>    |- Nil++== Constraining constructors with @:\<:@++The ':<:' type operator is used to ensure that a constructor is present in an+EADT. For example if we consider the following type signature (that will be+developed in the example below):++> distr :: (AddF :<: f, MulF :<: f) => EADT f -> Maybe (EADT f)++The constructors of @EADT f@ are not specified but the constraints+@(AddF :\<: f, MulF :\<: f)@ ensure that at least @AddF@ and @MulF@+constructors are present.++Note that to shorten a list of constraints such as+@(AddF :\<: f, MulF :\<: f)@ you can use the ':<<:' operator:+@[AddF,MulF] :\<\<: f@.++=== Transformation example++Suppose we have the following EADT for arithmetic expressions:++> {-# LANGUAGE DeriveFunctor #-}+>+> data ValF e = ValF Int deriving (Functor)+> data AddF e = AddF e e deriving (Functor)+> data MulF e = MulF e e deriving (Functor)+>+> eadtPattern 'ValF "Val"+> eadtPattern 'AddF "Add"+> eadtPattern 'MulF "Mul"+>+> type Expr = EADT [ValF, AddF, MulF]++We can define some value:++> e1 :: Expr+> e1 = Add (Val 10)+>          (Mul (Add (Val 5)+>                    (Val 10))+>               (Val 7))++We can define instances of the @MyShow@ class (defined above):++> instance MyShow (ValF e) where+>   myShow (ValF e) = show e+>+> instance MyShow e => MyShow (AddF e) where+>   myShow (AddF x y) = "(" ++ myShow x ++ " + " ++ myShow y ++ ")"+>+> instance MyShow e => MyShow (MulF e) where+>   myShow (MulF x y) = "(" ++ myShow x ++ " * " ++ myShow y ++ ")"+>+> > putStrLn (myShow e1)+> (10 + ((5 + 10) * 7))++Now we can define a transformation that distributes multiplication over+addition as follows:++> -- distribute multiplication over addition if it matches+> distr :: (AddF :<: f, MulF :<: f) => EADT f -> Maybe (EADT f)+> distr (Mul a (Add c d)) = Just (Add (Mul a c) (Mul a d))+> distr (Mul (Add c d) a) = Just (Add (Mul c a) (Mul d a))+> distr _                 = Nothing++Note that this function works on any EADT as long as it has @AddF@ and+@MulF@ constructors. We indicate such constraints with the ':<:' type operator.++Then we need a helper function that performs the traversal of the EADT:++> import Control.Arrow ((>>>))+>+> -- bottom up traversal that performs an additional bottom up traversal in+> -- the transformed sub-tree when a transformation occurs.+> bottomUpFixed :: Functor (VariantF cs) => (EADT cs -> Maybe (EADT cs)) -> EADT cs -> EADT cs+> bottomUpFixed f = project >>> fmap (bottomUpFixed f) >>> embed >>> f'+>    where+>       f' u = case f u of+>          Nothing -> u+>          Just v  -> bottomUpFixed f v+>+> -- | Distribute multiplication over addition+> distribute :: ([AddF,MulF] :<<: cs, Functor (VariantF cs)) => EADT cs -> EADT cs+> distribute = bottomUpFixed distr++Note: @bottomUpFixed@ is a generic recursion scheme over an EADT. You can read+more on this approach in the section __Recursion schemes and EADTs__ below.++Finally we can test the transformation on an example:++> > putStrLn (myShow e1)+> (10 + ((5 + 10) * 7))+>+> > putStrLn (myShow (distribute e1))+> (10 + ((5 * 7) + (10 * 7)))++=== Extensibility++Suppose we add a @PowF@ (power) constructor:++> data PowF e = PowF e e deriving (Functor)+>+> eadtPattern 'PowF "Pow"+>+> instance MyShow e => MyShow (PowF e) where+>   myShow (PowF x y) = "(" ++ myShow x ++ " ^ " ++ myShow y ++ ")"++We can now write expressions that use the @Pow@ constructor:++> type Expr2 = EADT [ValF, AddF, MulF, PowF]+>+> e2 :: Expr2+> e2 = Pow (Val 10)+>          (Mul (Add (Pow (Val 5) (Val 8))+>                    (Val 10))+>               (Val 7))++We can check that our distribution function still works on this new type of+expression without being modified at all:++> > putStrLn (myShow (distribute e2))+> (10 ^ (((5 ^ 8) * 7) + (10 * 7)))++== Recursion schemes and EADTs++Traversing an EADT explicitly (see __Explicit recursive traversal__ above) can+be tedious. Another approach consists in using dedicated composable combinators+called /recursion schemes/.++The well known @map@ and @fold@ functions are examples of recursion schemes+for lists: these functions handle the recursive traversal of the data+structure and are parameterized by the functions performing the actual work.+Recursion schemes are a generalization of this approach.++A good introduction to recursion schemes can be found here:+<https://blog.sumtypeofway.com/an-introduction-to-recursion-schemes/>++See also: <https://bartoszmilewski.com/2013/06/10/understanding-f-algebras/>++This package re-exports the @recursion-schemes@ machinery (e.g.,+'Data.Functor.Foldable.cata', 'Data.Functor.Foldable.ana',+'Data.Functor.Foldable.para', 'Data.Functor.Foldable.apo', etc.) and provides+in addition the simpler 'BottomUpF' / 'BottomUp' / 'bottomUp' helpers in+"Data.Variant.Functor" to dispatch a type-class method to every constructor in+the EADT.++=== Catamorphism: Show example++The 'EADTShow' class shipped with this module is the canonical example. We can+roll our own to see how it works:++> class FunctorShow (f :: Type -> Type) where+>   functorShow :: f String -> String++We can define instances for @NilF@ and @ConsF@:++> instance FunctorShow NilF where+>   functorShow _ = "Nil"+>+> instance Show a => FunctorShow (ConsF a) where+>   functorShow (ConsF a l) = show a ++ " : " ++ l++Note that there is no recursive call in the definition of the @ConsF@ instance:+it is because we are going to use a recursion scheme that will handle the+recursion.++Finally we can define a generic @myShow@ function that uses the catamorphism+recursion scheme with the @functorShow@ class method.++> myShow :: BottomUpF FunctorShow xs => EADT xs -> String+> myShow = bottomUp (toBottomUp @FunctorShow functorShow)++We can test it:++> intList :: List Int+> intList = Cons (10 :: Int) $ Cons (20 :: Int) $ Cons (30 :: Int) Nil+>+> mixedList :: EADT [ConsF Int, ConsF Float, ConsF String, NilF]+> mixedList = Cons @Int 10 $ Cons @Float 5.0 $ Cons "Test" Nil+>+> > putStrLn $ myShow intList+> 10 : 20 : 30 : Nil+>+> > putStrLn $ myShow mixedList+> 10 : 5.0 : "Test" : Nil++This is exactly how 'eadtShow' is implemented in this module: see 'EADTShow'+and 'eadtShow'.++=== Catamorphism: List mapping example++Similarly to the example above, suppose that we want to implement mapping over+an EADT list. We can use the following type-class:++> class MapEADT a xs (f :: Type -> Type) where+>   -- map the outer constructor of an EADT+>   mapEADT1 :: (a -> a) -> f (EADT xs) -> EADT xs++We need some instances to handle our EADT constructors:++> instance (NilF :<: xs) => MapEADT a xs NilF where+>   mapEADT1 _ NilF = Nil+>+> instance (ConsF a :<: xs) => MapEADT a xs (ConsF a) where+>   mapEADT1 f (ConsF a x) = Cons (f a) x++Now we can define the @mapEADT@ function by using the catamorphism combinator+@'Data.Functor.Foldable.cata'@ together with 'BottomUp' and 'toBottomUp':++> mapEADT :: ( BottomUpF (MapEADT a xs) xs+>            ) => (a -> a) -> EADT xs -> EADT xs+> mapEADT f = bottomUp (toBottomUp @(MapEADT a xs) (mapEADT1 f))++We can test it:++> intList :: List Int+> intList = Cons (10 :: Int) $ Cons (20 :: Int) $ Cons (30 :: Int) Nil+>+> > putStrLn $ myShow $ mapEADT ((+5) :: Int -> Int) intList+> 15 : 25 : 35 : Nil++== Safe pattern matching with @>:>@++Suppose we have the following @List@ EADT:++> data ConsF a l = ConsF a l deriving (Functor)+> data NilF    l = NilF      deriving (Functor)+>+> eadtPattern 'ConsF "Cons"+> eadtPattern 'NilF  "Nil"+>+> type List a = EADT [ConsF a, NilF]+>+> -- pattern for a specific EADT: List a+> pattern ConsList :: a -> List a -> List a+> pattern ConsList a l = Cons a l++Using classic pattern matching on @List@ constructors as we do below isn't+really typesafe because the compiler cannot detect that the pattern matching is+complete, hence we have the choice between a warning or adding a wildcard+match:++> showEADTList :: Show a => List a -> String+> showEADTList = \case+>    ConsList a l -> show a ++ " : " ++ showEADTList l+>    Nil          -> "Nil"+>    _            -> undefined -- this line avoids the warning but is unsafe+>                              -- if we add constructors in the future++A safe alternative is to rely on multi-continuations: we can transform any+@EADT [A,B,C]@ into a function whose type is @(A -> r, B -> r, C -> r) -> r@+with the @('Data.Variant.ContFlow.>:>')@ operator. Then we can safely provide+a function per constructor as in a pattern-matching.++=== Explicit recursion example++> import Data.Variant.ContFlow+>+> showCont' l = l >:>+>    ( \(ConsF a r) -> show a ++ " : " ++ showCont' r -- explicit recursion+>    , \NilF        -> "Nil"+>    )+>+> > showCont' intList+> "10 : 20 : 30 : Nil"++=== Recursion schemes (catamorphism)++> showCont l = l >:>+>    ( \(ConsF a r) -> show a ++ " : " ++ r -- no explicit recursion+>    , \NilF        -> "Nil"+>    )+>+> > cata showCont intList+> "10 : 20 : 30 : Nil"++== EADT constructor removal/transformation++Removing constructors from an EADT is equivalent to transforming every instance+of these constructors into other constructors of another EADT.++We consider 3 cases:++1. Fixed input EADT type; fixed list of constructors to act on+2. Generic input EADT type; fixed list of constructors to act on+3. Generic input EADT type; extensible list of constructors to act on++Note in the 3 cases we need to specify the resulting EADT type as it could be+anything fulfilling the constraints.++=== Fixed input, fixed matches++If the type of the input EADT is fixed, we can use safe pattern-matching with+the @('Data.Variant.ContFlow.>:>')@ operator as follows:++> -- replace Even and Odd constructors with a Cons constructor+> removeOddEven l = l >:>+>    (\(EvenF a r) -> Cons a r+>    ,\(OddF  a r) -> Cons a r+>    ,\NilF        -> Nil+>    )+>+> eo :: EADT [EvenF Int, OddF Int, NilF]+> eo = Even (10 :: Int) $ Odd (5 :: Int) $ Odd (7 :: Int) Nil+>+> > eadtShow (cata removeOddEven eo :: List Int)+> "10 : 5 : 7 : Nil"++Note that @removeOddEven@ only works on a specific EADT. If we want it to work+on any EADT that contains @EvenF@ and @OddF@ constructors, read the following+sections.++=== Generic input, fixed matches++If we want @removeOddEven@ to work on input EADTs of any type, we can extract+the constructors that we are interested in with 'splitVariantF' and lift the+left-over constructors with 'liftVariantF' as follows:++> removeOddEven x = case splitVariantF @[EvenF Int, OddF Int] x of+>    -- replace Even and Odd constructors with a Cons constructor+>    Right v        -> v >:>+>                         ( \(EvenF a l) -> Cons a l+>                         , \(OddF a l)  -> Cons a l+>                         )+>    -- do nothing to the other constructors+>    Left leftovers -> EADT (liftVariantF leftovers)+>+> eo1 :: EADT [EvenF Int, OddF Int, NilF]+> eo1 = Even (10 :: Int) $ Odd (5 :: Int) $ Odd (7 :: Int) Nil+>+> > eadtShow (cata removeOddEven eo1 :: List Int)+> "10 : 5 : 7 : Nil"+>+> -- additional `ConsF Int` constructor+> eo2 :: EADT [ConsF Int, EvenF Int, OddF Int, NilF]+> eo2 = Even (10 :: Int) $ Cons (5 :: Int) $ Odd (7 :: Int) Nil+>+> > eadtShow (cata removeOddEven eo2 :: List Int)+> "10 : 5 : 7 : Nil"++=== Generic input, extensible matches++If we want the @removeOddEven@ pattern match to be extensible, we can use+type-classes with an overlappable instance handling the generic case (i.e.+that only transfers constructors from one EADT to another without modifying+them).++> class RemoveOddEven ys (f :: Type -> Type) where+>    removeOddEven :: f (EADT ys) -> EADT ys+>+> -- replace Odd and Even with Cons+> instance ConsF a :<: ys => RemoveOddEven ys (OddF a) where+>    removeOddEven (OddF a l) = Cons a l+>+> instance ConsF a :<: ys => RemoveOddEven ys (EvenF a) where+>    removeOddEven (EvenF a l) = Cons a l+>+> -- handle remaining constructors generically+> instance {-# OVERLAPPABLE #-} f :<: ys => RemoveOddEven ys f where+>    removeOddEven = VF -- keep the other constructors unmodified++Then we lift it through the @VariantF@ combinator with 'BottomUp' /+'toBottomUp':++> myRemoveOddEven :: BottomUpF (RemoveOddEven ys) xs => EADT xs -> EADT ys+> myRemoveOddEven = bottomUp (toBottomUp @(RemoveOddEven ys) removeOddEven)++Test:++> eo :: EADT [EvenF Int, OddF Int, NilF]+> eo = Even (10 :: Int) $ Odd (5 :: Int) $ Odd (7 :: Int) Nil+>+> > eadtShow (myRemoveOddEven eo :: List Int)+> "10 : 5 : 7 : Nil"+>+> -- EADT with an additional `ConsF Int` constructor+> eo2 :: EADT [ConsF Int, EvenF Int, OddF Int, NilF]+> eo2 = Even (10 :: Int) $ Odd (5 :: Int) $ Cons (7 :: Int) $ Odd (7 :: Int) Nil+>+> > eadtShow (myRemoveOddEven eo2 :: List Int)+> "10 : 5 : 7 : 7 : Nil"+>+> -- EADT with an additional `ConsF String` constructor+> eo3 :: EADT [ConsF Int, EvenF Int, OddF Int, ConsF String, NilF]+> eo3 = Even (10 :: Int) $ Cons "Test" $ Odd (5 :: Int) $ Cons (7 :: Int) $ Odd (7 :: Int) Nil+>+> > eadtShow (myRemoveOddEven eo3 :: EADT [ConsF Int, ConsF String, NilF])+> "10 : \"Test\" : 5 : 7 : 7 : Nil"++We can extend @myRemoveOddEven@ to support other constructors by adding new+instances of @RemoveOddEven@ for them.++== Splitting EADT constructors++We can chose to handle only a subset of the constructors of an EADT by using+'splitVariantF'.++For instance in the following example we only handle @EvenF Int@ and+@OddF Int@ constructors. The other ones are considered as left-overs:++> alg x = case splitVariantF @[EvenF Int, OddF Int] x of+>   Right v        -> v >:>+>                        ( \(EvenF _ l) -> "Even : " ++ l+>                        , \(OddF  _ l) -> "Odd : "  ++ l+>                        )+>   Left _leftovers -> "something else"++We can test this code with:++> eo :: EADT [EvenF Int, OddF Int, NilF]+> eo = ... -- some value+>+> eo2 :: EADT [ConsF Int, EvenF Int, OddF Int, NilF]+> eo2 = Even (10 :: Int) $ Odd (5 :: Int) $ Cons (7 :: Int) $ Odd (7 :: Int) Nil+>+> > cata alg eo+> "Odd : Even : Odd : something else"+>+> > cata alg eo2+> "Even : Odd : something else"++Note that the traversal ends when it encounters an unhandled constructor.++== Background on EADTs++=== Why not Variant?++Extensible ADT (EADT) adds support for recursive datatypes to the 'V' / Variant+type (see "Data.Variant"). Indeed if we tried to define a recursive datatype+(e.g., a list) by using Variants, we would get the following error:++> data Cons a l = Cons a l+> data Nil      = Nil+>+> > type L a = V [Cons a (L a), Nil]+>+> <interactive>:19:2: error:+>     Cycle in type synonym declarations:+>       <interactive>:19:2-34: type L a = V [Cons a (L a), Nil]++The issue is that there is a cyclic definition and it isn't allowed. We could+introduce ad-hoc datatypes (e.g., @newtype L a = L (V [Cons a (L a),Nil])@) to+break this cycle but this would defeat our purpose because the datatype+wouldn't be generic anymore.++'EADT' is the datatype we use to break these cycles. By always using the same+datatype, we can provide functions that work for every EADTs. 'EADT' is very+similar to the @Fix@ datatype (fixed point of a functor). We use our own type+to declare our own instances.++For example with EADTs we just have to write the following code to declare a+@List@:++> data ConsF a l = ConsF a l deriving (Functor)+> data NilF    l = NilF      deriving (Functor)+>+> type List a = EADT [ConsF a, NilF]++=== History++==== The expression problem (1998)++In 1998, Philip Wadler defined the /Expression Problem/ as follows:++> The Expression Problem is a new name for an old problem. The goal is to+> define a datatype by cases, where one can add new cases to the datatype and+> new functions over the datatype, without recompiling existing code, and+> while retaining static type safety++See:++* <https://en.wikipedia.org/wiki/Expression_problem>+* <http://homepages.inf.ed.ac.uk/wadler/papers/expression/expression.txt>++In Haskell it is straightforward to add new functions over an ADT. Suppose we+have the following arithmetic expression ADT:++> data Expr = Val Int | Add Expr Expr++We can independently add an evaluator function, potentially in another module:++> eval :: Expr -> Int+> eval (Val x)   =  x+> eval (Add x y) = eval x + eval y++However if we want to add a new constructor to the ADT (say support for+multiplication), we have to modify both the ADT definition and the functions+using it:++> data Expr = .... | Mul Expr Expr+>+> eval :: Expr -> Int+> ....+> eval (Mul x y) = eval x * eval y++What we want is to be able to add a new independent module containing both the+@Mul@ constructor and the code to handle it, without modifying the other+modules defining the other constructors and the other code to handle them!++==== Data types à la carte (2008)++Ten years later (in 2008), Wouter Swierstra described a technique to handle+this in his well-known+<http://www.cs.ru.nl/~W.Swierstra/Publications/DataTypesALaCarte.pdf Data types à la carte>+paper. The first idea is to define data constructors independently of the ADT+and to use a type parameter to leave open the ADT they are part of.++> -- Independent data constructors. Parameter `e` represents the ADT they+> -- will be part of. It is required even if it is not used in the right hand+> -- side.+> data Val e = Val Int deriving (Functor)+> data Add e = Add e e deriving (Functor)++Defining a new independent constructor is easy:++> data Mul e = Mul e e deriving (Functor)++The second idea is to use a combinator data type @:+:@:++> data (f :+: g) e = Inl (f e) | Inr (g e)+>+> instance (Functor f, Functor g) => Functor (f :+: g) where ...++It is similar to 'Either' except that it passes the same additional type+parameter to both @f@ and @g@ type constructors. It can be used to compose+independent data constructors without creating a new data type:++> type ExprF = Val :+: Add++@ExprF@ has kind @Type -> Type@ and its type parameter is used as the @e@+parameter of the independent data constructors. We can set it to arbitrary+types such as @Int@ to build valid values:++> y = Inr (Add 5 8) :: ExprF Int++However the main use of this parameter should be to indicate the type of the+expression data type we want to build, say @Expr@. Hence we would like to+write something like this:++> type Expr = ExprF Expr+>+>  > error:+>  Cycle in type synonym declarations:+>    <interactive>:12:1-22: type Expr = ExprF Expr++Oops, we can't build this cyclic (infinite) type. This leads us to the third+idea: use another data type to handle the recursive nature of the expression+type:++> newtype Expr = Expr (ExprF Expr)++We can abstract over it to use the same data type for different expression+types:++> -- `Fix` type as defined in Data.Functor.Foldable for instance+> newtype Fix f = Fix (f (Fix f))+>+> type Expr = Fix ExprF++In summary, the approach uses 3 different sorts of data types:++1. Constructor data types: @Val@, @Add@, @Mul@...+2. Combinator data type: @:+:@+3. Recursion handling data type: @Fix@++By using these different data types we have untangled the construction of ADTs+(algebraic data types) and we can freely add new constructor data types and+mix them into different algebraic data types.++Operations on these algebraic data types can be defined independently by using+type-classes and recursion schemes.++==== EADT - Extensible ADT (2018)++The EADT approach builds on Swierstra's one but it replaces the combinator+data type @:+:@ with the 'VariantF' one based on Variant (see "Data.Variant").+Similarly to the @:+:@ combinator data type, 'VariantF' passes its @e@+parameter to all of its \"member\" types and has an instance of the 'Functor'+class.++> newtype VariantF (xs :: [Type -> Type]) e = VariantF (Variant (ApplyAll e xs))+>+> -- ApplyAll e [f,g,h] ==> [f e, g e, h e]+>+> instance Functor (VariantF xs) where ....++Now instead of writing @f :+: g :+: h :+: i@ to combine constructor data types+to form an ADT we can write @VariantF [f,g,h,i]@. Just like using 'V' is more+efficient -- O(1) memory usage and (de)construction -- than using a nest of+'Either', using 'VariantF' is more efficient than using a nest of @:+:@.++Finally an EADT is just @Fix (VariantF xs)@ except that we use our own 'EADT'+newtype instead of @Fix@ in order to define our own additional (and non-orphan)+type-class instances. 'EADT' implements 'Recursive' and 'Corecursive'+type-classes from the @recursion-schemes@ package, so usual @Fix@ functions+should work on 'EADT' too.++> newtype EADT xs = EADT (VariantF xs)++The next step is to define bidirectional pattern synonyms (see __Defining+pattern synonyms__ above) that make the manipulation of EADT values very+similar to the manipulation of usual ADTs. By using Template Haskell, these+patterns can be automatically generated.++In summary EADTs provide a nicer interface and a better asymptotic+implementation in both memory and runtime execution than Data types à la carte.+In the future it would be better to have native support for all of this in the+language, especially to enhance compilation times by not using type families.++-}+module Data.Variant.EADT+   ( EADT (..)+   , (:<:)+   , (:<<:)+   , pattern VF+   , appendEADT+   , liftEADT+   , popEADT+   , contToEADT+   , contToEADTM+   , EADTShow (..)+   , eadtShow+   -- * Reexport+   , module Data.Variant.Functor+   , module Data.Variant.VariantF+   )+where++import Data.Variant+import Data.Variant.VariantF+import Data.Variant.Types+import Data.Variant.ContFlow+import Data.Variant.Functor++import GHC.TypeLits++-- $setup+-- >>> :seti -XDataKinds+-- >>> :seti -XTypeApplications+-- >>> :seti -XTypeOperators+-- >>> :seti -XFlexibleContexts+-- >>> :seti -XTypeFamilies+-- >>> :seti -XPatternSynonyms+-- >>> :seti -XDeriveFunctor+-- >>>+-- >>> import Data.Functor.Classes+-- >>>+-- >>> data ConsF a e = ConsF a e deriving (Eq,Ord,Show,Functor)+-- >>> data NilF    e = NilF      deriving (Eq,Ord,Show,Functor)+-- >>>+-- >>> instance Eq a => Eq1 (ConsF a) where liftEq cmp (ConsF a e1) (ConsF b e2) = a == b && cmp e1 e2+-- >>> instance Eq1 NilF where liftEq _ _ _ = True+-- >>>+-- >>> :{+-- >>> pattern Cons :: ConsF a :<: xs => a -> EADT xs -> EADT xs+-- >>> pattern Cons a l = VF (ConsF a l)+-- >>> pattern Nil :: NilF :<: xs => EADT xs+-- >>> pattern Nil = VF NilF+-- >>> type ListF a = VariantF '[NilF, ConsF a]+-- >>> type List a = EADT '[NilF, ConsF a]+-- >>> :}+--+-- >>>+-- >>> let a = Cons "Hello" (Cons "World" Nil) :: List String+-- >>> let b = Cons "Bonjour" (Cons "Monde" Nil) :: List String+-- >>> a == b+-- False+-- >>> a == a+-- True+++-- | An extensible ADT+newtype EADT fs+   = EADT (VariantF fs (EADT fs))++type instance Base (EADT fs) = VariantF fs++instance Functor (VariantF fs) => Recursive (EADT fs) where+   project (EADT a) = a++instance Functor (VariantF fs) => Corecursive (EADT fs) where+   embed = EADT++instance Eq1 (VariantF fs) => Eq (EADT fs) where+  EADT a == EADT b = eq1 a b++instance Ord1 (VariantF fs) => Ord (EADT fs) where+  compare (EADT a) (EADT b) = compare1 a b++instance Show1 (VariantF fs) => Show (EADT fs) where+  showsPrec d (EADT a) =+    showParen (d >= 11)+      $ showString "EADT "+      . showsPrec1 11 a++-- | Constructor `f` is in `xs`+type family f :<: xs where+   f :<: xs = EADTF' f (EADT xs) xs++-- | Forall `x` in `xs`, `x :<: ys`+type family (:<<:) xs ys :: Constraint where+   '[] :<<: ys       = ()+   (x ': xs) :<<: ys = (x :<: ys, xs :<<: ys)++type EADTF' f e cs =+   ( Member f cs+   , Index (IndexOf (f e) (ApplyAll e cs)) (ApplyAll e cs) ~ f e+   , PopVariant (f e) (ApplyAll e cs)+   , KnownNat (IndexOf (f e) (ApplyAll e cs))+   , Remove (f e) (ApplyAll e cs) ~ ApplyAll e (Remove f cs)+   )++-- | Pattern-match in an extensible ADT+pattern VF :: forall e f cs.+   ( e ~ EADT cs  -- allow easy use of TypeApplication to set the EADT type+   , f :<: cs     -- constraint synonym ensuring `f` is in `cs`+   ) => f (EADT cs) -> EADT cs+pattern VF x = EADT (VariantF (VSilent x))+   -- `VSilent` matches a variant value without checking the membership: we+   -- already do it with :<:++-- | Append new "constructors" to the EADT+appendEADT :: forall ys xs zs.+   ( zs ~ Concat xs ys+   , ApplyAll (EADT zs) zs ~ Concat (ApplyAll (EADT zs) xs) (ApplyAll (EADT zs) ys)+   , Functor (VariantF xs)+   ) => EADT xs -> EADT zs+appendEADT (EADT v) = EADT (appendVariantF @ys (fmap (appendEADT @ys) v))++-- | Lift an EADT into another+liftEADT :: forall e as bs.+   ( e ~ EADT bs+   , LiftVariantF as bs e+   , Functor (VariantF as)+   ) => EADT as -> EADT bs+liftEADT = cata (EADT . liftVariantF)++-- | Pop an EADT value+popEADT :: forall f xs e.+   ( f :<: xs+   , e ~ EADT xs+   , f e :< ApplyAll e xs+   ) => EADT xs -> Either (VariantF (Remove f xs) (EADT xs)) (f (EADT xs))+popEADT (EADT v) = popVariantF v++-- | MultiCont instance+--+-- >>> let f x = toCont x >::> (const "[]", \(ConsF u us) -> u ++ ":" ++ f us)+-- >>> f a+-- "Hello:World:[]"+instance (Functor (VariantF xs), ContVariant (ApplyAll (EADT xs) xs)) => MultiCont (EADT xs) where+   type MultiContTypes (EADT xs) = ApplyAll (EADT xs) xs+   toCont  (EADT v) = variantFToCont v+   toContM f        = variantFToContM (project <$> f)++-- | Convert a multi-continuation into an EADT+contToEADT ::+   ( ContVariant (ApplyAll (EADT xs) xs)+   ) => ContFlow (ApplyAll (EADT xs) xs)+                 (V (ApplyAll (EADT xs) xs))+     -> EADT xs+contToEADT c = EADT (contToVariantF c)++-- | Convert a multi-continuation into an EADT+contToEADTM ::+   ( ContVariant (ApplyAll (EADT xs) xs)+   , Monad f+   ) => ContFlow (ApplyAll (EADT xs) xs)+                 (f (V (ApplyAll (EADT xs) xs)))+     -> f (EADT xs)+contToEADTM f = EADT <$> contToVariantFM f+++-- | Show an EADT constructor.+--+-- Provide an instance per constructor and use 'eadtShow' to display the whole+-- EADT. class EADTShow f where    eadtShow' :: f String -> String
src/lib/Data/Variant/EGADT.hs view
@@ -1,4 +1,3 @@-{-# LANGUAGE CPP #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE KindSignatures #-}@@ -14,6 +13,134 @@ {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE ViewPatterns #-} +{- | Extensible GADT (EGADT)++EGADTs are to GADTs what 'Data.Variant.EADT.EADT' is to plain ADTs: an EGADT+carries an extra type index just like a GADT, but its constructors are+__open__ — defined independently as standalone data types and combined into+an EGADT through a type-level list, so the same constructor can be reused in+different EGADTs and new constructors can be added without touching existing+code.++> -- closed: a fixed set of constructors, each constraining the index `t`+> data AST t where+>    Var :: String -> AST Int+>    Lam :: (AST a -> AST b) -> AST (a -> b)+>    App :: AST (a -> b) -> AST a -> AST b+>+> -- open: each constructor is its own data type; the EGADT is a type alias+> data VarF ast t where+>   VarF :: String -> VarF ast Int+> data LamF ast 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+>+> type AST t = EGADT [VarF, LamF, AppF] t++The first parameter of each constructor (@ast@ above) is the+\"recursion-handling\" parameter, similar to the @e@ parameter of EADT+constructors (see "Data.Variant.EADT"); t'EGADT' substitutes itself for it.+The+second parameter (@t@) is the GADT-style type index that constructors can+constrain (e.g., @VarF@ forces @t ~ Int@).++== Defining constructors++EGADT constructors use GADT syntax. They take two extra type parameters in+addition to their fields:++* the recursion parameter (@ast@): the type used for recursive sub-terms;+* the index (@t@): the type the term represents.++> {-# LANGUAGE GADTs #-}+> {-# LANGUAGE KindSignatures #-}+>+> import Data.Kind (Type)+>+> data VarF (ast :: Type -> Type) t where+>   VarF :: String -> VarF ast Int+>+> data LamF (ast :: Type -> Type) t where+>   LamF :: (ast a -> ast b) -> LamF ast (a -> b)+>+> data AppF (ast :: Type -> Type) t where+>   AppF :: ast (a -> b) -> ast a -> AppF ast b++Like a GADT, the result type @VarF ast t@ is constrained inside the+constructor (here @t ~ Int@). Unlike a GADT, the constructor doesn't fix what+@ast@ is — the EGADT machinery will tie the recursive knot.++== Defining the EGADT++An EGADT is just a type alias listing the open constructors and exposing the+index parameter:++> type AST t = EGADT [VarF, LamF, AppF] t++== Creating values++Use the 'VF' pattern synonym to wrap a constructor value into an EGADT. The+GADT-style refinement of the index follows the constructor:++> -- a variable always has type Int+> v :: AST Int+> v = VF (VarF "x")+>+> -- (\x -> x) :: Int -> Int+> i :: AST (Int -> Int)+> i = VF (LamF (\x -> x))+>+> -- application of an `Int -> Int` to an `Int` produces an `Int`+> e :: AST Int+> e = VF (AppF i v)++Trying to build an ill-typed term (e.g., applying @v@ to itself) is a+compile-time error, just like with a regular GADT.++== Pattern matching++Match on EGADT values with the 'VF' pattern synonym. Inside each branch the+GADT refinement of @t@ is in scope, so the body can use type-class instances+or operations that depend on @t@:++> isVar :: AST t -> Bool+> isVar = \case+>    VF (VarF _) -> True  -- here t ~ Int+>    _           -> False++== Membership constraints: ':<!' and ':<<!'++The ':<!' type operator is the EGADT equivalent of+'Data.Variant.EADT.:<:' — it constrains a constructor to be present in the+constructor list:++> -- works on any EGADT that has at least the VarF constructor+> mkVar :: (VarF :<! fs) => String -> EGADT fs Int+> mkVar s = VF (VarF s)++The ':<<!' operator (analogous to 'Data.Variant.EADT.:<<:') shortens a list of+':<!' constraints:++> -- @[VarF, AppF] :<<! fs@ is shorthand for @(VarF :<! fs, AppF :<! fs)@++== Recursion schemes++EGADT supports the higher-order recursion schemes from+"Data.Variant.Functor" via its 'HRecursive' and 'HCorecursive' instances. Use+'hcata' / 'hana' / 'hpara' / 'hapo' / 'hhylo' to traverse an EGADT in a+type-indexed way.++== See also++* "Data.Variant.EADT" — extensible recursive ADTs without a GADT-style+  index. The motivation, history and design discussion there apply to EGADTs+  as well.+* "Data.Variant.VariantF" — the underlying open functor that EGADT builds on.+* "Data.Variant.Functor" — recursion schemes and the higher-order variants+  used by EGADT.++-} module Data.Variant.EGADT where  import Unsafe.Coerce@@ -25,104 +152,6 @@ import Data.Variant.VariantF import Data.Variant.Types import Data.Variant.Functor--#if MIN_VERSION_base(4,18,0)--- $setup--- >>> :seti -XDataKinds--- >>> :seti -XTypeApplications--- >>> :seti -XTypeOperators--- >>> :seti -XFlexibleContexts--- >>> :seti -XTypeFamilies--- >>> :seti -XPatternSynonyms--- >>> :seti -XDeriveFunctor--- >>> :seti -XGADTs--- >>> :seti -XPolyKinds--- >>> :seti -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--#else--- $setup--- >>> :seti -XDataKinds--- >>> :seti -XTypeApplications--- >>> :seti -XTypeOperators--- >>> :seti -XFlexibleContexts--- >>> :seti -XTypeFamilies--- >>> :seti -XPatternSynonyms--- >>> :seti -XDeriveFunctor--- >>> :seti -XGADTs--- >>> :seti -XPolyKinds--- >>> :seti -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-#endif-  -- | An EADT with an additional type parameter newtype EGADT fs t = EGADT (HVariantF fs (EGADT fs) t)
+ src/tests/EGADT.hs view
@@ -0,0 +1,59 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}++module EGADT+   ( testsEGADT+   )+where++import Test.Tasty+import Test.Tasty.QuickCheck as QC++import Data.Kind+import Data.Variant.EGADT++-------------------------------+-- Typed lambda-calculus AST+-------------------------------++data LamF (ast :: Type -> Type) t where+   LamF :: (ast a -> ast b) -> LamF ast (a -> b)++data AppF (ast :: Type -> Type) t where+   AppF :: ast (a -> b) -> ast a -> AppF ast b++data VarF (ast :: Type -> Type) t where+   VarF :: String -> VarF ast Int++type AST a = EGADT '[LamF, AppF, VarF] a++-- replace any variable name with "zz"+renameVar :: AST Int -> AST Int+renameVar (VF (VarF _)) = VF (VarF "zz")+renameVar _             = error "Unhandled case"++-- application of a lambda to a variable: well-typed at `AST Int`+applyLamToVar :: AST Int+applyLamToVar = VF (AppF (VF (LamF renameVar)) (VF (VarF "a")))++-------------------------------+-- Tests+-------------------------------++testsEGADT :: TestTree+testsEGADT = testGroup "EGADT" $+   [ testProperty "VarF: pattern match extracts the variable name" $+        case VF (VarF "a") :: AST Int of+           VF (VarF x) -> x == "a"+           _           -> False++   , testProperty "AppF + LamF: well-typed application is constructible" $+        case applyLamToVar of+           VF (AppF _ _) -> True+           _             -> False+   ]
src/tests/Main.hs view
@@ -2,9 +2,11 @@  import Variant import EADT+import EGADT  main :: IO () main = defaultMain $ testGroup "utils-variant"   [ testsVariant   , testsEADT+  , testsEGADT   ]
variant.cabal view
@@ -1,6 +1,6 @@ cabal-version:       2.4 name:                variant-version:             1.0.2+version:             1.0.3 synopsis:            Variant and EADT license:             BSD-3-Clause license-file:        LICENSE@@ -70,6 +70,7 @@    other-modules:          Variant       ,  EADT+      ,  EGADT     build-depends:          base                    >= 4.9 && < 5.0