I had been trying to 'hello world' style stuff with coq extraction to haskell and tried this:
Require Extraction.
Extraction Language Haskell.
Require Import ExtrHaskellNatNum.
Fixpoint add (a b:nat):nat :=
match a, b with
| O, b => b
| S a', b => S (add a' b)
end.
Recursive Extraction add.
This results in the following Haskell snippet:
module Main where
import qualified Prelude
data Nat =
O
| S Nat
add :: Nat -> Nat -> Nat
add a b =
case a of {
O -> b;
S a' -> S (add a' b)}
Is there a way to have deriving Show
along with the definition of the Haskell form of Nat
so that we can print the values when we try it out with ghci?
And would it be possible for the extracted code to directly use the haskell integers instead of a newly defined type Nat
?
Is there no way to do that in a certified way?
And would it be possible for the extracted code to directly use the haskell integers instead of a newly defined type Nat?
Is there no way to do that in a certified way?
Sadly no.
Note that Coq's standard library already provides the relevant directives, so you can just do From Coq Require Import ExtrHaskellNatInteger ExtrHaskellNatNum.
As for the certification, extraction itself is not certified, so the point is moot. But you can still look at the files ExtrHaskell*.v
and see whether something is amiss.
another approach is using hs-to-coq, then the problem is trusting the translation from Haskell into Coq, rather than the other way around: https://github.com/plclub/hs-to-coq
But at least the printing / deriving Show
issue becomes moot.
Regarding the use of Extract Inductive
, we would need to have constrtuctors for haskell integers, right? But Haskell integers are sort of hardcoded and doesn't have constructors. Isn't that so (not sure if that's indeed the case).
Ah.. extraction itself isn't verified. Yeah, then not much of a point talking about certification of extraction internals..
But at https://coq.inria.fr/library/Coq.extraction.ExtrHaskellNatNum.html, there's a message saying:
Efficient (but uncertified) extraction of usual nat functions into equivalent versions in Haskell's Prelude that are defined for any Num typeclass instances. Useful in combination with Extract Inductive nat that maps nat onto a Haskell type that implements Num.
Extraction itself isn't verified, then why mention that extraction of nat functions isn't certified specially? Is there some detail that I am missing?
No it's just formal verification people being extra cautious as usual.
Each non-certified component is an addition to your TCB.
IOW, you need to trust not just extraction but also the specific mapping to integers.
Last updated: Oct 13 2024 at 01:02 UTC