## Stream: Coq users

### Topic: Haskell extraction with type constraints

#### Julin S (Aug 01 2022 at 09:18):

I was trying to have the following haskell code to be extracted from a coq function.

``````pickif :: (Num n, Eq e)
=> e -> e -> n -> n -> n
pickif a b c d = if a==b then c
else b
``````

How can we have type contraints like `Num` and `Eq` incorporated into the coq counterpart of the haskell `pickif` function here?

I tried:

``````Require Extraction.

Definition pickif (a b c d:nat) : nat :=
if (Nat.eqb a b) then a
else b.

Recursive Extraction pickif.
``````

and got (among other things) this:

``````pickif :: Prelude.Int -> Prelude.Int -> Prelude.Int -> Prelude.Int -> Prelude.Int
pickif a b _ _ =
case eqb a b of {
Prelude.True -> a;
Prelude.False -> b}
``````

How can we incorporate the type constraints?

Any idea?

#### Li-yao (Aug 01 2022 at 10:21):

You probably can't do that within Coq. One potential solution is to post-process the extracted code to generalize signatures whenever certain ad hoc types occur in them.

#### Julin S (Aug 01 2022 at 10:35):

Could the coq typeclasses be of any help?

Is there a way to map coq type classes to haskell type classes?

#### Julin S (Aug 01 2022 at 10:35):

Tried using `Extract Constant` on a coq typeclass, but it said it is not a constant.

#### Li-yao (Aug 01 2022 at 10:36):

Coq typeclasses are a surface-level feature, after typechecking they're just regular records.

#### Julin S (Aug 01 2022 at 10:41):

Just did a print on a trivial typeclass and it indeed shows as a normal record.

#### Julin S (Aug 01 2022 at 10:41):

Aren't records not extractable either?

#### Julin S (Aug 01 2022 at 10:44):

Okay, looks like they become `type`.

``````Class Show A : Type :=
{
show : A -> string
}.

Extraction Show.
(*
type Show a =
a -> String
-- singleton inductive, whose constructor was Build_Show
*)
``````

#### Gaëtan Gilbert (Aug 01 2022 at 11:55):

Records are inductive types with some syntax sugar, so you have to use Extract Inductive not Extract Constant if you want to customize their extraction

Last updated: Jan 29 2023 at 06:02 UTC