search

fmease / lushui

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

Parse pi type literal with nameless implicit parameter and emit a warning later #107

Open fmease opened 3 years ago

fmease commented 3 years ago

This is not about discarded parameters (using _) but the following: 'Type -> ?A -> ?A. This is currently a syntax error but it also does not make any sense to assign it a different meaning (e.g. see #102). The given expression does not make much sense semantically since an implicit parameter can never be inferred if it's never bound to a name just like '(_: Type) -> ?A -> ?A or '(unused: Type) -> X -> Y (on the other hand '(unused: Type) -> ?A -> ?A might be useful for interactive editing).

We should warn on 'X -> Y and '(_: X) -> Y for any expressions X, Y suggesting to remove the apostrophe or to name the parameter and use it in the codomain. It's similar to an unused-binding lint (yet to be implemented) except that names are missing.

fmease commented 2 years ago

Note that this would start parsing 'F A -> B as an implicit pi type literal with domain F A , although it looks quite weird tbh.