Replace `Pure` with `F Identity`?

[bglgwyng]

I’m still getting used to hypertypes, but I’ve noticed that most of my use cases involve F m, where m is especially often a monad. I usually write do-notation code wrapped in _F # do ....

This made me wonder whether Pure and Prune could be replaced by F Identity and F Maybe, respectively. It seems like this might be more convenient and encourage a more canonical style when working with hypertypes.

Has this approach been considered before? Are there semantic, ergonomics, or performance reasons to keep Pure and Prune as separate types?

[yairchu]

That's a suggestion worth considering. Chronologically, F was added after Pure. Possibly it might have been implemented as you suggest otherwise.

Minor points ergonomics-wise:

• Pure is shorter than F Identity, but that can be helped by a type alias
• Using _F # for construction provides fewer hints to type-checking. Perhaps we would want to add a specialized iso specifically for F Identity

Prune is used much less then Pure. We could try migrating off of that first and then seeing what the ergonomics repercussions are for it. By doing a quick check I appear to be using it in Lamdu. I could try making a branch that uses F Maybe there instead and seeing how that looks like.