Stream: Coq users

Topic: Extraction: Inductive type with args


view this post on Zulip Julin S (Jul 28 2022 at 04:43):

I got an inductive type like

Inductive foo (K:Type) : Type :=
| Foo : foo K.

How can I extract this from Coq?

I'm trying to extract to haskell with

(* Assuming there's a haskell type [foo] with constructor [Foo] *)
Extract Inductive foo "K" => "foo" [ "Foo" ].
(* Error at:          ↑↑↑                  *)

But that gave error:

Syntax error: '=>' expected after [reference] (in [command]).

For constants taking arguments we could do like:

Definition bar (A:Type) := id A.

Extract Constant bar "a" => "Bar a".
(* Assuming there's a haskell type [Bar] *)

Is there a similar way for inductive types taking arguments?

view this post on Zulip Yannick Forster (Jul 28 2022 at 06:52):

To extract foo, it suffices to do Require Import Extraction. Extraction foo. If you want the language to be Haskell, here is a minimal example with some renaming first (because in Haskell datatypes start with capital letters):

view this post on Zulip Yannick Forster (Jul 28 2022 at 06:53):

Require Import Extraction.

Inductive Foo (K : Type) : Set :=
| FooC : Foo K.

Definition test {K} (x : Foo K) : Foo K := FooC K.

Extraction Language Haskell.
Extraction Foo.

view this post on Zulip Julin S (Jul 28 2022 at 07:42):

(deleted)

view this post on Zulip Julin S (Jul 28 2022 at 07:46):

I thought I had it, but I think I'll need a closer look. So I deleted the earlier message.


Last updated: Jan 31 2023 at 14:03 UTC