Stream: Coq users

Topic: ✔ fmap in coq-ext-lib

Julin Shaji (Aug 24 2022 at 09:15):

I was trying to use fmap from coq-ext-lib. So I tried:

Require Import ExtLib.Structures.Functor.
Import FunctorNotation.

Compute (S <$> Some 2).
(*
= match ?Functor with
       | {| fmap := fmap |} => fmap
       end nat nat (fun x : nat => S x) (Some 2)
     : option nat
*)

Check (S <$> Some 2).
(*
S <$> Some 2
     : option nat
where
?Functor : [ |- Functor option]
*)

I was hoping to get Some 3 out of S <$> Some 2. What am I missing here?

Julin Shaji (Aug 24 2022 at 09:15):

Is it because of some type class?

Julin Shaji (Aug 24 2022 at 09:18):

fmap's type is like:

Check fmap.
(*
fmap
     : (?A -> ?B) -> ?F ?A -> ?F ?B
where
?F : [ |- Type -> Type]
?Functor : [ |- Functor ?F]
?A : [ |- Type]
?B : [ |- Type]
*)

Wouldn't giving S: nat -> nat make A and B to be nat? With option as F?

Kenji Maillard (Aug 24 2022 at 09:31):

yes that's exactly what happens: in (S <$> Some 2), ?F is unified with option while ?A,?B are unified with nat. The problem is that the ?Functor argument is still missing.

Kenji Maillard (Aug 24 2022 at 09:32):

I guess you should either define an instance of Functor option, or maybe it already exists somewhere in extlib but is not accessible with the specific imports you used.

Julin Shaji (Aug 24 2022 at 09:37):

Thanks.

I did

Require Import ExtLib.Data.Option.                               │

(still not sure if that's the right package, but it works.)

and then

Compute (S <$> Some 2).

gave Some 3.

Notification Bot (Aug 24 2022 at 09:37):

Julin S has marked this topic as resolved.

Last updated: Oct 03 2023 at 02:34 UTC