EGADTs

[xgrommx]

Hello @hsyl20 What do u think about create HVariantF for GADTs? And use indexed version of Fix with polykinds?

[hsyl20]

Hello, Do you have a concrete implementation example? I don't see how to get GADT behavior with variants. How do you see it working?

[sheaf]

@hsyl20 Maybe something like the following:

data HFix (f :: (k -> Type) -> (k -> Type)) :: k -> Type where
  HFix :: f (HFix f) a -> HFix f a

newtype HVariantF xs ast t
  = HVariantF (V (HApplyAll xs ast t))

type family HApplyAll (xs :: [ ( k -> Type ) -> ( k -> Type ) ]) (ast :: k -> Type) (t :: k) :: [Type] where
  HApplyAll '[]          _  _ = '[]
  HApplyAll ( x ': xs ) ast t = ( x ast t ': HApplyAll xs ast t )

This seems like it would allow extending the functionality of the library to indexed types / GADTs. For instance we can have HOAS constructors:

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 a = HFix ( HVariantF '[ LamF, AppF ] ) a

[xgrommx]

@sheaf looks good for me, but we can use newtype for HFix

newtype HFix (h :: (k -> Type) -> (k -> Type)) (a :: k) = HFix { unHFix :: h (HFix h) a }

I think it should works

type (~>) f g = forall a. f a -> g a

type family HApplyAll (xs :: [(k -> Type) -> (k -> Type)]) (ast :: k -> Type) (t :: k) :: [Type] where
  HApplyAll '[]          _  _ = '[]
  HApplyAll (x ': xs) ast t = (x ast t ': HApplyAll xs ast t)

newtype HVariantF xs ast t = HVariantF (V (HApplyAll xs ast t))

newtype EGADT xs a = EGADT (HVariantF xs (EGADT xs) a)

class HFunctor (h :: (k -> Type) -> (k -> Type)) where
  hfmap :: (f ~> g) -> h f ~> h g

type family HBase (h :: k -> Type) :: (k -> Type) -> (k -> Type)

class HFunctor (HBase h) => HRecursive (h :: k -> Type) where
  hproject :: h ~> (HBase h) h

class HFunctor (HBase h) => HCorecursive (h :: k -> Type) where
  hembed :: (HBase h) h ~> h

type instance HBase (EGADT xs) = HVariantF xs

instance HFunctor (HVariantF xs) => HRecursive (EGADT xs) where
  hproject (EGADT a) = a

instance HFunctor (HVariantF xs) => HCorecursive (EGADT xs) where
  hembed = EGADT

What do u think about it @hsyl20 ?

[hsyl20]

Oh I see! Very cool!

I've slightly adapted your code and pushed it: https://github.com/haskus/packages/commit/ecb5a5e89d81efc700c5fddee341d02427cf80ff

We still need to adapt constraint code (:<:) and TH code to generate pattern synonyms but it looks very promising. And it seems to work well: I inverted AppF parameters by mistake and I got:

src/lib/Haskus/Utils/EGADT.hs:63: failure in expression `let z = VF (AppF (VF (VarF "a")) (VF (LamF f)))'
expected: 
 but got: 
          <interactive>:735:19: error:
              • Couldn't match type ‘Int’ with ‘(Int -> Int) -> a’
                Expected type: EGADT '[LamF, AppF, VarF] ((Int -> Int) -> a)
                  Actual type: EGADT '[LamF, AppF, VarF] Int
              • In the first argument of ‘AppF’, namely ‘(VF (VarF "a"))’
                In the first argument of ‘VF’, namely
                  ‘(AppF (VF (VarF "a")) (VF (LamF f)))’
                In the expression: VF (AppF (VF (VarF "a")) (VF (LamF f)))
              • Relevant bindings include
                  z :: EGADT '[LamF, AppF, VarF] a (bound at <interactive>:735:5)

Tested with stack test haskus-utils-variant.

[xgrommx]

@hsyl20 nice, this is full context

type f ~> g = forall a. f a -> g a
type NatM m f g = forall a. f a -> m (g a)

type family HBase (h :: k -> Type) :: (k -> Type) -> (k -> Type)

type HAlgebra h f = h f ~> f
type HAlgebraM m h f = NatM m (h f) f
type HGAlgebra w h a = h (w a) ~> a
type HGAlgebraM w m h a = NatM m (h (w a)) a

type HCoalgebra h f = f ~> h f
type HCoalgebraM m h f = NatM m f (h f)
type HGCoalgebra m h a = a ~> h (m a)
type HGCoalgebraM n m h a = NatM m a (h (n a))

class HFunctor (h :: (k -> Type) -> (k -> Type)) where
  hfmap :: (f ~> g) -> h f ~> h g

class HFunctor h => HFoldable (h :: (k -> Type) -> (k -> Type)) where
  hfoldMap :: Monoid m => (forall b. f b -> m) -> h f a -> m

class HFoldable h => HTraversable (h :: (k -> Type) -> (k -> Type))  where
  htraverse :: Applicative e => NatM e f g -> NatM e (h f) (h g)

class HFunctor (HBase h) => HRecursive (h :: k -> Type) where
  hproject :: HCoalgebra (HBase h) h

  hcata :: HAlgebra (HBase h) f -> h ~> f
  hcata algebra = algebra . hfmap (hcata algebra) . hproject

class HFunctor (HBase h) => HCorecursive (h :: k -> Type) where
  hembed :: HAlgebra (HBase h) h

  hana :: HCoalgebra (HBase h) f -> f ~> h
  hana coalgebra = hembed . hfmap (hana coalgebra) . coalgebra

hhylo :: HFunctor f => HAlgebra f b -> HCoalgebra f a -> a ~> b
hhylo f g = f . hfmap (hhylo f g) . g

hcataM :: (Monad m, HTraversable (HBase h), HRecursive h) => HAlgebraM m (HBase h) f -> h a -> m (f a)
hcataM f = f <=< htraverse (hcataM f) . hproject

hlambek :: (HRecursive h, HCorecursive h) => HCoalgebra (HBase h) h
hlambek = hcata (hfmap hembed)

hpara :: (HFunctor (HBase h), HRecursive h) => HGAlgebra (Product h) (HBase h) a -> h ~> a
hpara phi = phi . hfmap (\a -> Pair a (hpara phi a)) . hproject

hparaM :: (HTraversable (HBase h), HRecursive h, Monad m) => HGAlgebraM (Product h) m (HBase h) a -> NatM m h a
hparaM phiM = phiM <=< htraverse (\a -> liftA2 Pair (pure a) (hparaM phiM a)) . hproject

hanaM :: (Monad m, HTraversable (HBase h), HCorecursive h) => HCoalgebraM m (HBase h) f -> f a -> m (h a)
hanaM f = fmap hembed . htraverse (hanaM f) <=< f

hcolambek :: HRecursive h => HCorecursive h => HAlgebra (HBase h) h
hcolambek = hana (hfmap hproject)

hapo :: HCorecursive h => HGCoalgebra (Sum h) (HBase h) a -> a ~> h
hapo psi = hembed . hfmap (coproduct id (hapo psi)) . psi
  where
    coproduct f _ (InL a) = f a
    coproduct _ g (InR a) = g a

hapoM :: (HCorecursive h, HTraversable (HBase h), Monad m) => HGCoalgebraM (Sum h) m (HBase h) a -> NatM m a h
hapoM psiM = fmap hembed . htraverse (coproduct pure (hapoM psiM)) <=< psiM
  where
    coproduct f _ (InL a) = f a
    coproduct _ g (InR a) = g a

hhyloM :: (HTraversable t, Monad m) => HAlgebraM m t h -> HCoalgebraM m t f -> f a -> m (h a)
hhyloM f g = f <=< htraverse(hhyloM f g) <=< g

[hsyl20]

Wow! Shouldn't this be a PR for the recursion-schemes package? We could integrate it in haskus packages but it seems much more general.

[xgrommx]

@hsyl20 I have some discussion about it https://github.com/ekmett/recursion-schemes/issues/43 But probably we can keep it standalone in haskus packages

[xgrommx]

I have one question, how can I install current version with support for EGADTs but via github?

[hsyl20]

@hsyl20 I have some discussion about it ekmett/recursion-schemes#43 But probably we can keep it standalone in haskus packages

Alright we can include it in Haskus.Utils.Functor.

I have one question, how can I install current version with support for EGADTs but via github?

If you use stack, you can easily add a git extra-deps in stack.yaml:

extra-deps:
- git: https://github.com/haskus/packages.git
  commit: a033f0180b42ca4b650716c45a3eb02a79895152 # change commit here
  subdirs:
     - haskus-utils-variant
     - haskus-utils-types
     - haskus-utils-data

I think cabal now supports something like this via cabal.project files but I have never used it.

I am currently uploading newer versions on hackage (to fix #26). But as EAGDT are quite in flux, it could be better to make git deps work.

[hsyl20]

Merged. Thanks again!

There are still some things lacking (TH, etc.) but I think they could be opened as separate PRs (or more specific issues).

I have just uploaded haskus-utils-variant-3.0 on Hackage.

[sheaf]

With cabal you can include the following in your cabal.project (or cabal.project.local):

source-repository-package
  type: git
  location: https://github.com/haskus/packages
  tag: 27b2eee849a3d6fd052f9c0450d69309b3c29d82
  subdir: haskus-utils-variant
          haskus-utils-types
          haskus-utils-data

[xgrommx]

@hsyl20 What is will be HFunctor for HVariantF?

[xgrommx]

@hsyl20 ok, solve problem with HFunctor. But now I don't understand about alg

toHVariantFHead :: forall x xs t e. x t e -> HVariantF (x ': xs) t e
toHVariantFHead v = HVariantF (toVariantFHead @(x t) @(ApplyAll t xs) v)

toHVariantFTail :: forall x xs t e. HVariantF xs t e -> HVariantF (x ': xs) t e
toHVariantFTail (HVariantF v) = HVariantF (toVariantFTail @(x t) @(ApplyAll t xs) v)

instance HFunctor (HVariantF '[]) where
  hfmap _ = undefined

instance (HFunctor (HVariantF fs), HFunctor f) => HFunctor (HVariantF (f ': fs)) where
  hfmap f (HVariantF v) = case popVariantFHead v of
    Right x -> toHVariantFHead (hfmap f x)
    Left xs -> toHVariantFTail (hfmap f (HVariantF xs))

data ValF (h :: Type -> Type) t where
  ValF :: Int -> ValF h t

instance HFunctor ValF where
  hfmap _ (ValF x) = ValF x

val :: Int -> EGADT '[ValF] Int
val x = VF (ValF x)

res :: Identity Int
res = hcata alg (val 10) where
  alg v = _t

[xgrommx]

@hsyl20, @sheaf are u here?

[hsyl20]

Yes. I will look into this later. Reopening to not forget.

[xgrommx]

@hsyl20, @sheaf As I understand it also will be helpful for build extensible mutual recursive construction?

[hsyl20]

You can find an example of EGADTs in use in @sheaf's project:

• AST definition: https://gitlab.com/sheaf/fir/blob/master/src/FIR/AST.hs#L86
• CodeGen operation: https://gitlab.com/sheaf/fir/blob/master/src/CodeGen/CodeGen.hs#L144

BottomUp is a simpler name standing for catamorphism. Algebras are constructed via type-classes (e.g. CodeGen type-class).

I hope that helps. I need to digest it all myself and to write some docs about it.

[xgrommx]

@hsyl20 cool. My question about https://www.reddit.com/r/haskell/comments/3sm1j1/comment/cwyr61h how we can use mutually recursion with EGADTS

[xgrommx]

For example I want convert it to EGADTS

infix 1 :=

data Expr a =  Const  Int
            |  Add    (Expr a)  (Expr a)
            |  Mul    (Expr a)  (Expr a)
            |  EVar   (Var a)
            |  Let    (Decl a)  (Expr a)
  deriving Show

data Decl a =  Var a := Expr a
            |  Seq    [Decl a]
            |  None
  deriving Show

type Var a  =  a

[sheaf]

I don't know exactly what you want, but I expect it would look something like this

type Var a = a

data ConstF expr a where
  ConstF :: Int -> ConstF expr Int
data AddF expr a where
  AddF :: expr a -> expr a -> AddF expr a
data MulF expr a where
  MulF :: expr a -> expr a -> MulF expr a
data EVarF expr a where
  EVarF :: Var a -> EVarF expr a
data LetF expr a where
  LetF :: DeclF expr a -> expr a -> LetF expr a

data DeclF expr a where
  (:=%) :: Var a -> expr a -> DeclF expr a
  SeqF  :: [ DeclF expr a ] -> DeclF expr a
  NoneF :: DeclF expr a

type Expr = EGADT '[ ConstF, AddF, MulF, EVarF, LetF ]

and then pattern synonyms for the constructors

pattern Const = VF ConstF
...

The idea being you leave the recursion open and tie the knot later by taking a fix point (which is what EGADT does). I think you might have to tie the knot manually if you want several mutually recursive open sum types.

[xgrommx]

@sheaf sorry for this question, but how can I implement a simple evaluator?

[sheaf]

It should be rather similar to what hsyl20 said in a previous comment: implement it via a typeclass, with one instance for each constructor, one instance for the variant type, and then one instance to handle the recursion.

[xgrommx]

@sheaf interesting but looks like we cannot create HFunctor for

data LamF ast t where
  LamF :: (ast a -> ast b) -> LamF ast (a -> b)

according your comment https://github.com/haskus/packages/issues/16#issuecomment-566856496

[xgrommx]

@hsyl20, @sheaf no some news?)

[hsyl20]

Regarding your previous comment, I don't know if it's possible to implement a HFunctor for LamF. IIUC it would change the ast type but as it is used in both covariant/contravariant positions in LamF I don't see how to do this. Perhaps you should change the LamF representation to something else (not a Haskell function)?

[xgrommx]

@hsyl20 But what I should do if I want HOAS?

[hsyl20]

Applying transformations to HOAS is harder because of these Haskell functions with the high-order type on the left of the arrow. An approach is to keep HOAS for the EDSL and then to translate HOAS into FOAS before performing transformations.

For example they did this in http://www.cse.chalmers.se/~josefs/publications/haskell2013.pdf See also: https://stackoverflow.com/questions/21771353/differences-between-hoas-and-foas

[xgrommx]

@hsyl20 can u provide some example with haskus?

[hsyl20]

I don't have any. I haven't used EGADT yet. Perhaps @sheaf has some examples to share?

[xgrommx]

@sheaf any news?)

[sheaf]

I'm not clear exactly what you would like to know, but let me try to clarify what I do know.

Say we have the following HOAS constructors

data LamF ( ast :: Type -> Type ) ( t :: Type ) where
  LamF :: ( ast a -> ast b ) -> LamF ast ( a -> b )

data AppF ( ast :: Type -> Type ) ( t :: Type ) where
  AppF :: ast ( a -> b ) -> ast a -> AppF ast b

data ValueF ( ast :: Type -> Type ) ( t :: Type ) where
  ValueF :: a -> ValueF ast a

For simplicity, the extra parameter has kind Type, but you could do much the same with a different kind (e.g. ast :: k -> Type for some other type k).

Then we recursively instantiate these constructors using EGADT to obtain a HOAS AST:

type AST = EGADT '[ LamF, AppF, ValueF ]

where I remind you that EGADT vs a is coercible to

VariantF ( ApplyAll ( EGADT vs ) vs ) a

That is, it is a variant type where we have recursively instantiated ast in the constructors above with the overall type EGADT vs (in this case vs ~ '[ LamF, AppF, ValueF ]).

Now an evaluator should have type

eval :: AST a -> a

As EGADT is an open sum type as explained above, to implement evaluation we just need to cover the three cases. You can do that by hand and it'll work fine, however I've had more success using a typeclass. So you'd define:

class Eval (ast :: Type -> Type) where
  eval :: ast a -> a

Sylvain's package provides a nice typeclass ToBottomUp :

class BottomUp c vs where
  toBottomUp :: ( forall v. c v => v a -> b ) -> VariantF vs a -> b

with appropriate instances. This means that, if, for each constructor type v, you can provide a function v a -> b when given an instance c v, then you can handle the whole open sum type (which boils down to pattern matching on a sum type).

Hence you can define a set of recursive instances:

-- Handle the individual constructors
instance Eval ast => Eval ( LamF ast ) where
  eval ( LamF f ) = \ a -> eval ( f $ Val a )
instance Eval ast => Eval ( AppF ast ) where
  eval ( AppF f a ) = ( eval f ) ( eval a )
instance Eval ValueF where
  eval ( ValueF v ) = v

-- Handle the open sum type using `BottomUp`
instance BottomUp Eval vs => Eval (VariantF vs) where
  eval = toBottomUp @Eval eval

-- Handle the `AST` type using a coercion
deriving via VariantF ( ApplyAll (EGADT vs) vs )
  instance BottomUp Eval ( ApplyAll (EGADT vs) vs )
        => Eval ( EGADT vs )

here I've defined

pattern Val a = VF ( ValF a )

using Sylvain's pattern synonym VF.

This extends nicely to adding more constructors. When you forget to handle constructors, instance resolution will fail because it won't be able to deduce that Eval :: Type -> Constraint is satisfiable for each constructor ( relative to the definition AST = EGADT vs).

I don't know anything about recursion schemes so I'm not qualified to comment on that.

I hope that's helpful; I can't really answer usefully unless you have a more specific question.