Stream: Coq users

Topic: ✔ fmap in coq-ext-lib


view this post on Zulip Julin S (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?

view this post on Zulip Julin S (Aug 24 2022 at 09:15):

Is it because of some type class?

view this post on Zulip Julin S (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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Julin S (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.

view this post on Zulip Notification Bot (Aug 24 2022 at 09:37):

Julin S has marked this topic as resolved.


Last updated: Jan 29 2023 at 01:02 UTC