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: Jun 13 2024 at 04:03 UTC