Mutually recursive EADTs

[MonadicT]

I am modeling a mutually recursive data structure (AST) and unable to make sense of the type check errors from GHC. Here is the essence of the problem.

data AF b f = AF b deriving (Functor)

eadtPattern 'AF "A"

data BF a f = BF a deriving (Functor)

eadtPattern 'BF "B"

foo :: EADT '[AF b, BF a] -> EADT '[AF b, BF a]
foo b = A b

The error is:

src/Types2.hs:390:9: error: • Couldn't match type ‘Haskus.Utils.Types.List.Index' (Haskus.Utils.Types.List.IndexOf' (Haskus.Utils.Types.List.MaybeIndexOf' 0 (AF (EADT '[AF b, BF a]) (EADT '[AF b, BF a])) '[AF b (EADT '[AF b, BF a]), BF a (EADT '[AF b, BF a])]) (AF (EADT '[AF b, BF a]) (EADT '[AF b, BF a])) '[AF b (EADT '[AF b, BF a]), BF a (EADT '[AF b, BF a])]) '[AF b (EADT '[AF b, BF a]), BF a (EADT '[AF b, BF a])] '[AF b (EADT '[AF b, BF a]), BF a (EADT '[AF b, BF a])]’ with ‘AF (EADT '[AF b, BF a]) (EADT '[AF b, BF a])’ arising from a use of ‘A’ • In the expression: A b In an equation for ‘bar’: bar b = A b • Relevant bindings include b :: EADT '[AF b, BF a] (bound at src/Types2.hs:390:5) bar :: EADT '[AF b, BF a] -> EADT '[AF b, BF a] (bound at src/Types2.hs:390:1) | 390 | bar b = A b | ^^^

I was expecting the type of A b to EADT '[AF b, BF a] but clearly it's not. My questions is, how do I decode this error?

[hsyl20]

That's some ugly error message :/

To decode/debug this, notice that the innermost type family doesn't reduce:

Haskus.Utils.Types.List.MaybeIndexOf'
0
(AF (EADT '[AF b, BF a]) (EADT '[AF b, BF a]))
'[AF b (EADT '[AF b, BF a]), BF a (EADT '[AF b, BF a])]

To reduce this, the solver would have to find that b ~ (EADT '[AF b, BF a]) but then b would be an infinite type.

foo :: EADT '[AF b, BF a] -> EADT '[AF b, BF a] foo b = A b I was expecting the type of A b to EADT '[AF b, BF a] but clearly it's not.

But b :: EADT '[AF b, BF a] so the types are:

foo :: EADT '[AF b, BF a] -> EADT '[AF (EADT '[AF b, BF a]), BF a]
foo b = A b

-- or with a synonym:

type Ast a b = EADT '[AF b, BF a]

bar :: Ast a b -> Ast a (Ast a b)
bar b = A b

The types corresponding to your function would be:

data AF f = AF f deriving (Functor)
eadtPattern 'AF "A"

data BF f = BF f deriving (Functor)
eadtPattern 'BF "B"

foo :: EADT '[AF,BF] -> EADT '[AF,BF]
foo b = A b

But I don't know if that's what you had in mind?

[MonadicT]

Thanks for your response.

Some of the error messages are inscrutable to me and I need to understand the library better.

I didn't do a good job of framing my question. Let me work on a better example and get back on this.

[MonadicT]

Here is a better example of my problem (Github won't let me attach ".hs" files)

The Expr and Decln data types are pared-down versions. The issue is, LetF and DeclF are not functors but bi-functors. I think the problem of implementing EADTShow instance for them captures the mutual recursion requirement. Given the way code is written, the application of eadtShow doesn't type check.

I attempted to add constraints to instance EADTShow but that didn't feel like it was the right approach. Maybe I am looking to do the impossible here or missing something obvious.

Hope that conveys what I am trying to do.

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}

module Foo where

import Haskus.Utils.EADT
import Haskus.Utils.EADT.TH
import Haskus.Utils.Variant
import Haskus.Utils.VariantF

data LetF d e = LetF d e deriving (Functor)

eadtPattern 'LetF "Let"

data DeclF e d = DeclF String e

eadtPattern 'DeclF "Decl"

type Expr d = EADT '[LetF d]

type Decln e = EADT '[DeclF e]

instance EADTShow (LetF d) where
  eadtShow' (LetF d e) = mconcat ["let " {- eadtShow d, -}, " in ", e]

instance EADTShow (DeclF e) where
  eadtShow' (DeclF s e) = mconcat [s, "=" {- ,eadtShow e -}]

[hsyl20]

I see. The following instances typecheck:

instance (d ~ EADT xs, BottomUpF EADTShow xs) => EADTShow (LetF d) where
  eadtShow' (LetF d e) = mconcat ["let ", eadtShow d, " in ", e]

instance (e ~ EADT xs, BottomUpF EADTShow xs) => EADTShow (DeclF e) where
  eadtShow' (DeclF s e) = mconcat [s, "=" ,eadtShow e]

These instances are very generic (any EADT with EADTShow instances can be used for d and e). I'm not very happy that the implementation leaks into client code (BottomUpF). We could hide it with a constraint synonym and I should perhaps use it to define eadtShow:

type EADTShowC d xs =
  ( d ~ EADT xs
  , BottomUpF EADTShow xs
  )

instance (EADTShowC d xs) => EADTShow (LetF d) where
  eadtShow' (LetF d e) = mconcat ["let ", eadtShow d, " in ", e]

instance (EADTShowC e xs) => EADTShow (DeclF e) where
  eadtShow' (DeclF s e) = mconcat [s, "=" ,eadtShow e]

I attempted to add constraints to instance EADTShow but that didn't feel like it was the right approach. Maybe I am looking to do the impossible here or missing something obvious.

It depends how extensible you want your datatypes to be. With the current code there is nothing binding Decln and Expr together. We can use some newtypes to fix the expression and declaration types:

newtype Expr  = Expr (EADT '[LetF Decln])
newtype Decln = Decln (EADT '[DeclF Expr])

instance EADTShow (LetF Decln) where
  eadtShow' (LetF (Decln d) e) = mconcat ["let ", eadtShow d, " in ", e]

instance EADTShow (DeclF Expr) where
  eadtShow' (DeclF s (Expr e)) = mconcat [s, "=" ,eadtShow e]

But it makes them no longer extensible...

Sadly I don't have a better answer for mutually recursive types. It seems like we would have to steal some ideas from https://hackage.haskell.org/package/multirec or https://victorcmiraldo.github.io/data/tyde2018_draft.pdf

[MonadicT]

Thanks for your response.

These instances are very generic (any EADT with EADTShow instances can be used for d and e). I'm not very happy that the implementation leaks into client code (BottomUpF). We could hide it with a constraint synonym and I should perhaps use it to define eadtShow:

This is actually fine for my purposes. I can definitely live with adding constraints synonym to my typeclasses.

It depends how extensible you want your datatypes to be. With the current code there is nothing binding Decln and Expr together. We can use some newtypes to fix the expression and declaration types:

I don't think I intended Decln and Expr to be completely detached.

Sadly I don't have a better answer for mutually recursive types. It seems like we would have to steal some ideas from https://hackage.haskell.org/package/multirec or https://victorcmiraldo.github.io/data/tyde2018_draft.pdf

I have a multirec-based representation but I really like the approach taken in your library. Thanks for your help and I am going to close this issue.