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.
Extraction Language Haskell.
Require Import ExtrHaskellBasic.
Require Import ExtrHaskellNatInt.
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?

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.

Could the coq typeclasses be of any help?

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

Tried using `Extract Constant`

on a coq typeclass, but it said it is not a constant.

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

Oh.. Had't known that..

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

Aren't records not extractable either?

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
*)
```

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: Jun 25 2024 at 15:02 UTC