Update traces to deal with events that do not return

[Lysxia]

This looks good to me.

@gmalecha @Zdancewic any more comments?

[gmalecha]

This looks pretty reasonable to me. A few questions that are probably worth thinking about before we merge:

1. Is it always the best thing to do to drop Taus from traces? This is probably the case.
2. The separation between Event and EventEnd seems slightly strange. Originally, I had thought that there would be an EventOut and EventIn where EventOut sends the message to the environment and EventIn receives the result. This allows you to, for example, give a modular trace prefix to a simple program that calls the environment. With the definition that you are proposing here, the trace is different if the environment terminates or doesn't terminate.
3. Looking to the future. I wonder a little bit about what the Event choice means for concurrent systems. This is by no means a solved question, but in the current definition, you can't really have multiple requests pending on the external environment. This may be desireable, or it may be undesireable, I'm not sure right now.

Closes #21

[Zdancewic]

This definition does look reasonable for what we're doing so far, but I agree with @gmalecha that it probably won't scale to concurrency in the way that we might eventually want. Separating EventIn and EventOut would make things more flexible for future use -- in particular, dealing with asynchronous interactions with the environment.

It is probably worth doing the experiment to see how the EventIn and EventOut traces work out.

There is the question of what the types of these events should be. For example, I can imagine that we might want them to be completely symmetric, perhaps something like:

Variant event (I O : Type -> Type) :=
| EventIn : forall X, I X -> event I O
| EventOut : forall X, O X -> event I O.

Definition trace I O R := list (event I O) * (option R)

For our current purposes, we could define the "type of responses to events E" as something like:

Variant responseE {E : Type -> Type} : Type -> Type :=
| respond : forall X, E X -> X -> responseE X.

The type of traces we would work with for itree E R would be trace E (responseE E) R.

I guess that an alternative to the above would be:

Variant event E :=
| EventOut : forall X, E X -> event
| EventIn : forall X, X -> event.

For the purposes of our current work, it may be best to just stick with @Grain 's trace' for now...

Thoughts?

[gmalecha]

What are we planning on using this trace definition for? If what we want to do fits within its expressivity, then we don't need to dig deeper in the immediate future.

[Lysxia]

Ok then let's merge this.

• This shows formally an equivalence between itrees and sets of/predicates on traces.

• Predicates on traces can be easier to define (by induction on traces), the trade-off being that you might need to ensure on the side that these predicates are prefix-closed.

• Generalization to support concurrency is future work.