Hi.

I was trying to translate this haskell snippet to coq:

```
{-# LANGUAGE RankNTypes #-}
data TreeP a v =
Empty
| Var v
| Mu ([v] -> [TreeP a v])
| Fork a (TreeP a v) (TreeP a v)
newtype Tree a = Hide {
reveal :: forall v. TreeP a v
}
a = Hide $ Mu $ \(~(x:y:_)) -> [
Fork 1 (Var y) (Var x),
Fork 2 (Var x) (Var y)]
```

Is this possible?

How can we bind multiple values where a value being bound is visible to all other values being bound at the same time?

The `Mu`

constructor.

I sort of randomly tried this:

```
Inductive TreeP (A:Type) (V:Type) : Type :=
| Empty: TreeP A V
| Var: V -> TreeP A V
| Mu: ____ ???
| Fork: A -> TreeP A V -> TreeP A V.
```

Am I on the right track in getting this done?

I got the haskell snippet from this paper: https://dl.acm.org/doi/pdf/10.1145/2364527.2364541 (Functional programming with structured graphs)

https://github.com/michaelt/structured-graphs/blob/master/Trees.hs

For non-indexed inductive types, you can use a Haskell-like syntax, like in the second example block here.

However, a Coq function from `List v`

will have to handle lists of all lengths, and lazy matching `~`

is not available

Still, the data type definition should succeed (along what James suggested), and those differences should be solvable (but there are many options, so probably you should experiment and/or ask follow-up questions)

Last updated: Jun 16 2024 at 02:41 UTC