I got a haskell type like
data Foo d a = Nil d a | Cons a (Foo d a)
Corresponding to this, I got this type in Coq:
Inductive D : Type := | dcons. Inductive Foo (d: D) (A:Type) : Type := | Nil : Foo d A | Cons : A -> Foo d A Extract Inductive D => "()" [ "()" ]. Extract Inductive Foo => "Foo" [ "Nil" "Cons" ]. Definition eg:Foo dcons nat := Nil dcons nat. Recursive Extraction eg.
With this, I got
eg :: Foo Prelude.Int eg = Nil
But I was hoping for something like:
eg :: Foo () Int eg = Nil () Int
Why is one argument (
dcons mapped to haskell's
()) not showing up in the extracted code?
A are parameter of your inductive family
Foo. They are only part of the type, not of the values. So, they get erased when extracting
Nil. Moreover, since
d cannot have any impact on the constructors of
d is not a type), it is also removed from
Foo itself, and thus from the type of
To mirror between haskell and coq better, I suggest using GADT syntax. That way, you would have
data Foo d a where Nil :: d -> a -> Foo d a Cons :: a -> Foo d a -> Foo d a
With this, you would have easier time representing it in coq.
Last updated: Sep 30 2023 at 06:01 UTC