Comments (13)
Awesome @josefs! Thanks for challenging my idea - it turned out a lot better this way!
from gradualizer.
@Zalastax, what you're saying about "safe" downcasts makes perfect sense (although I think words like "sensible" or "consistent" would be better adjectives to use rather than "safe" in this context). I like your suggestion of having upcasting be done by type annotations and "consistent" downcasting done by type assertions. In particular, I really like the idea of forcing people to convert back and forth to any()
if they want to do truly unsafe downcasting.
Just to be clear, type annotation wouldn't only be about upcasting, since, as you say, that happens automatically. It would also convert from any()
.
from gradualizer.
I think the string representation is the easiest and most intuitive of these. Then we can accept types in the usual type notation such as <<_:3, _:_*42>>
and {1..12, [apa|bepa, ...]}
. Possibly we can accept the AST form as well.
from gradualizer.
We can add a macro that converts the second argument to its string representation. (We already use this technique in a test suite, the macro ?t
.)
-define(as_type(E, T), '::'(E, ??T).
foo(A) -> ?as_type(A, pos_integer()).
from gradualizer.
Some thoughts:
Regarding the semantics, there are two reasonable alternatives that we can go with. I'll be referring to them as type annotation and type assertion.
-
Type annotation works like in Haskell, where the declared type has to match both the expression and the context. The declared type doesn't change types as such, just improves type propagation.
The type rule would be:T <: S check(e, T) -------------------- check(e :: T, S)
-
Type assertion converts the type of an expression first to
any()
and then to the asserted type. It lets the programmer say, "no matter what the type of this expression is, I'm now asserting that it has the following type".
Both of these are useful. But I'd argue that type annotations are more useful than type assertions. We don't have to choose between one or the other though. We can have both.
I makes sense to use the '::'
syntax proposed by @zuiderkwast for the type annotation semantics as that corresponds well with how other languages use it. If we want, we can have another syntax (like assert_ty
) for type assertion.
As for the syntax of types, why can't we use any()
to represent the type any()
?
from gradualizer.
Thanks for the semantics! It like it.
As for the syntax of types, why can't we use
any()
to represent the typeany()
?
Well, the expression any()
is a function call unless we transform it, either by stringifying it using a macro or by parse transforming it to something else.
from gradualizer.
Well, the expression any() is a function call unless we transform it, either by stringifying it using a macro or by parse transforming it to something else.
Right. I'm imagining that we would transform them since you suggested we use a parse transform anyway. Using the internal representation as a syntax seems to me like very poor ergonomics.
from gradualizer.
Agree. I suggest we use the string form then for the '::'
function and an optional macro annotate_type
that accepts non-string types.
Nothing prevents us from also supporting a parse transform in the future which would transform the 2nd argument to a string unless it already is a string. However, there is some type syntax that is not valid expression syntax, e.g. ranges and types like fun((...) -> x
. In these cases, a parse transform doesn't work, but then you can still write it as a string.
from gradualizer.
@josefs there's a third valid semantic (used in TS):
Basically, the assertion from type S to T succeeds if either S is a subtype of T or T is a subtype of S
This means you can walk along the subtyping latice in a way that is useful and fairly safe. I don't know how it interacts with blame calculus but, assuming that it doesn't clash, it's the semantics I would greatly prefer for assertions since you can always get the unrestricted semantics by manually taking the step via any.
Supporting both annotations and assertions seems like the best way to go about it. '::' should be an annotation; any ideas for the assertion operator?
from gradualizer.
@Zalastax, I can't say I'm a fan of the Typescript semantics. In order to understand whether you're doing something potentially unsafe you have know the exact type of the expression you're annotating and how it relates to the type you're annotating it with. If you're upcasting, that's totally safe, but if you're downcasting you're doing something potentially dangerous. From a blame calculus perspective it gets very weird because the blame is different depending on whether you're downcasting or upcasting. It's probably possible to fit it into the blame calculus somehow but it's going to get very complicated. I'd rather we didn't have this semantics if we're ever going to have a shot at proving anything about this type system.
from gradualizer.
@josefs what if upcasting is done via type annotations and downcasting via type assertions? That would correspond to how I use assertions in TS, i.e. I annotate potentially wider types for my variables let a : boolean | string = true
and I assert narrower types via as
. Or is it important that annotations can't upcast?
Since upcasting is performed automatically (in most cases or always?) what I've been missing is safe downcasts. Downcasting is inherently unsafe
but some downcasts are more unsafe than others. Without a very expressive type system, downcasts are sometimes necessary. Therefore I want to support it while making it clear when you are downcasting (red flags and horns if possible). Without safe downcasts, every downcast will be done by annotating first any, then the type you want. From experience I know that I've been saved several times by TS checking that the downcast makes sense (types change and the downcast is now illegal) which the compiler can't see if the cast goes via any.
from gradualizer.
annotation macros were implemented in #166 and #167 and documented on the wiki
from gradualizer.
Thanks for adding the wiki page Peti!
from gradualizer.
Related Issues (20)
- Refine bound vars with guards
- Uncaught case clause error #{'Value' => {type,0,tuple,any}} HOT 1
- Keep track of variable bindings & types HOT 5
- Crash with Uncaught error: function_clause HOT 6
- Crash with `Uncaught error: {case_clause, ..` in `typechecker:do_type_check_expr/2`
- Crash with Uncaught error: {badkey, ...} HOT 1
- No clause for gradualizer_lib:pick_value(module()) HOT 2
- No clause of gradualizer_lib:pick_value(any()) HOT 2
- Support the new dynamic() type
- `ok bsr ok` crashes erl_eval:do_apply/7 HOT 4
- An invalid utf32 value can crash eval_bits:eval_exp_field/6
- Crash in gradualizer_fmt:format_type_error: no function_clause_matching
- Crash in typechecker:do_type_check_expr_in/3: bad_key in map_get/2
- Invalid polymorphic code accepted HOT 2
- Support old-style 'catch' keyword HOT 5
- Wrong type in receive...after Timeout
- `binary_to_atom/1` breaks compatibility below OTP 23 HOT 4
- Solving local constraints at each function call to a polymorphic function HOT 6
- support for OTP 26 map comprehensions
- Wrong type location reported?
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from gradualizer.