Effect aliasing

[Orbion-J]

I added the possibility to write effect aliases, similarly as what already exists for types.

• there is a new keyword effectname
• to write an alias for an effect row : effectname MyEffectRow(a, ... ,e::Eff, ...) = { Op1 : type, ... | e } the arguments being type variable of any kind (kinds other than type must be explicit)
• we can have, as above, an open row (the row variable is a parameter of the effect alias) or a closed one (just do not write the | e
• To use it in a signature or in another type or effect alias just apply it with the right arguments as for typename things.
• In arrows, we can use them as row variables: () -MyEffectRow(args)-> () (idem with ~>)
• However, due to lack of kind inference, row variables and aliases have to be used carefully so that links does not think they are of kind type. We need to write them most of the time between braces { | ... }. For instance, if you have effectname E(a::Eff) = {X : ... | a } and a row variable e::Eff, you will have to write E({ |e}). (Idem for another effect alias instead of the variable). This makes the usage of several nested aliases a bit messy, it would be nice if we could avoid it.
• We cannot write recursive effect aliases for now. In the branch visitor, I added another transformer that makes possible simple recursion by inlining a mu type in one pass.
• For now the aliases are replaced by the row they correspond to : we do not keep aliases.
• In the repl, effect alias definitions are printed but without the braces ! Rows are in general printed without braces and the alias body is a row. => this might need to be enhanced

About implementation, I copied and then merged most of the time what existed for typename.

[jamescheney]

I don't know the backstory of this, and haven't had a chance to look at this carefully, but instead of adding a keyword and duplicating a lot of code for typename, would it be possible (and wouldn't it be nicer) to augment typename to allow an optional kind, and generalize it to allow any kind of type alias (with Type being the default used if no explicit kind is given)?

e.g. instead of

effectname MyEffectRow(a, ... ,e::Eff, ...) = { Op1 : type, ... | e }

could we write

typename MyAlias(...) :: K = ty

for any kind K, with Eff being a special case, and just generalize the existing code for aliases to allow this?

The description and comments suggest that this may not be straightforward, because of existing idiosyncrasies, but the above design seems cleaner and something we should work toward (see also #44 and comments about row aliases). Perhaps a constructive compromise could be to adopt this PR with a small change: allowing (in addition or only)

typename  MyEffectRow(a, ... ,e::Eff, ...):: Eff =  { Op1 : type, ... | e }

as a special case without (yet) trying to generalize to allow aliases of any kind.

[Orbion-J]

@jamescheney I can surely do something that looks like that. At least syntacticly, I can check during parsing which kind do we have and use after the same things I ve already done.
I will still try see how complicated it would be to extend to presence, in order to be able to at least use it for every primary kind.

[dhil]

It looks to me like you are not expanding effect aliases in place, but rather following the typename infrastructure. Ultimately we want to do something like that, but as a first step I just wanted to use the expansion-technique to keep the diff and redundancy minimal. Alas, that ship may have sailed.

There are a couple of instances that I am not convinced are correct; I think some more testing and careful thought is necessary, e.g. see my comment about instantiate.ml.

[dhil]

I don't know the backstory of this, and haven't had a chance to look at this carefully, but instead of adding a keyword and duplicating a lot of code for typename, would it be possible (and wouldn't it be nicer) to augment typename to allow an optional kind, and generalize it to allow any kind of type alias (with Type being the default used if no explicit kind is given)?

Ultimately, we want to do something like that. But we before we do that we should have a design in mind. The point of this change is to introduce the minimal thing that let us tweak the programming experience / presentation with / of effects and handlers.

In its current state this patch is more invasive than I had originally intended. However, it is probably fine, but we need to be a bit more careful about mixing kind type and row in one alias environment -- I am sure this approach opens up an avenue for a lot of new bugs.

[Orbion-J]

I fixed the simple things.
I tried to add what james was suggesting, I had to do a a bit of a hack in the parser to make it work but it seems to be ok. I added also a few things for presence but this is neither complete nor working.
Anyway, you are right mixing everything could cause some unexpected behavior as :

links> typename A = Int ;
A = Int
links> effectname B = { Op:() -A-> () } ;
***: Error: File "core/types.ml", line 1435, characters 11-17: Assertion failed 

this should for instance cause a kind mismatch. I think checking in instantiate.ml would help but there could be other issues.

[dhil]

I fixed the simple things. I tried to add what james was suggesting, I had to do a a bit of a hack in the parser to make it work but it seems to be ok. I added also a few things for presence but this is neither complete nor working. Anyway, you are right mixing everything could cause some unexpected behavior as :

links> typename A = Int ;
A = Int
links> effectname B = { Op:() -A-> () } ;
***: Error: File "core/types.ml", line 1435, characters 11-17: Assertion failed 

this should for instance cause a kind mismatch. I think checking in instantiate.ml would help but there could be other issues.

Yes. Do not implement James' suggestion. That's for later when we have worked out a proper design. It is too much to bundle it all up.

[jamescheney]

Do not implement James' suggestion. That's for later when we have worked out a proper design. It is too much to bundle it all up.

Of course, I was just asking if this was a "good enough for now" change or intended as a long-term proper design.

[Orbion-J]

I discussed with Sam today and he suggested to me to add kind information in the alias context. I also added that info to each alias instance, so that we can know easily the kind, without having to compute it. It solves then #1141 (comment). For now I just used the primary kind but it could easily be extended to a complete kind if needed.

Within this setting, we can fail when we encounter a situation like in #1141 (comment) :

links> typename A = Int ;
A = Int
links> effectname E = { X : () -A-> () } ;
<stdin>:1: Kind mismatch: Type argument 0 for type constructor A has kind Type, but an argument of kind Row was expected. 
In:
() -A-> ()

I used the kind mismatch error that already exists. I should probably create a new error because the message is not very appropriate. fixed

[dhil]

LGTM modulo the requested changes.

[dhil]

LGTM. I will merge this tomorrow.