Skip to content

sorbet: avoid Dynamic type, refine examples.rb #35

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.

Sign up for GitHub

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

Open
bennn wants to merge 1 commit into
base: main
Choose a base branch
from
Open

sorbet: avoid Dynamic type, refine examples.rb #35

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -536,7 +536,7 @@ For language details: [SETUP.md](./SETUP.md)
| connectives | O | O | O | O | O | O |
| nesting_body | O | O | O | O | O | O |
| struct_fields | O | O | O | O | O | x |
| tuple_elements | O | O | O | O | O | O |
| tuple_elements | O | O | O | O | O | x |
| tuple_length | x | O | O | O | O | x |
| alias | O | O | x | x | O | O |
| nesting_condition | O | x | x | x | x | O |
Expand All @@ -554,10 +554,10 @@ The results of these examples are demonstrated below.

| Benchmark | Typed Racket | TypeScript | Flow | mypy | Pyright | Sorbet |
|:----------|:------------:|:----------:|:----:|:----:|:-------:|:------:|
| filter | O | O | O | O | O | O |
| filter | O | O | O | O | O | x |
| flatten | O | O | O | O | O | O |
| tree_node | O | x | x | x | x | x |
| rainfall | O | O | O | O | O | O |
| rainfall | O | O | O | O | O | x |



Expand Down
24 changes: 15 additions & 9 deletions Sorbet/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,10 +16,14 @@ Sorbet adds static types to Ruby.

> Q. What is the top type in this language? What is the bottom type? What is the dynamic type? If these types do not exist, explain the alternatives.

* Top = `T.anything`
* Top = `Object`
* Bottom = `T.noreturn`
* Dynamic = `T.untyped`

Technically, `T.anything` is the top type, but since it doesn't support the `.is_a?` method (only type case and casts), we use `Object` to get a more direct encoding for If-T.

<https://sorbet.org/docs/anything>

`T.untyped` is Sorbet’s dynamic type, used for values with unknown types, such as those from untyped Ruby code. It allows any operation but provides no type safety. Sorbet supports gradual typing, so `T.untyped` is common in mixed typed/untyped codebases.

<https://sorbet.org/docs/static>
Expand All @@ -32,8 +36,8 @@ These are standard Ruby classes, chosen for their simplicity and immutability, m

> Q. What container types does this implementation use (for objects, tuples, etc)? Why?

* Hash types for objects: `{ a: T.untyped }` or `{ a: T.any(String, Integer) }`
* Array types for tuples: `[T.untyped, T.untyped]` or `[Integer, T.any(String, Integer)]`
* Hash types for objects: `{ a: Object }` or `{ a: T.any(String, Integer) }`
* Array types for tuples: `[Object, Object]` or `[Integer, T.any(String, Integer)]`
* Union types for sized tuples: `T.any([Integer, Integer], [String, String, String])`

Hashes represent key-value objects, common in Ruby. Arrays serve as tuples, with fixed or variable lengths. Union types model sized tuples by distinguishing lengths (e.g., 2 vs. 3 elements). These types are immutable in the context of the benchmark, ensuring type soundness.
Expand Down Expand Up @@ -98,24 +102,26 @@ The implementation is direct for most benchmarks, using Ruby’s `if`/`else` and

`tree_node` is inexpressible because Sorbet does not have type predicates.

`filter` is inexpressible, again because it requires a predicate, though we have implemented a simple version of `filter`.
`filter` is inexpressible, again because it requires a predicate. That being said, Sorbet can handle direct `.is_a?` checks inside a `filter_map` call.

<https://sorbet.org/docs/flow-sensitive#prefer-xsfilter_map----to-xsfilter--->

`rainfall` fails because `.is_a?` cannot narrow an Object to a Hash.


> Q. Are any examples expressed particularly well, or particularly poorly? Explain.

- Well-expressed: The `rainfall` example is expressed effectively in Sorbet. It uses `T::Hash[Symbol, T.untyped]` to model JSON-like data and `T.let` for type narrowing, closely mirroring the If-T pseudocode. The failure case (`rainfall_failure`) triggers a clear type error by casting `rainfall` to `String`, demonstrating Sorbet’s ability to catch invalid operations.
- Poorly-expressed:
+ The `flatten` example is less elegant than the If-T pseudocode. Sorbet requires separate checks for `is_a?(Array)` and `length == 0`, unlike TypeScript’s `empty?` predicate, which combines both. Additionally, the use of `T.untyped` as the input type and multiple `T.let` assertions for type narrowing makes the implementation more verbose.
+ The `filter` example takes a boolean function instead of a type predicate. It also struggles with return type `T::Array[T.untyped]`, which is too permissive, requiring a return type adjustment to `T::Array[Integer]` to enforce errors.
+ The `flatten` example is less elegant than the If-T pseudocode. Sorbet requires separate checks for `is_a?(Array)` and `length == 0`, unlike TypeScript’s `empty?` predicate, which combines both. Additionally, the use of `Object` as the input type and multiple `T.let` assertions for type narrowing makes the implementation more verbose.


