Singleton interfaces

[phischu]

We have records that desugar to data types with a single constructor.

record Stuff[A](x: A)

type Stuff[A] {
  Stuff(x: A)
}

Dually, we could have operations that desugar to an interface with a single method.

operation Work[A](): A

interface Work {
  def Work[A](): A
}

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

interface Work[A] {
  def Work(): A
}

They should be used on the term level as follows:

def myWork = new Work[Int] { () => 0 }

myWork()

The following should not be ok:

def myWork = new Work[Int] { () => 0 }

myWork.Work()

Singleton effect operations should work as before except that it is harder to define Fail and Raise with universally quantified result type.

[b-studios]

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.

[b-studios]

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?

[marvinborner]

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.

[phischu]

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.

1. Symmetry: With records we do not do the following, which would introduce an existential:

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.