Stream: Coq users

Topic: Extracting type with 2 args to Haskell


view this post on Zulip Julin S (Aug 29 2022 at 03:26):

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?

view this post on Zulip Guillaume Melquiond (Aug 29 2022 at 05:28):

d and 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 Foo (d is not a type), it is also removed from Foo itself, and thus from the type of eg.

view this post on Zulip abab9579 (Aug 29 2022 at 07:20):

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: Jan 31 2023 at 14:03 UTC