-
Notifications
You must be signed in to change notification settings - Fork 1
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Sequence Constructors, Blocks can't be annotated with types #175
Comments
Blocks also can't be typed. We can put type annotations on the parameters of a block, but not on the result. The above idea could be extended to blocks:
would be a block with type |
In statically typed languages, return types of functions are inferred and then checked against the declaration. I.e., the return type is redundant and mainly there for documentation and to make sure that the inferred type is the one the programmer intended. This would be true as well of a statically-typed Grace. |
... In a purely statically typed dialect, types of blocks and sequences should be able to be inferred (aside from the empty list). If the dialect doesn't do full static typing then can infer return type of block or sequence as unknown if insufficient information. |
I was thinking about this after our meeting was over. The problem I see is that we have defined the types of method results to depend on the type arguments, not on type inference. For example, in
we can infer that the type of Why is this? The type of
Where Yes, we can easily infer that Because We get the same problem when constructing collections. If we don't provide an explicit type argument to the class, and instead define something like
then it doesn't help us to infer that the sequence constructor has type |
static or dynamic type?
I think there will be lots of problems if we start doing static typing properly.
If I keep sayjng |
Static type, because it's only statically that we care. So
which would mean: the static type of the argument to |
The problem with this proposal is that the dynamic semantics of the language would depend on the exact type inference rules, and thus the type inference rules would need to be part of the language definition. This is probably true if we allow inference at all. |
It's not a question of allowing inference. A dialect can infer whatever it likes, and check whatever it infers however it wants. The question is (a) can the type inference affect the operational semantics, i.e. the runtime behaviour, |
I'm beginning to think that we should make sure all of these expressions can take explicit type parameters, and leave it up to dialects to determine which ones can be inferred. The at()ifAbsent(), for example, can take a type parameter for the type returned from the block parameter (though I suspect most of the time it will just be the type of the elements in the collections -- and in many cases it will just raise an exception). In the base (non-statically typed) version of the language type parameters can always be deleted, so it shouldn't muck up programs there. I can imagine a base static-typing dialect that would require all type annotations and another that does some simple inference. It does mean though that we need to admit syntax like
|
The problem with this idea is that the dialect is now changing the program — replacing the implicit ⟦Unknown⟧ arguments by implicit ⟦inferred⟧ arguments. This will change the behaviour of running programs, something that we have so far agreed that dialects should not do. Having a dialect take out a check that it has proved redundant is one thing; this is quite another. |
I fear once again we are getting confused by the difference between static and dynamic type checked. The current spec says that omitted type parameters become A static checker could do whatever it liked to infer tighter types and report static errors based on those types - provided that it does not change the program to bind those parameters at runtime (or otherwise runtime behaviour now depends on types). (I don't think so-called "sound" gradual typing schemes have to do this, but I think they could. Monotonic can narrow types at runtime) So a static checker could certainly raise a type error in the code below, on the grounds that the seq really has static type
But our principles say it shouldn't change the code that gets run, because that would cause this (evil) code to break:
The inference rule above would make the
This will fail a dynamic type test at runtime, but I think must always pass a static type checker. |
We have a notation for a sequence constructor
but we don't have a way of giving it a type. Do we want to add one? The "obvious" syntax would be
For example,
Note that the expressions inside the sequence constructor can be anything at all, so if we say "we should infer the types", then we are committing to inference everywhere — including inferring the result types of methods on arbitrary objects. If we do that, we have Haskell or ML, not Grace. (Is full type inference on an OO language even decidable?)
An alternative is adding type information to sequence constructors to say that the type of a sequence constructor is always
Sequence⟦Unknown⟧
. If you want to assert otherwise, you can convert it:which has type
Sequence⟦String⟧
but will in general require a dynamic check on each element. Of course, a decent implementation (not minigrace) would get rid of the dynamic check in the case where theexp_n
are statically known to be Strings.The text was updated successfully, but these errors were encountered: