How can we extract coq functions considering haskell type class constraints?

I got a coq function like

```
Definition addC (x y:nat) : nat := x + y.
```

which I want to map to `(+)`

of Haskell, which has type

```
(+) :: Num a => a -> a -> a
```

How can I properly map the `addC`

(coq) to `(+)`

(Haskell)?

I tried

```
Require Import Extraction.
Extraction Language Haskell.
Definition addC (x y:nat) : nat := x + y.
Extract Constant addC => "(+)".
Extract Inductive nat => int [ "0" "succ" ] "(fun fO fS n -> if n=0 then fO () else fS (n-1))".
Recursive Extraction addC.
```

I got

```
addC :: int -> int -> int
addC = (+)
```

But this won't work since the extracted `addC`

doesn't have the `Num a`

constraint.

```
<interactive>:6:8: error:
• No instance for (Num int) arising from a use of ‘+’
Possible fix:
add (Num int) to the context of
the type signature for:
addC :: int -> int -> int
• In the expression: (+)
In an equation for ‘addC’: addC = (+)
```

How can we work around this?

(deleted)

I don't know Haskell, so I might be wrong, but why did you use lowercase `int`

in the first place? I am pretty sure that, if you had used `Int`

instead, it would have worked just fine. In other words,

```
addC :: Int -> Int -> Int
addC = (+)
```

is a well-typed Haskell definition.

By the way, you might want to use `Integer`

instead of `Int`

, since the former is unbounded and thus a better match for `nat`

.

Ah.. yes it should've `Int`

instead of `int`

. Thanks.

That coupled with `Inlined`

in the extraction command made it work.

Julin S has marked this topic as resolved.

Last updated: Jun 24 2024 at 01:01 UTC