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: Oct 05 2023 at 02:01 UTC