Type assertion operator

[Zalastax]

One of the discussions in #83 regards type assertions. A good idea that spawned out of that (thanks @zuiderkwast!) was that adding an id-function that accepts an extra dummy parameter representing a type would allow us to implement type assertions in an efficient and general way without the need to extend the language. To exemplify:

% defined in a header file, I suppose
assert_ty(V, _) -> V.

% Inferred spec: -spec foo(any()) -> integer().
foo(A) -> assert_ty(A, {type, integer}).

-spec bar(integer() | boolean()) -> integer().
% Trust me, due to "circumstances" I'm only ever called with integers...
bar(A) -> assert_ty(A, {type, integer}). 

To provide nicer syntax for type assertions @zuiderkwast suggests a parse transform:

I think it is possible to write a parse transform which allows us to write type annotations on this form: '::'(42, pos_integer()).
[...]
Example: A call to '::'([42], nonempty_list(pos_integer())) is transformed into '::'([42], {type, 0, nonempty_list, [{type, 0, pos_integer, []}]}.

Discussion points:

• What should the semantics of type assertions be? TypeScript sets a good precedence with their type assertion mechanism in that only "safe" type assertions are allowed without using "double assertion" via any. "Basically, the assertion from type S to T succeeds if either S is a subtype of T or T is a subtype of S".
• What should the syntax for types be? We need to limit ourselves to terms that are valid in any context, e.g. using any() to represent any() does not fly. Some ideas: the internal representation of types ('::'([42], {type, 0, nonempty_list, [{type, 0, pos_integer, []}]}), structured data that needs to be massaged (if we add some helper functions, e.g. type(T) -> {type, T}, this might turn out OK), or as a string (which we'll have to parse) e.g. '::'(42, "pos_integer()").

[zuiderkwast]

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.

[zuiderkwast]

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()).

[josefs]

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()?

[zuiderkwast]

Thanks for the semantics! It like it.

As for the syntax of types, why can't we use any() to represent the type any()?

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.

[josefs]

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.

[zuiderkwast]

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.

[Zalastax]

@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?

[josefs]

@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.

[Zalastax]

@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.

[josefs]

@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().

[Zalastax]

Awesome @josefs! Thanks for challenging my idea - it turned out a lot better this way!

[gomoripeti]

annotation macros were implemented in #166 and #167 and documented on the wiki

[zuiderkwast]

Thanks for adding the wiki page Peti!