Allow bundling associated types in interfaces

[apaszke]

It is often convenient to have type-to-type maps (e.g. given a mapping type such as the HashDict of #343, what is its key and value type), and we could easily implement those by putting types in interfaces. For example:

interface Map m
  keyType : Type
  valueType : Type
  lookup : m -> keyType -> Maybe valueType

One challenge here is that keyType has no way of resolving which type class it should use, because m is not mentioned in the type. A potential solution would be to allow prefixing the definitions with indexed (or some other word, naming is hard...) which would append the type parameter as an explicit argument instead of trying to infer it:

-- for keyType : Type we would generate
def keyType [Map m] : Type = <generated>

-- for indexed keyType : Type we would generate
def keyType (m : Type) [Map m] : Type = <generated>

cc @danieldjohnson who had some ideas

[danieldjohnson]

Another potential syntax:

interface Map m
  keyType m : Type
  valueType m : Type
  lookup : m -> keyType -> Maybe valueType

The general idea would be that interface fields could be written referencing any of the binders in the interface type, and those would turn into explicit args instead of implicit ones.

[dan-zheng]

The general idea would be that interface fields could be written referencing any of the binders in the interface type, and those would turn into explicit args instead of implicit ones.

Seems that both options are syntactically viable. Perhaps both could be supported, so users can choose argument implicitness.

[apaszke]

Huh, I do actually like the binders before annotation. It's kind of like Haskell function defs where you can have args on the left of =

[dan-zheng]

It's kind of like Haskell function defs where you can have args on the left of =

Small tangent: could Dex support these pattern-matching-based definitions like Haskell?

fib :: Integer -> Integer
fib 0 = 0
fib 1 = 1
fib n = fib (n-1) + fib (n-2)

Edit: we discussed this yesterday (January 22, 2021) and most people did not like this style of pattern-matching definition. One cited reason is that the function name (fib) must be typed multiple times. A consensus more interesting direction would be "powerful" pattern synonyms in Dex.

[cristianurlea]

Haskell's associated data types come to mind.