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`

?

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

Could it make any difference if use a type other than `nat`

? Like `N`

?

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

Last updated: Jun 16 2024 at 01:42 UTC