Stream: Coq users

Topic: Extracting type with 2 args to Haskell

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?

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.

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: Sep 30 2023 at 06:01 UTC