---
title: Type assertions and type applications
tags: steep, spec
---
This is a spec of adding type assertions and type application syntax to Steep.
Type assertion is a feature similar to *cast*, but we use *assertion* here after the name of the feature of TypeScript. They use *assertion* because of it doesn't have *runtime support*. This is same for Steep. The *assertion* tells how the type checker behaves, but doesn't do anything in runtime.
# Motivating example
One of the most common use cases of `@type var` annotation is initializing local variables.
```ruby=
# @type var strings: Array[String]
strings = []
# @type var path: Pathname?
path = nil
```
`strings` would have type `Array[untyped]` without the `@type var strings: ...` annotation. `path` would have type `nil` without the `@type var path: ...` annotation.
These annotations can be removed if the type of the right hand side can be declared with casts.
**Note that the `as` is a pseudo syntax.** That is not supported by Ruby/Steep.
```ruby=
strings = [] as Array[String]
path = nil as Pathname?
```
Note that the `as` syntax must be associated with the right hand side of the assignments.
The following code has *false assertion* that cannot be satisfied, but we expect the type of `strings` is `Array[String]`.
```ruby=
strings = {} as Array[String]
```
If the type assertion is associated to the local variable assignment itself, the type of `string` will be `Hash[untyped]`. Because the assertion works after the type of `strings` is determined.
Another example is *type application*. The following is the example.
```ruby=
strings.each_with_object({}) do |string, count|
# @type var count: Hash[String, Integer]
count[string] = count.fetch(string, 0) + 1
end
```
The `@type var` annotation plays an important role here too, which actually gives a concrete type to the argument `{}`.
The type of `#each_with_object` method is `[T] (T) { (Elem, T) -> void } -> T`. The type annotation gives the type of block parameter `T`, and it propagates to the type of the method parameter.
This works but we want better way that it requires additional line here. This can be written with *type application* syntax `<>`.
**Note that the `<>` is a pseudo syntax.** That is not supported by Ruby/Steep.
```ruby=
strings.each_with_object<Hash[String, Integer]>({}) do |string, count|
count[string] = count.fetch(string, 0) + 1
end
```
The call of `#each_with_object` has an explicit type application of`Hash[String, Integer]` that results in `(Hash[String, Integer]) { (Elem, Hash[String, Integer]) -> void } -> Hash[String, Integer]`.
# Syntax
Steep will have two *extended* syntax rule:
```markdown
node ::= ...
| node `as` type # Type assertion
| node `<` type `,` ... `>` # Type application
```
The `node` inside *type application* is one of the following:
1. `send` node
2. `csend` node
3. `block` node with `send` or `csend` node
4. `numblock` node with `send` or `csend` node
## Concrete syntax by comments
The abstract syntax above cannot be implemented because Ruby doesn't have the syntax constructs. So, we need to define a conversion from *concrete syntax* that can be represented in Ruby to the abstract syntax.
### Type assertion
A comment of format `: ${type}` represents a *type assertion comment*, that associates node and the type of the assertion.
```ruby=
strings = [] #: Array[String]
path = nil #: Pathname?
```
The association is defined as follows:
1. A *type assertion comment* at line `n` is associated to the outer-most node that ends at line `n`, except the following cases
2. Assignment node is skipped during the detection and right hand side will be treated as the outer-most node
3. *Void* nodes (`return`, `break`, `next`) is skipped, and the value node will be treated as the outer-most node
4. `begin` nodes without parens is skpped
```ruby=
hello.world #: Symbol
# ^^^^^^^^^ The associated node
@foo = [] #: Array[String]
# ^^ The associated node
return 1 # : Numeric
# ^ The associated node
hello
world #: bool
# ^^^ The associated node
(bar = 123) #: boolish
# ^^^^^^^^^ The associated node
```
### Type application
A comment of format `$ ${type}, ...` represents a *type application comment* that associates `send` node and the type application.
```ruby=
foo([]) #$ Array[String]
foo( #$ Array[String]
[]
)
foo([]) {|x| x.to_s } #$ Array[String]
foo([]) do |x| #$ Array[String]
x.to_s
end
```
A type application comment is associated to a `send` or `block` node that is:
1. The *selector* is at the same line with the comment
2. The outer call has priority
3. The *operator* style method calls (`x + y`) are ignored
Google Drive
Gist
Clipboard
Sign in with Wallet
