I got this coq snippet that makes and uses a functor type class.
Require Import Extraction.
Require Import ExtrHaskellBasic.
Require Import ExtrHaskellNatInt.
Extraction Language Haskell.
Class Functor (f: Type -> Type) := {
fmap : forall {A B:Type}, (A -> B) -> f A -> f B
}.
Class Applicative (f: Type -> Type) `{Functor f} :=
{
pure: forall {A:Type}, A -> f A;
ap: forall {A B:Type}, f (A -> B) -> f A -> f B
}.
#[export] Instance option_functor : Functor option := {
fmap {A B:Type} f x :=
match x with
| Some x' => Some (f x')
| None => None
end
}.
Definition optS (f:nat -> nat) (a: option nat): option nat :=
fmap f a.
This gave
__ :: any
__ = Prelude.error "Logical or arity value used"
type Functor f =
() -> () -> (Any -> Any) -> f -> f
-- singleton inductive, whose constructor was Build_Functor
fmap :: (Functor a1) -> (a2 -> a3) -> a1 -> a1
fmap functor x x0 =
unsafeCoerce functor __ __ x x0
option_functor :: Functor (Prelude.Maybe Any)
option_functor _ _ f x =
case x of {
Prelude.Just x' -> Prelude.Just (f x');
Prelude.Nothing -> Prelude.Nothing}
optS :: (Prelude.Int -> Prelude.Int) -> (Prelude.Maybe Prelude.
Int) ->
Prelude.Maybe Prelude.Int
optS f a =
fmap (unsafeCoerce option_functor) f a
A new type with name Functor
got produced.
I wanted to use the Functor
type class that's already there in Haskell.
Something like:
optS :: Functor f
=> (Int -> Int)
-> (Maybe Int)
-> (Maybe Int)
optS f a = fmap f a
How can we do that?
Coq type classes are like inductive types. So doing
Extract Inductive Functor => Functor [ fmap ].
would be like mapping fmap
to something like an mkFunctor
.
There is a command that lets you omit arguments. I haven't tried it. And in any case you would still need post-processing or some hack to insert the constraints in signatures because AFAIK there is no support for them in extraction.
The command that allows us to skip arguments seems to be Extraction Implicit
.
Now (to keep things simpler, to go one step at a time) I am just looking to get:
optS :: (Prelude.Int -> Prelude.Int)
-> (Prelude.Maybe Prelude.Int)
-> (Prelude.Maybe Prelude.Int)
optS f a =
fmap f a
instead of
optS :: (Prelude.Int -> Prelude.Int)
-> (Prelude.Maybe Prelude.Int)
-> (Prelude.Maybe Prelude.Int)
optS f a =
fmap (unsafeCoerce option_functor) f a
But how can the option_functor
be thrown away?
I mean, it's not exactly an argument when we look at from coq, right?
optS
: (nat -> nat) -> option nat -> option nat
You would tell fmap
to throw away its argument.
Another caveat is that Coq typeclasses and Haskell typeclasses don't follow the same rules, and I expect there will be examples where Haskell inference will give different results or fail — at least contrived ones, but there seems to be some chance this would happen by accident. (The easiest way is to shadow a typeclass instance, or pass one by hand).
Last updated: Oct 13 2024 at 01:02 UTC