Open phischu opened 1 year ago
Singleton objects currently work (just with a different keyword -- effect
instead of operation
).
https://github.com/effekt-lang/effekt/pull/361/commits/87133e558f5b502be54923b8eafb039981ecede2
However the second variant, that you said should not work, is what is currently implemented.
TBH I would also prefer op
over operation
since in demos I am typing A LOT of operations. I know that this is inconsistent with interface
, record
, and type
.
But typing operation in a demo seems like a lot of effort. I also don't like typing interface
too much; and I realized now why:
effect
I can type with ONLY my left hand. For interface
, the right hand starts with in
and then the left hand types terface
which requires a brief pause in my brain.
Maybe somebody could improve the VSCode plugin so that it can autocomplete our kewords better? @marvinborner you are now our resident LSP expert. Can this be done only in Intelligence or do we need to also do something with the VSCode plugin?
I believe this can be implemented without any changes to the plugin. VSCode sends a textDocument/completion request to the LSP server. I don't think Kiama currently supports this request at all (see this issue or Kiama's Server.scala
). I could look into implementing it, it's probably not that complicated.
Apart from the keyword and the way these operations are invoked there is another difference between the current implementation and what I am proposing.
Currently we have the following:
operation Work[A](): A
interface Work {
def Work[A](): A
}
But I want:
operation Work[A](): A
interface Work[A] {
def Work(): A
}
There are two reasons.
record Stuff[A](x: A)
type Stuff { Stuff[A](x: A) }
2. Usefulness: Effects where the type parameter is at the interface and not at the operation are much more common. One exception is `Fail[A]`, but we are using `Nothing` for this one nowadays. Indeed the current desugaring introduces higher-rank polymorphism, which is a rather unusual thing to want.
We have records that desugar to data types with a single constructor.
Dually, we could have operations that desugar to an interface with a single method.
These are essentially nominally typed functions.
However, as the above example reveals it is not clear where type parameters should be put.
One idea would be to mirror what happens with data types
They should be used on the term level as follows:
The following should not be ok:
Singleton effect operations should work as before except that it is harder to define
Fail
andRaise
with universally quantified result type.