Mutually recursive expression types?

[mrkgnao]

I'm thinking about implementing the System DC language (from this paper, essentially "dependent GHC Core", to save you a click) using Bound.

The problem is that it has mutually recursive types for terms and coercions, like so:

data Tm a 
  = TmVar a | TmConv (Tm a) (Co a) 
  | TmPi (Tm a) (Scope () Tm a) | TmCoAbs (Tm a) (Scope () Co a) | ...
data Co a = CoVar a | CoRefl (Tm a) | CoSym (Co a) | CoPiFst (Scope () Co a) ...

so I don't think Monad instances are happening for either.

Some points:

• Co nodes appear in the Tm type, and vice versa, as noted
• Scope b Co a appears in both types
• Scope b Tm a only appears in the first (as far as I can tell)

How would I modify these types to support something akin to @gelisam's "sideways" imperative example?

The semantics I want are captured by the simple-minded types I wrote above; unlike in the Imperative example, I have no need for bound variables being unavailable in certain parts of the ASTs or anything of the sort.

Edit: also see this comment below, it appears I need two kinds of binders

[mrkgnao]

@ollef suggested that I generalise the types a little, perhaps modifying Tm and Co enough to give them Bound instances.

Consider the following condensed form of the types, which should be sufficient to demonstrate all the features of the actual problem.

data Tm a = TmP a | TmI (Tm a) (Co a) | TmS (Scope' Tm a) (Scope' Co a)
data Co a = CoP a | CoI (Co a) (Tm a) | CoS (Scope' Co a) (Scope' Tm a)

I managed to generalise it to the following, per the Imperative example:

data Tm co a = TmP a | TmI (Tm co a) (co a) (Tm (Scope' (Tm co)) a) (Tm (Scope' co) a)
data Co tm a = CoP a | CoI (Co tm a) (tm a) (Co (Scope' (Co tm)) a) (Co (Scope' tm) a)

and then take a sort of fixed-point for each:

newtype Tm a = MkTm (TmF Co a)
newtype Co a = MkCo (CoF Tm a)

but I don't know where to go from here. I don't think these fixed-points have Monad instances either.

[tomjaguarpaw]

I think what you have got here is strictly more general that what bound deals with, because you have two different types of thing that can be bound Tm and Co. This means you need to generalise the bound machinery. If you define

data Tm a b
  = TmVar a | TmConv (Tm a) (Co b) 
  | TmPi (Tm a) (Scope () Tm a) | TmCoAbs (Tm a) (Scope () Co b) | ...

data Co a b = CoVar b | CoRefl (Tm a) | CoSym (Co b) | CoPiFst (Scope () Co b) ...

then I think you have something that is kind of "bimonadic" in the sense that you have operations

Tm a b -> (a -> Tm a' b') -> (b -> Co a' b')

Co a b -> (a -> Tm a' b') -> (b -> Co a' b')

Then I think you can generalise the bound machinery to something that works with these kinds of "bimonadic" things instead of plain Monads.

[mrkgnao]

I did try something along similar lines (again, the idea was Olle's, who also came up with signatures similar to what you're describing):

data Tm cv tv = TmVar tv | ... | TmConv (Tm cv tv) (Co tv cv) 
data Co cv tv = CoVar cv | .. (Tm tv cv) ...

I wrote Bifunctor etc instances but never got as far as what you (both) are suggesting.

Something I just realised: I'm also missing another subtlety, which is that there are two types of binders in this language. In the attached images, c means a CoVar, and x means a TmVar.

Does this mean I should have two variants on Scope, one for CoVar b a and one for TmVar b a? Or will just using something like Scope (CoVar ()) be enough?

[tomjaguarpaw]

Interesting. Yes, you might need two scopes, one which scopes over variables in the first type parameter and one which scopes over variables in the second.

[mpickering]

I tried to use bound to implement a language which had two different kinds of binders like this and found that it was far too inflexible to deal with it properly. I wouldn't bother trying to smash it around to fit. In the end I just used strings for variable names and renamed when doing substitution.

[ekmett]

You might want to look at something like how we handle this sort of thing in Ermine:

https://github.com/ermine-language/ermine/blob/02b456e3cc32db4bb2374496263d5a8f683ffd22/src/Ermine/Syntax/Term.hs#L216

That said, if I had it to do over again, I'd probably join the term and type level into one ADT and used one type of variable binding.

Alternately, this is actually a good point where unbound may be more appropriate than bound.

[mrkgnao]

@ekmett thanks for the reference.

I believe the (Tm, Flip Co) pair is a monad in Hask * Hask, if one defines type Flip bif a b = bif b a, in the sense of this SO answer:
https://stackoverflow.com/questions/13556314/biapplicative-and-bimonad

so @tomjaguarpaw was right in a way in predicting the type of bibind.

Indeed, we have TmVar :: y -> Tm x y and CoVar :: x -> Co y x, and all occurrences of Co occur in the Co y x form, so flipping the indices to give CoVar :: x -> Co x y should be fine. I chose to do this because this gives a sensible pair of Functor instances.

http://lpaste.net/1398906578140135424

Edit: I've since corrected the indices in Tm, giving up fmap for a much less confusing API.

[mrkgnao]

I think we can close this now, since I've more or less settled on an extra-Bound solution to my problem.