Stream: Coq users

Topic: ✔ Extraction: Haskell type constraints

Julin S (Aug 30 2022 at 04:52):

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?

Julin S (Aug 30 2022 at 04:54):

(deleted)

Guillaume Melquiond (Aug 30 2022 at 05:52):

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.

Guillaume Melquiond (Aug 30 2022 at 05:54):

By the way, you might want to use Integer instead of Int, since the former is unbounded and thus a better match for nat.

Julin S (Aug 30 2022 at 05:57):

Ah.. yes it should've Int instead of int. Thanks.

Julin S (Aug 30 2022 at 05:57):

That coupled with Inlined in the extraction command made it work.

Notification Bot (Aug 30 2022 at 05:58):

Julin S has marked this topic as resolved.

Last updated: Oct 05 2023 at 02:01 UTC