search

fmease / lushui

The reference compiler of the Lushui programming language
Apache License 2.0
5 stars 0 forks source link

Allow implicit parameters to lack a type annotation #102

Open fmease opened 3 years ago

fmease commented 3 years ago

This requires type inference for implicit parameters (#2). It supersedes #74.

Declarations and their parameters have to be explicitly annotated with a type compared to parameters of lambda literals and let/in-expressions which do not necessarily need one (unless a type cannot be inferred). This aids readability, it documents the code, leads to better error messages if types somewhere else cannot be inferred and helps the bidirectional inference engine (#1) (since there are not principal types, there is more information around; global type inference is AFAIK impossible in a dependently-typed language).

This proposal relaxes the previously mentioned requirement for implicit parameters (only). For example, the following code should become legal with this change:

identity 'A (a: A): A = a
flip 'A 'B 'C (f: A -> B -> C): B -> A -> C = \b a => f a b
append 'A 'm 'n (v: Vector A n) (w: Vector A m): Vector A (+ n m) = ?_
data 'A (a: A): Type of
id: '(A: _) -> A -> A = identity

The types of those parameters now need to be inferred. This should be possible to implement, see Idris 1 for prior art.

It might be tempting to extend this concept to pi type literals: 'x -> F x => '(x: _) -> F x. However, that is inconsistent and very confusing: A -> A and 'A -> A would suddenly mean completely different things ((_: A) -> A vs. '(A: _) -> A). Sadly, '(n: _) -> '(A: _) -> Array n A -> X does look very appealing compared to e.g implicit name binding (Array n a -> X) like in Haskell or Idris or custom syntax (forall n A -> Array n A -> X) like in Haskell. This ugly syntax will probably discourage writing module-level definitions in a point-free style.

Actually, people can just combine the point-free and non-point-free style:

something 'n 'A 'B: Array n A -> Array n B -> Array n (Tuple A B) = ?point-free-definition
fmease commented 2 years ago

Regarding #74: We might still want to support such implicit parameters "defined inline" with the twist that they cannot ever be explicitly provided (via the <callee> '<argument> syntax) by design. The Rust team is leaning towards such a feature with "impl trait in argument position". Not sure if it's useful in our language. Maybe it becomes useful with "auto params" (trait system impl) to avoid making "helper parameters" part of the API. Not sure. Just wanted to jot that down.