Theoretical question: Since Trace is some kind of free monad, leverage cofree comonads?

[bollu]

The interplay between free monads and cofree comonads has been written about to some degree. Would it be possible to expose this theory in the implementation of InteractionTrees to make implementing interpreters easier?

I have no idea if this simplifies or complicates the proof since I've never reasoned with cofree comonads, but one could possibly suspect that this might help?

I'd like to understand

1. If this has been tried before, and if this was successful
2. If something like this should ship with InteractionTrees

[gmalecha]

I haven't dug deeply into this, but I believe this is what eff_hom is all about, right? See #7

[gmalecha]

@bollu Am I right about eff_hom? Or is there something that I am missing (very possible)?

[bollu]

I'm sorry, I didn't have time to look into this so far -- thanks for the nudge, I shall do so tomorrow :)

On Mon 23 Jul, 2018, 04:01 Gregory Malecha, notifications@github.com wrote:

@bollu https://github.com/bollu Am I right about eff_hom? Or is there something that I am missing (very possible)?

— You are receiving this because you were mentioned.

Reply to this email directly, view it on GitHub https://github.com/DeepSpec/InteractionTrees/issues/8#issuecomment-406902186, or mute the thread https://github.com/notifications/unsubscribe-auth/ABncjYmFADXUn-dRS4c47hABYBPJx6F0ks5uJP1GgaJpZM4VO3J- .

-- Sending this from my phone, please excuse any typos!

[gmalecha]

@bollu (nudge).

[bollu]

@gmalecha I am not sure, I think eff_hom is some way to lift morphisms of effects into morphisms of trees, right? I was expecting something like this: http://dlaing.org/cofun/posts/free_and_cofree.html

ie, a type that contains all possible ways of "interpreting" the current value and some kind of "next handler". I can try and mock this up if this helps :)

[gmalecha]

It might be that eff_hom is a first-order representation of this where effects are "pure". Note that there are a lot of different eff_homs specialized to different monads, so it might be possible to try to wrap this up into.

CoInductive Eff_hom (a b : Type -> Type) : Type :=
{ eval : forall t, a t -> itree b (t * Eff_hom a b) }.

Which seems like it might be morally the equivalent of cofree. it should be trivial to give an inclusion of eff_hom_state into this type.

Maybe you can lift the resulting Eff_hom to make:

CoInductive Eff_hom (a b : Type -> Type) : Type :=
{ eval : forall t, a t -> itree b t * Eff_hom a b }.

Though you lose power here.

Perhaps if you add a monadic effect you can interpret other monads as well?

[gmalecha]

This is done.