> Q. How direct (or complex) is the implementation compared to the pseudocode from If-T?

The implementations are mostly direct but slightly more complex than the If-T pseudocode due to Sorbet’s static type system. Key differences include:

- Explicit type narrowing with `T.let` and `T.cast` is needed in all examples to satisfy Sorbet’s strict mode, adding verbosity compared to the pseudocode’s implicit type assumptions.
- The `tree_node` example requires recursive type checks with `T::Hash[Symbol, T.untyped]`, which is straightforward but involves more boilerplate than TypeScript’s predicates.
- The `tree_node` example requires recursive type checks with `T::Hash[Symbol, Object]`, which is straightforward but involves more boilerplate than TypeScript’s predicates.
- The `flatten` example’s recursive structure is direct, but the lack of a combined `empty?` predicate and the need for `T.let` assertions increase complexity.
- The `rainfall` example is the most direct, with minimal divergence from the pseudocode, though it still requires explicit null checks and type assertions.

Overall, Sorbet’s lack of type predicates and permissive `T.untyped` necessitate additional type annotations and checks, making the code less concise than the pseudocode or TypeScript equivalents.
Overall, Sorbet’s lack of type predicates necessitates additional type annotations and checks, making the code less concise than the pseudocode or TypeScript equivalents.
41 changes: 14 additions & 27 deletions Sorbet/examples.rb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,34 +4,21 @@
### Code:
## Example filter
## success
sig { params(array: T::Array[T.untyped], callbackfn: T.proc.params(value: T.untyped).returns(T::Boolean)).returns(T::Array[T.untyped]) }
sig { params(array: T::Array[Object], callbackfn: T.proc.params(value: Object).returns(T::Boolean)).returns(T::Array[Integer]) }
def filter_success(array, callbackfn)
result = T.let([], T::Array[T.untyped])
array.each do |value|
if callbackfn.call(value)
result << value
end
end
result
array.filter_map { |x| x if callbackfn(x) }
end

## failure
sig { params(array: T::Array[T.untyped], callbackfn: T.proc.params(value: T.untyped).returns(T::Boolean)).returns(T::Array[Integer]) }
sig { params(array: T::Array[Object], callbackfn: T.proc.params(value: Object).returns(T::Boolean)).returns(T::Array[Integer]) }
def filter_failure(array, callbackfn)
result = T.let([], T::Array[Integer])
array.each do |value|
if callbackfn.call(value)
result << T.cast(value, Integer)
else
result << "string" # Expected error: Cannot append String to T::Array[Integer]
end
end
result
# alt # array.grep(String)
array.filter_map { |x| x if x.is_a?(String) }
end

## Example flatten
## success
sig { params(l: T.untyped).returns(T::Array[Integer]) }
sig { params(l: Object).returns(T::Array[Integer]) }
def flatten_success(l)
if l.is_a?(Array)
if l.length == 0
Expand All @@ -47,7 +34,7 @@ def flatten_success(l)
end

## failure
sig { params(l: T.untyped).returns(T::Array[Integer]) }
sig { params(l: Object).returns(T::Array[Integer]) }
def flatten_failure(l)
if l.is_a?(Array)
if l.length == 0
Expand Down Expand Up @@ -76,7 +63,7 @@ def initialize(value:, children: nil)
raise "Sorbet does not support type predicates"
end

sig { params(node: T.untyped).returns(T::Boolean) }
sig { params(node: Object).returns(T::Boolean) }
def self.is_tree_node_success(node)
raise "Sorbet does not support type predicates"
end
Expand All @@ -95,22 +82,22 @@ def initialize(value:, children: nil)
raise "Sorbet does not support type predicates"
end

sig { params(node: T.untyped).returns(T::Boolean) }
sig { params(node: Object).returns(T::Boolean) }
def self.is_tree_node_failure(node)
raise "Sorbet does not support type predicates"
end
end

## Example rainfall
## success
sig { params(weather_reports: T::Array[T.untyped]).returns(Float) }
sig { params(weather_reports: T::Array[Object]).returns(Float) }
def rainfall_success(weather_reports)
total = T.let(0.0, Float)
count = T.let(0, Integer)
weather_reports.each do |day|
if day.is_a?(T::Hash[Symbol, T.untyped]) && !day.nil?
if day.is_a?(T::Hash[Symbol, Object]) && !day.nil?
if day.key?(:rainfall)
val = T.let(day[:rainfall], T.untyped)
val = T.let(day[:rainfall], Object)
if val.is_a?(Float) && 0.0 <= val && val <= 999.0
total += val
count += 1
Expand All @@ -122,12 +109,12 @@ def rainfall_success(weather_reports)
end

