Ignored type arguments

[kyay10]

It would be nice to have ignored type arguments like in Scala Foo[_] or in Kotlin Foo<*>. This can be useful for interfaces where an operation does not use one of the interface's type parameters, and hence callers don't have to have it at hand. This basically opens the door to existential types as well. Example:

interface Foo[A, B] {
  def foo(): A
}
def foo[A](): A / Foo[A, _] = do foo()

[jiribenes]

Hi, this was implemented slightly more generally by a student in #276 as a part of a thesis, but the PR is unfortunately quite outdated & thus hard to rebase.

But I agree, something like this would be helpful :)

[phischu]

I do not understand what this should mean. How is your example different from

def foo[A](): A / Foo[A, Unit] = do foo()

Or should this be syntactic sugar for

def foo[A, C](): A / Foo[A, C] = do foo()

As mentioned, we considered using this syntax for "please infer", as in zip[Int, _]([1,2,3], ["a", "b", "c"]).

Effekt does have existential types:

type Showable {
  Pack[A](value: A, show: A => String at {})
}

[kyay10]

Underscore can be nice for "please infer" as well (Kotlin uses it as such, and it uses * for ignored type args instead of Scala's _). In this specific case, yes it should be almost syntactic sugar for

def foo[A, C](): A / Foo[A, C] = do foo()

but with the caveat that you don't (and can't) explicitly pass in C. The caveat is that, in some other positions, this doesn't trivially translate to a universal quantifier (specifically, when returned by a function).

I see there's an Any type, but I don't understand it enough to know whether it can help here.