quint
quint copied to clipboard
Deprecate and remove the ambiguous form of type annotation
If I have
def condition(f: int => bool): bool = {
state.filter(f).size() > 0
}
And decide I want to remove the type annotation on f
and let that be inferred:
def condition(f): bool = {
state.filter(f).size() > 0
}
I now have an ill-typed spec:
static analysis error: error: [QNT000] Couldn't unify oper and bool
Trying to unify ((int) => bool) => bool and bool
def condition(f): bool = {
^^^^^^^^^^^^^^^^^^^^^^^^^^
state.filter(f).size() > 0
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
}
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
I don't think removing a type annotation in this way should change the meaning of the annotations.
I am surprised it is syntax correct. I would expect the parser to report a syntax error in this case.
I don't think it's a parser bug. The parser understands bool
to be the ML-like type signature, and therefore, there is a type error. We currently do not support partially annotated defs (i.e. def(a: int, b): int
is not supported). Perhaps we could, but then we would have to come up with a syntax to disambiguate this from the ML-like signatures (as in Shon's example)
Yep: not a parser bug. I think it's rather a design bug ;)
The problem is that with 1 operator lambdas it looks like a partial annotation to the user, and this is what they'd expect coming from an ML, but it actually changes the meaning of the bit after the :
. This is not nice behavior IMO.
I suggest we drop support this ambiguous, kind of confused, form of annotation entirely. If we want to be able to succinct signatures for operators, rather than interleaving it with the operator parameters, we can introduce a dedicated, unambiguous signature for that. And if we ever introduce the ability to define bindings like
def f = (a, ..., c) => foo
Then the current annotation approach will work for annotating operator signatures as is.