Stream: Coq users

Topic: Extraction: nat to Integer (Haskell)

Julin S (Sep 03 2022 at 04:01):

I was trying out coq extraction to haskell.

While extracting Coq's nat to Haskell's Integer, a nat value like 2 gets extracted as succ (succ 0) instead of just 2.

Though succ (succ 0) matches the coq definition of 2:nat (S (S O)).

Is there a way to make the extraction of 2:nat (Haskell) to be just 2:Integer (Haskell) instead of succ (succ 0) (Haskell)?

(The same seems to happen in the ocaml extraction as well.)

This is what I had been trying:

Require Import ExtrHaskellBasic.
Require Import ExtrHaskellNatInteger.
Extraction Language Haskell.
Definition foo := 2.
Extraction foo.
Recursive Extraction foo.

This gave:

foo :: Prelude.Integer
foo =
  Prelude.succ (Prelude.succ 0)

Can we make the Prelude.succ (Prelude.succ 0) just 2?

Guillaume Melquiond (Sep 03 2022 at 05:43):

No. As you wrote, it matches the definition. So, it would require a lot of hardcoding in the extraction plugin to produce something else.

Julin S (Sep 03 2022 at 15:31):

Could it make any difference if use a type other than nat? Like N?

Paolo Giarrusso (Sep 03 2022 at 16:37):

I would expect GHC’s optimizer to constant fold these expressions, maybe with some convincing

Last updated: Oct 04 2023 at 22:01 UTC