Stream: Coq users

Topic: Extraction: Inductive type with args

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?

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):

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.

Julin S (Jul 28 2022 at 07:42):

(deleted)

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: Apr 18 2024 at 23:01 UTC