quint icon indicating copy to clipboard operation
quint copied to clipboard

Deprecate and remove the ambiguous form of type annotation

Open shonfeder opened this issue 1 year ago • 4 comments

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.

shonfeder avatar Jun 02 '23 23:06 shonfeder

I am surprised it is syntax correct. I would expect the parser to report a syntax error in this case.

konnov avatar Jun 03 '23 11:06 konnov

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)

bugarela avatar Jun 12 '23 14:06 bugarela

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.

shonfeder avatar Jun 12 '23 14:06 shonfeder

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.

shonfeder avatar Feb 14 '24 12:02 shonfeder