Stream: Coq users

Topic: Haskell extraction with type constraints


view this post on Zulip Julin S (Aug 01 2022 at 09:18):

I was trying to have the following haskell code to be extracted from a coq function.

pickif :: (Num n, Eq e)
       => e -> e -> n -> n -> n
pickif a b c d = if a==b then c
                 else b

How can we have type contraints like Num and Eq incorporated into the coq counterpart of the haskell pickif function here?

I tried:

Require Extraction.
Extraction Language Haskell.
Require Import ExtrHaskellBasic.
Require Import ExtrHaskellNatInt.

Definition pickif (a b c d:nat) : nat :=
    if (Nat.eqb a b) then a
    else b.

Recursive Extraction pickif.

and got (among other things) this:

pickif :: Prelude.Int -> Prelude.Int -> Prelude.Int -> Prelude.Int -> Prelude.Int
pickif a b _ _ =
  case eqb a b of {
   Prelude.True -> a;
   Prelude.False -> b}

How can we incorporate the type constraints?

Any idea?

view this post on Zulip Li-yao (Aug 01 2022 at 10:21):

You probably can't do that within Coq. One potential solution is to post-process the extracted code to generalize signatures whenever certain ad hoc types occur in them.

view this post on Zulip Julin S (Aug 01 2022 at 10:35):

Could the coq typeclasses be of any help?

Is there a way to map coq type classes to haskell type classes?

view this post on Zulip Julin S (Aug 01 2022 at 10:35):

Tried using Extract Constant on a coq typeclass, but it said it is not a constant.

view this post on Zulip Li-yao (Aug 01 2022 at 10:36):

Coq typeclasses are a surface-level feature, after typechecking they're just regular records.

view this post on Zulip Julin S (Aug 01 2022 at 10:41):

Oh.. Had't known that..

Just did a print on a trivial typeclass and it indeed shows as a normal record.

view this post on Zulip Julin S (Aug 01 2022 at 10:41):

Aren't records not extractable either?

view this post on Zulip Julin S (Aug 01 2022 at 10:44):

Okay, looks like they become type.

Class Show A : Type :=
  {
    show : A -> string
  }.

Extraction Show.
(*
type Show a =
  a -> String
  -- singleton inductive, whose constructor was Build_Show
*)

view this post on Zulip Gaƫtan Gilbert (Aug 01 2022 at 11:55):

Records are inductive types with some syntax sugar, so you have to use Extract Inductive not Extract Constant if you want to customize their extraction


Last updated: Jan 29 2023 at 06:02 UTC