The Coq mailing list

[Merlin Göttlinger <megoettlinger AT gmail.com>]

Hi,

Joachim Breitner <mail AT joachim-breitner.de> schrieb am Mo., 8. Jan. 2018 um 11:04 Uhr:

Hi,


Am Montag, den 08.01.2018, 08:23 +0000 schrieb Merlin Göttlinger:
> sure. My guess would be that I messed up the encoding of the
> hierarchy and the fmap call in the implementation of traverse is
> therefore not resolved to be be the Vector.map call.
> https://gist.github.com/mgttlinger/db35a3748f1dfe68c152678f9a714c06

ah, you are using features I have not played around with (e.g. :>, and
default definitions in a record).

I just tried implementing traverse like this:

  Definition traverse `{T: Traversable} `{@Applicative G} {t u} : (t -> G u) -> F t -> G (F u) :=

    let f := T _ (t_f__) in fun f ft => sequence (fmap f ft).

As to not rely on the default implementation in the record. That didn't change anything.

Implementing traverse at the instance creation also didn't help.

I suspect it could be because my implementation is defined interactively.

 Definition vSequence {G} {n} `{Applicative G} : forall T, Vector.t (G T) n -> G (Vector.t T n).

    intros. induction X; pose proof _f as f; pose proof _p as p. apply pure; trivial. apply (@point (fun f => Vector.t f 0) _ _). eapply ap. apply (fmap (fun a b => a :: b) h). exact IHX. 

  Defined. 

This is the definition. The Instance is then essentially

Definition vTraversable {G} {n} : @Traversable__Dict (fun t => Vector.t t n) G := {| sequence__ _ := vSequence;

|}.    

  Global Instance vector_Traversable {n} {G} : @Traversable (fun t => Vector.t t n) G := fun r f => f vTraversable.

  

Does it work if you do not give the definition of traverse__ in the
Record definition, and instead give it during your Instance? Where is
your Instance?

> What is the "local go" pattern? A quick google lead me only to things
> related to Go-lang.

There might be a better name. It is the problem that nested recursion
through map defined like

Fixpoint map f xs := match xs with
        | [] => []
        | x :: ys => f x :: map f ys end.

fails but

Definition map f :=
   fix go xs := match xs with
        | [] => []

  | x :: ys => f x :: go ys end.

works.

Good to know.

Cheers,

Merlin