Notation "~>" for natural transformations and simplified Fix

[Lysxia]

• New notation E ~> F for forall T, E T -> F T and use that where possible.

  • I'm not too convinced about making the T implicit (it was, for some functions), I think an extra underscore is a little price to pay for the convenience when it needs to be explicit.

  • For the reader interpreters, the type E ~> readerT R (itree F) doesn't seem too convenient compared to R -> E ~> itree F, which is why I chose this way.

• Rework Fix, removed MutFix. The new combinators are mrec and rec.

  • the name mfix is misleading for Haskellers (mfix :: MonadFix m => (a -> m a) -> m a has entirely different semantics)

  • The idea is to view, for any D : Type -> Type (user-defined), a mutually recursive definition of the effect D (defining a function for each constructor of D) as a morphism D ~> itree (D +' E). Then normal recursion is a special case where D has a single constructor. (I wrote a detailed example in Fix.v)

  • The parametric version is missing. It could be added, but seems more cumbersome to use than the current specialized versions.

• Added translate : (E ~> F) -> itree E ~> itree F (mentioned by Steve in this comment https://github.com/DeepSpec/InteractionTrees/pull/49#issuecomment-460687880).

• Renamed Convertible -> Subeffect (but really use the -< notation everywhere)

• Split the definition of sum1 out of OpenSum, which now only contains the type class implementation (most of the internal code actually doesn't depend on these classes, as opposed to sum1 itself).

[Zdancewic]

This cleanup looks great! We should merge to master as soon as we can.

[gmalecha]

I actually had some thoughts about this. I can try to propose them in another pull request. In particular, I don't really understand the benefit of the handleF abstractions. Pattern matches seem easy to understand and the different variants of handleF seem strange.

[Lysxia]

The point is to make the common structure between the various interpreters more explicit. And, while pattern-matches are easy to understand, their syntax is quite heavyweight, especially in proofs where we have little control over formatting. The pattern of handleF is common enough to be worthwhile to abstract, and it's not really much of an abstraction, rather it is a thin layer of sugar.

match t.(observe) with
| RetF r => Ret r
| TauF t => Tau (interp f _ t)
| Vis e k => vis e (fun x => interp f _ k)
end

=

handleF (interp f _)
  (fun _ e k => vis e (fun x => interp f _ k))
  t.(observe)