The Coq mailing list

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

Hi,

sorry for the confusion:

https://gist.github.com/mgttlinger/cede4fd8fe96aa7f7996341f878a8eb5

That should be a self contained file that exhibits the desired and the working implementation.

The version with traverse being implemented on instance creation is also in there as traverse'.

Cheers,

Merlin

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

Hi,

I am a bit lost. Can you share a complete minimal working example of
the Coq code that you hoped to work, and also the variant that you
wrote that actually work?

Cheers,
Joachim

Am Montag, den 08.01.2018, 10:53 +0000 schrieb Merlin Göttlinger:
> 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
--
Joachim Breitner
  mail AT joachim-breitner.de
  http://www.joachim-breitner.de/