Stream: Coq users

Topic: Multiple binders

Julin S (Jan 31 2023 at 09:36):

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?

Julin S (Jan 31 2023 at 09:36):

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

James Wood (Jan 31 2023 at 12:12):

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

Paolo Giarrusso (Jan 31 2023 at 23:02):

However, a Coq function from List v will have to handle lists of all lengths, and lazy matching ~ is not available

Paolo Giarrusso (Jan 31 2023 at 23:13):

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: Oct 13 2024 at 01:02 UTC