Stream: Coq users

Topic: Haskell extraction deriving Show


view this post on Zulip Julin S (Jul 13 2022 at 03:38):

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?

view this post on Zulip Li-yao (Jul 13 2022 at 06:32):

And would it be possible for the extracted code to directly use the haskell integers instead of a newly defined type Nat?

Extract Inductive

Is there no way to do that in a certified way?

Sadly no.

view this post on Zulip Guillaume Melquiond (Jul 13 2022 at 06:54):

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.

view this post on Zulip Karl Palmskog (Jul 13 2022 at 11:44):

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.

view this post on Zulip Julin S (Jul 14 2022 at 04:30):

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).

view this post on Zulip Julin S (Jul 14 2022 at 04:31):

Ah.. extraction itself isn't verified. Yeah, then not much of a point talking about certification of extraction internals..

view this post on Zulip Julin S (Jul 14 2022 at 04:33):

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?

view this post on Zulip Li-yao (Jul 14 2022 at 08:52):

No it's just formal verification people being extra cautious as usual.

view this post on Zulip Paolo Giarrusso (Jul 14 2022 at 11:05):

Each non-certified component is an addition to your TCB.

view this post on Zulip Paolo Giarrusso (Jul 14 2022 at 11:08):

IOW, you need to trust not just extraction but also the specific mapping to integers.


Last updated: Jan 31 2023 at 13:02 UTC