Julin S (Aug 01 2022 at 09:18): 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?
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.
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?
Julin S (Aug 01 2022 at 10:35):Tried using Extract Constant on a coq typeclass, but it said it is not a constant.
Li-yao (Aug 01 2022 at 10:36):Coq typeclasses are a surface-level feature, after typechecking they're just regular records.
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.
Julin S (Aug 01 2022 at 10:41):Aren't records not extractable either?
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
*)
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: Oct 13 2024 at 01:02 UTC