The Coq mailing list

[Joachim Breitner <mail AT joachim-breitner.de>]

Hi,

ok, I found the problem. See
https://gist.github.com/nomeata/1c2bae07c4f4943fc9f9cd64801d9ad4

The CPS-trick helps only if you _never ever_ have a global definition
of a dictionary record. Instead, dictionary records must only occur as
arguments to continuations. So don't write

    Definition vPure : @Pure__Dict (fun t => Vector.t t 1) :=
      {| pure__ _ x := [x] |}.
    Global Instance vector_Pure : @Pure (fun t => Vector.t t 1) :=
      fun r f => f vPure.

but write

    Global Instance vector_Pure : @Pure (fun t => Vector.t t 1) :=
      fun r f => f {| pure__ := fun _ x => [x] |}.

Then your definitions go through!

Joachim

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

Attachment: signature.asc
Description: This is a digitally signed message part