Rename itree?

[gmalecha]

In some of my experimentation, I've been toying with an inductive formulation of itree in addition to the co-inductive definition. I'm wondering if people would be open to some surgery to rename things to be a bit more generic. Here's my concrete proposal (open to suggestions):

Section with_effects.
  Variable eff : Type -> Type.

  Inductive Eff (t : Type) : Type :=
  | Ret (_ : t)
  | Vis {u} (_ : eff u) (_ : u -> Eff t).

  CoInductive CEff (t : Type) : Type :=
  | CRet (_ : t)
  | CVis {u} (_ : eff u) (_ : u -> CEff t)
  | CTau (_ : CEff t).

Note that with Eff, we don't need Tau steps at all (though we don't get divergence either). One thing that I'm not certain about is how to share code between the two definitions. It might be that in practice we can't really share anything due to the duality of the two types.

[bollu]

it's possible to write theorems that provide some notion of equality between the finite and infinite versions, the way we can for lists and streams? That way, there's no sharing of code needed per se, just a bijection. Does this somehow not fit the bill?

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

In some of my experimentation, I've been toying with an inductive formulation of itree in addition to the co-inductive definition. I'm wondering if people would be open to some surgery to rename things to be a bit more generic. Here's my concrete proposal (open to suggestions):

Section with_effects. Variable eff : Type -> Type.

Inductive Eff (t : Type) : Type := | Ret ( : t) | Vis {u} ( : eff u) (_ : u -> Eff t).

CoInductive coEff (t : Type) : Type := | coRet ( : t) | coVis {u} ( : eff u) ( : u -> Eff t) | coTau ( : Eff t).

Note that with Eff, we don't need Tau steps at all (though we don't get divergence either). One thing that I'm not certain about is how to share code between the two definitions. It might be that in practice we can't really share anything due to the duality of the two types.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/DeepSpec/InteractionTrees/issues/12, or mute the thread https://github.com/notifications/unsubscribe-auth/ABncjRUfFE_rTmIaL_8DRld5QDrn1741ks5uJP0GgaJpZM4VaLPh .

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

[bcpierce00]

Calling things coRet, coVis, etc. suggests that coRet is somehow dual to Ret — is this your intuition? (Mine has been that they are not — that Ret and coRet are the same thing, basically, though they live in trees with different shapes…)

• B

On Jul 22, 2018, at 6:30 PM, Gregory Malecha <notifications@github.com mailto:notifications@github.com> wrote:

In some of my experimentation, I've been toying with an inductive formulation of itree in addition to the co-inductive definition. I'm wondering if people would be open to some surgery to rename things to be a bit more generic. Here's my concrete proposal (open to suggestions):

Section with_effects. Variable eff : Type -> Type.

Inductive Eff (t : Type) : Type := | Ret ( : t) | Vis {u} ( : eff u) (_ : u -> Eff t).

CoInductive coEff (t : Type) : Type := | coRet ( : t) | coVis {u} ( : eff u) ( : u -> Eff t) | coTau ( : Eff t). Note that with Eff, we don't need Tau steps at all (though we don't get divergence either). One thing that I'm not certain about is how to share code between the two definitions. It might be that in practice we can't really share anything due to the duality of the two types.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/DeepSpec/InteractionTrees/issues/12, or mute the thread https://github.com/notifications/unsubscribe-auth/AGsIC9DILlMs-TVknwBYq_ACg2coyfLQks5uJP0GgaJpZM4VaLPh.

[bcpierce00]

Or is “co” just for “coinductive”?

(In which case maybe CRet, to avoid confusion?)

On Jul 22, 2018, at 6:48 PM, Benjamin C. Pierce <bcpierce@cis.upenn.edu mailto:bcpierce@cis.upenn.edu> wrote:

Calling things coRet, coVis, etc. suggests that coRet is somehow dual to Ret — is this your intuition? (Mine has been that they are not — that Ret and coRet are the same thing, basically, though they live in trees with different shapes…)

• B

On Jul 22, 2018, at 6:30 PM, Gregory Malecha <notifications@github.com mailto:notifications@github.com> wrote:

In some of my experimentation, I've been toying with an inductive formulation of itree in addition to the co-inductive definition. I'm wondering if people would be open to some surgery to rename things to be a bit more generic. Here's my concrete proposal (open to suggestions):

Section with_effects. Variable eff : Type -> Type.

Inductive Eff (t : Type) : Type := | Ret ( : t) | Vis {u} ( : eff u) (_ : u -> Eff t).

CoInductive coEff (t : Type) : Type := | coRet ( : t) | coVis {u} ( : eff u) ( : u -> Eff t) | coTau ( : Eff t). Note that with Eff, we don't need Tau steps at all (though we don't get divergence either). One thing that I'm not certain about is how to share code between the two definitions. It might be that in practice we can't really share anything due to the duality of the two types.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/DeepSpec/InteractionTrees/issues/12, or mute the thread https://github.com/notifications/unsubscribe-auth/AGsIC9DILlMs-TVknwBYq_ACg2coyfLQks5uJP0GgaJpZM4VaLPh.

[gmalecha]

@bollu It sounds like that would fit the bill. I'm not sure if I have seen anything like that before. Do you have a pointer?

@bcpierce00 You are right, they are definitely not dual. I am using co to mean "co-inductive". Maybe CXxx is better. Hopefully we can hide most of the naming behind the Monad typeclass, but that isn't a reason to give misleading names.

(I will update the proposal in the main issue text to avoid confusion).

[gmalecha]

Note that there will still be some duplication between these types and the ones in #13 . In that PR, I could insert the OutOfFuel as an effect to maintain the connection, which might be a reasonable way to go.

[gmalecha]

@Lysxia @Zdancewic Thoughts on this? I'd like to solidify the interface soon because I'm finding myself starting to duplicate a lot of this code in my own work.

[Lysxia]

I was actually starting to grow fond of the name "interaction tree". In spite of seeming like a bit too concrete of a name, it does give at least one intuition about what those things are to the uninitiated.

[bcpierce00]

I also like ITree pretty well.

   - Benjamin

On Jul 27, 2018, at 19:50, Xia Li-yao notifications@github.com wrote:

I was actually starting to grow fond of the name "interaction tree". In spite of seeming like a bit too concrete of a name, it does give at least one intuition about what those things are to the uninitiated.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub, or mute the thread.