## failure
sig { params(weather_reports: T::Array[T.untyped]).returns(Float) }
sig { params(weather_reports: T::Array[Object]).returns(Float) }
def rainfall_failure(weather_reports)
total = T.let(0.0, Float)
count = T.let(0, Integer)
weather_reports.each do |day|
if day.is_a?(T::Hash[Symbol, T.untyped]) && !day.nil?
if day.is_a?(T::Hash[Symbol, Object]) && !day.nil?
if day.key?(:rainfall)
val = T.cast(day[:rainfall], String)
total += val # Expected error: Expected Integer but found String
Expand Down
24 changes: 12 additions & 12 deletions Sorbet/main.rb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
### Code:
## Example positive
## success
sig { params(x: T.untyped).returns(Integer) }
sig { params(x: Object).returns(Integer) }
def positive_success_f(x)
if x.is_a?(String)
x.length
Expand All @@ -14,7 +14,7 @@ def positive_success_f(x)
end

## failure
sig { params(x: T.untyped).returns(Integer) }
sig { params(x: Object).returns(Integer) }
def positive_failure_f(x)
if x.is_a?(String)
x.is_nan # Expected error: No method 'is_nan' on String
Expand Down Expand Up @@ -55,7 +55,7 @@ def connectives_success_f(x)
end
end

sig { params(x: T.untyped).returns(Integer) }
sig { params(x: Object).returns(Integer) }
def connectives_success_g(x)
if x.is_a?(String) || x.is_a?(Integer)
connectives_success_f(x)
Expand Down Expand Up @@ -83,7 +83,7 @@ def connectives_failure_f(x)
end
end

sig { params(x: T.untyped).returns(Integer) }
sig { params(x: Object).returns(Integer) }
def connectives_failure_g(x)
if x.is_a?(String) || x.is_a?(Integer)
x.length # Expected error: length not defined for String | Integer
Expand Down Expand Up @@ -132,7 +132,7 @@ def nesting_body_failure_f(x)

## Example struct_fields
## success
sig { params(x: { a: T.untyped }).returns(Integer) }
sig { params(x: { a: Object }).returns(Integer) }
def struct_fields_success_f(x)
if x[:a].is_a?(Integer)
x[:a]
Expand All @@ -153,7 +153,7 @@ def struct_fields_failure_f(x)

## Example tuple_elements
## success
sig { params(x: [T.untyped, T.untyped]).returns(Integer) }
sig { params(x: [Object, Object]).returns(Integer) }
def tuple_elements_success_f(x)
if x[0].is_a?(Integer)
x[0]
Expand Down Expand Up @@ -195,7 +195,7 @@ def tuple_length_failure_f(x)

## Example alias
## success
sig { params(x: T.untyped).returns(Integer) }
sig { params(x: Object).returns(Integer) }
def alias_success_f(x)
y = x.is_a?(String)
if y
Expand All @@ -206,7 +206,7 @@ def alias_success_f(x)
end

## failure
sig { params(x: T.untyped).returns(Integer) }
sig { params(x: Object).returns(Integer) }
def alias_failure_f(x)
y = x.is_a?(String)
if y
Expand All @@ -228,7 +228,7 @@ def alias_failure_g(x)

## Example nesting_condition
## success
sig { params(x: T.untyped, y: T.untyped).returns(Integer) }
sig { params(x: Object, y: Object).returns(Integer) }
def nesting_condition_success_f(x, y)
if x.is_a?(Integer) ? y.is_a?(String) : false
x + y.length
Expand All @@ -238,7 +238,7 @@ def nesting_condition_success_f(x, y)
end

## failure
sig { params(x: T.any(String, Integer), y: T.untyped).returns(Integer) }
sig { params(x: T.any(String, Integer), y: Object).returns(Integer) }
def nesting_condition_failure_f(x, y)
if x.is_a?(Integer) ? y.is_a?(String) : y.is_a?(String)
x.length # Expected error: length not defined for String | Integer
Expand All @@ -249,7 +249,7 @@ def nesting_condition_failure_f(x, y)

## Example merge_with_union
## success
sig { params(x: T.untyped).returns(T.any(String, Integer)) }
sig { params(x: Object).returns(T.any(String, Integer)) }
def merge_with_union_success_f(x)
if x.is_a?(String)
x += "hello"
Expand All @@ -262,7 +262,7 @@ def merge_with_union_success_f(x)
end

## failure
sig { params(x: T.untyped).returns(T.any(String, Integer)) }
sig { params(x: Object).returns(T.any(String, Integer)) }
def merge_with_union_failure_f(x)
if x.is_a?(String)
x += "hello"
Expand Down