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
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.
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?
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
Ah.. yes it should've
Int instead of
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