Stream: Coq users

Topic: Extracting Functor typeclass to Haskell

view this post on Zulip Julin S (Sep 12 2022 at 09:52):

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

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.

view this post on Zulip Li-yao (Sep 12 2022 at 10:13):

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.

view this post on Zulip Julin S (Sep 12 2022 at 10:49):

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?

     : (nat -> nat) -> option nat -> option nat

view this post on Zulip Li-yao (Sep 12 2022 at 10:52):

You would tell fmap to throw away its argument.

view this post on Zulip Paolo Giarrusso (Sep 12 2022 at 13:36):

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: Feb 06 2023 at 12:04 UTC