diff --git a/CHANGELOG.md b/CHANGELOG.md
index f4dbfc433..c865d7abc 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -22,6 +22,7 @@ and this project does not currently adhere to a particular versioning scheme.
### Added
+- Add type system for Bend. ([#615][gh-615], [#679][gh-679], see [Type Checking](docs/type-checking.md))
- Add import system. ([#544][gh-544])
- Add multi line comment `#{ ... #}` syntax. ([#595][gh-595])
- Add error message when input file is not found. ([#513][gh-513])
diff --git a/cspell.json b/cspell.json
index 4aa80d973..0ade9d2e0 100644
--- a/cspell.json
+++ b/cspell.json
@@ -34,6 +34,7 @@
"foldl",
"hasher",
"hexdigit",
+ "Hindley",
"hvm's",
"indexmap",
"inet",
@@ -57,6 +58,7 @@
"lnil",
"lpthread",
"mant",
+ "Milner",
"miscompilation",
"mult",
"namegen",
@@ -109,6 +111,7 @@
"succ",
"supercombinator",
"supercombinators",
+ "Tarjan's",
"tlsv",
"TSPL",
"tunr",
diff --git a/docs/syntax.md b/docs/syntax.md
index 389a422c0..25d5d03c8 100644
--- a/docs/syntax.md
+++ b/docs/syntax.md
@@ -10,6 +10,10 @@ Click [here](#import-syntax) to see the import syntax.
Click [here](#comments) to see the syntax for commenting code.
+Click [here](#imp-type-syntax) to see the imperative type syntax.
+
+Click [here](#fun-type-syntax) to see the functional type syntax.
+
Both syntaxes can be mixed in the same file like the example below:
```python
@@ -44,12 +48,15 @@ main =
Defines a top level function.
```python
-def add(x, y):
+def add(x: u24, y: u24) -> u24:
result = x + y
return result
+def unchecked two() -> u24:
+ return 2
+
def main:
- return add(40, 2)
+ return add(40, two)
```
A function definition is composed by a name, a sequence of parameters and a body.
@@ -59,6 +66,10 @@ A top-level name can be anything matching the regex `[A-Za-z0-9_.-/]+`, except i
The last statement of each function must either be a `return` or a selection statement (`if`, `switch`, `match`, `fold`)
where all branches `return`.
+Each parameter of the function can receive a type annotation with `param_name: type` and the return value of the function can also be annotated with `def fn_name(args) -> return_type:`.
+
+We can force the type-checker to run or not on a specific function by adding `checked` or `unchecked` between `def` and the function name.
+
### Type
Defines an algebraic data type.
@@ -68,14 +79,16 @@ type Option:
Some { value }
None
-type Tree:
- Node { value, ~left, ~right }
+type Tree(T):
+ Node { value: T, ~left: Tree(T), ~right: Tree(T) }
Leaf
```
Type names must be unique, and should have at least one constructor.
-Each constructor is defined by a name followed by its fields.
+For a generic or polymorphic type, all type variables used in the constructors must be declared first in the type definition with `type Name(type_var1, ...):`
+
+Each constructor is defined by a name followed by its fields. The fields can be annotated with types that will be checked when creating values of that type.
The `~` notation indicates a recursive field. To use `fold` statements with a type its recursive fields must be correctly marked with `~`.
@@ -89,9 +102,9 @@ Read [defining data types](./defining-data-types.md) to know more.
Defines a type with a single constructor (like a struct, a record or a class).
```python
-object Pair { fst, snd }
+object Pair(A, B) { fst: A, snd: B }
-object Function { name, args, body }
+object Function(T) { name: String, args, body: T }
object Vec { len, data }
```
@@ -1256,6 +1269,11 @@ hvm link_ports:
(a (b *))
& (c a) ~ (d e)
& (e b) ~ (d c)
+
+# Casts a `u24` to itself.
+# We can give type annotations to HVM definitions.
+hvm u24_to_u24 -> (u24 -> u24):
+ ($([u24] ret) ret)
```
It's also possible to define functions using HVM syntax. This can be
@@ -1338,3 +1356,248 @@ Multi-line commenting should also be used to document code.
def second(x, y):
return y
```
+
+
+
+# Imp Type Syntax
+
+## Variable
+
+Any name represents a type variable.
+
+Used in generic or polymorphic type definitions.
+
+```python
+# T is a type variable
+type Option(T):
+ Some { value: T }
+ None
+
+# A is a type variable
+def id(x: A) -> A:
+ return x
+```
+
+## Constructor
+
+`Ctr(...)` represents a constructor type.
+
+Used for defining custom data types or algebraic data types.
+Can contain other types as parameters.
+
+```python
+def head(list: List(T)) -> Option(T)
+ match list:
+ case List/Nil:
+ return Option/None
+ case List/Cons:
+ return Option/Some(list.head)
+```
+
+## Any
+
+`Any` represents the untyped type.
+
+It accepts values of alls type and will forcefully cast any type to `Any`.
+
+Can be used for values that can't be statically typed, either because
+they are unknown (like in raw IO calls), because they contain untypable
+expressions (like unscoped variables), or because the expression cannot
+be typed with the current type system (like the self application `lambda x: x(x)`).
+
+```python
+def main -> Any:
+ return 24
+```
+
+## None
+
+`None` represents the eraser `*` or absence of a value.
+
+Often used to indicate that a function doesn't return anything.
+
+```python
+def none -> None:
+ return *
+```
+
+## Hole
+
+`_` represents a hole type.
+
+This will let the type checker infer the most general type for an argument or return value.
+
+```python
+def increment(x: _) -> _:
+ return x + 1
+```
+
+## u24
+
+`u24` represents an unsigned 24-bit integer.
+
+```python
+def zero -> u24:
+ return 0
+```
+
+## i24
+
+`i24` represents a signed 24-bit integer.
+
+```python
+def random_integer -> i24:
+ return -42
+```
+
+## f24
+
+`f24` represents a 24-bit floating-point number.
+
+```python
+def PI -> f24:
+ return 3.14
+```
+
+## Tuple
+
+`(_, _, ...)` represents a tuple type.
+
+Can contain two or more types separated by commas.
+
+```python
+def make_tuple(fst: A, snd: B) -> (A, B):
+ return (fst, snd)
+```
+
+## Function
+
+`a -> b` represents a function type.
+
+`a` is the input type, and `b` is the output type.
+
+```python
+def apply(f: A -> B, arg: A) -> B:
+ return f(arg)
+```
+
+
+
+# Fun Type Syntax
+
+## Variable
+
+Any name represents a type variable.
+
+Used in generic or polymorphic type definitions.
+
+```python
+# T is a type variable
+type (Option T)
+ = (Some T)
+ | None
+
+# A is a type variable
+id : A -> A
+id x = x
+```
+
+## Constructor
+
+`(Ctr ...)` represents a constructor type.
+
+Used for defining custom data types or algebraic data types.
+Can contain other types as parameters.
+
+```python
+head : (List T) -> (Option T)
+head [] = Option/None
+head (List/Cons head _) = (Option/Some head)
+```
+
+## Any
+
+`Any` represents the untyped type.
+
+It accepts values of alls type and will forcefully cast any type to `Any`.
+
+Can be used for values that can't be statically typed, either because
+they are unknown (like in raw IO calls), because they contain untypable
+expressions (like unscoped variables), or because the expression cannot
+be typed with the current type system (like the self application `λx (x x)`).
+
+```python
+main : Any
+main = @x x
+```
+
+## None
+
+`None` represents the eraser `*` or absence of a value.
+
+Often used to indicate that a function doesn't return anything.
+
+```python
+none : None
+none = *
+```
+
+## Hole
+
+`_` represents a hole type.
+
+This will let the type checker infer the most general type for an argument or return value.
+
+```python
+increment : _ -> _
+increment x = (+ x 1)
+```
+
+## u24
+
+`u24` represents an unsigned 24-bit integer.
+
+```python
+zero : u24
+zero = 0
+```
+
+## i24
+
+`i24` represents a signed 24-bit integer.
+
+```python
+random_integer : i24
+random_integer = -24
+```
+
+## f24
+
+`f24` represents a 24-bit floating-point number.
+
+```python
+PI : f24
+PI = 3.14
+```
+
+## Tuple
+
+`(_, _, ...)` represents a tuple type.
+
+Can contain two or more types separated by commas.
+
+```python
+make_tuple : A -> B -> (A, B)
+make_tuple fst snd = (fst, snd)
+```
+
+## Function
+
+`a -> b` represents a function type.
+
+`a` is the input type, and `b` is the output type.
+
+```python
+apply : (A -> B) -> A -> B
+apply f arg = (f arg)
+```
diff --git a/docs/type-checking.md b/docs/type-checking.md
new file mode 100644
index 000000000..37ed41e3a
--- /dev/null
+++ b/docs/type-checking.md
@@ -0,0 +1,138 @@
+# Type Checking
+
+Bend has a type checker with optional typing support based on a Hindley Milner type system.
+
+Programs can be optionally typed using the respective imp or fun type syntax. Type checking is
+enabled by default, but can be toggled with the `-Otype-check` and `-Ono-type-check` options.
+
+Every function can be annotated with a type for its arguments and return value.
+The type checker will infer the type of the function and then compare if it's compatible with the annotated type.
+
+```python
+def add(x: u24, y: u24) -> u24:
+ return x + y
+
+# Arguments or return value without annotation are considered `Any`.
+# They will be accepted by any function, regardless of being correct or not.
+def push(list: List(T), value) -> List(T):
+ match list:
+ case List/Nil:
+ return List/Cons(value, List/Nil)
+ case List/Cons:
+ return List/Cons(list.head, push(list.tail, value))
+
+# Error, List(T) must only receive values of type `T`.
+def append_num(list: List(T), num: u24) -> List(T):
+ return List/Cons(num, list)
+
+# Error, Tree(T) can only store one type of value.
+def my_tree() -> _:
+ return ![!1, !"a"]
+
+# Error, can't add a `u24` and a `f24`.
+# Bend doesn't have implicit type conversions.
+def add_float(x: u24, y: f24) -> f24:
+ return x + y
+```
+
+Bend comes with the following builtin types:
+
+* `u24`: Unsigned 24-bit integer.
+* `i24`: Signed 24-bit integer.
+* `f24`: Floating point number.
+* `(T1, ..., Tn)`: Tuple with `n` elements of types `T1` to `Tn`.
+* `Any`: Untyped value.
+* `None`: Eraser `*`.
+* `_`: A type that will be inferred by the type checker.
+
+The prelude library also defines some basic types that are used in Bend programs:
+
+* `String`: Text represented as a sequence of Unicode characters.
+* `List(T)`: A list of values of type `T`.
+* `Tree(T)`: A binary tree with values of type `T` at the leaves.
+* `Map(T)`: A map from keys of type `u24` to values of type `T`.
+* `IO(T)`: A monadic IO type that can be used to perform IO operations.
+* `Result(O, E)`: Represents the result of an operation that can either succeed with an `O` or fail with an `E`.
+
+
+Additionally, you can define your own algebraic data types.
+In this case, all the type variables that occur in the constructors must be previously defined.
+
+```python
+type Option(T):
+ Some { value: T }
+ None
+```
+
+All the constructors will be declared with the same type `TypeName(var2, var2, ...)`.
+
+### Enabling and disabling type checking
+
+In some cases we know that dynamically our program will not do something wrong despite not being able to give it the proper type.
+
+We can disable type checking for a specific function by either removing the type annotations or by giving it the `unchecked` keyword:
+
+```python
+# Error, type-checked functions can't contain an unscoped variable.
+def channel(x: u24) -> (u24 -> u24, u24):
+ return (lambda $a: x, $a)
+
+# We can remove the annotations. It won't be type-checked,
+# but its type will be `Any -> Any`.
+def channel(x):
+ return (lambda $a: x, $a)
+
+# Instead, we can use the `unchecked` keyword.
+# The annotated type will be considered the truth, regardless of being correct or not.
+def unchecked channel(x: u24) -> (u24 -> u24, u24):
+ return (lambda $a: x, $a)
+```
+
+The opposite is also possible, we can enable type checking for an unannotated function by using the `checked` keyword before the name of the function in its declaration:
+
+```python
+# Despite the inferred type being `List(T) -> List(T)`, the type checker will consider it as `Any -> Any` because it's not annotated.
+def checked tail(list):
+ match list:
+ case List/Nil:
+ return List/Nil
+ case List/Cons:
+ return list.tail
+
+# Error, can't infer the type of this function, despite having type `Any`.
+# Not typeable by a Hindley-Milner type system.
+checked (scott_concat a b) = (a
+ λh λt λcons λnil (cons h (scott_concat t b))
+ b
+)
+```
+
+We can also disable type checking for the entire program by using the `-Ono-type-check` option.
+
+Native HVM definitions are always unchecked.
+
+```python
+# This function will be given the type `a -> a`.
+hvm native_id -> (a -> a):
+ (x x)
+```
+
+### Limitations
+
+Currently, the following are not supported by the type checker:
+
+- Superpositions (`{a, b}`, the tuple type with duplication semantics, see [Dups and sups](https://github.com/HigherOrderCO/Bend/blob/main/docs/dups-and-sups.md)).
+- Unscoped variables and variable binds (`$a`, `let $a = ...`, see [Scopeless lambdas](https://github.com/HigherOrderCO/Bend/blob/main/docs/using-scopeless-lambdas.md)).
+- Expressions not typeable by a Hindley-Milner type system (e.g. self application `λx: x(x)`).
+
+Additionally, the builtin types `Number` and `Integer` can't be used directly in type annotations. They are used internally by the type checker to handle numeric expressions.
+
+```python
+# The inferred type will be `Number(a) -> Number(a) -> Number(a)`.
+def add(x: _, y: _) -> _:
+ return x + y
+
+# The inferred type will be `Integer(a) -> Integer(a) -> Integer(a)`.
+def shift(x: _, n: _) -> _:
+ return x << n
+```
diff --git a/examples/bubble_sort.bend b/examples/bubble_sort.bend
index 4a0cf6f36..d3c05ade2 100644
--- a/examples/bubble_sort.bend
+++ b/examples/bubble_sort.bend
@@ -1,28 +1,26 @@
# Sorts a list
-def sort(xs):
+def sort(xs: List(u24)) -> List(u24):
match xs:
case List/Nil:
return List/Nil
case List/Cons:
return insert(xs.head, sort(xs.tail))
-# Insert : U60 -> List -> List
-def insert(v, xs):
+def insert(v: u24, xs: List(u24)) -> List(u24):
match xs:
case List/Nil:
return List/Cons(v, List/Nil)
case List/Cons:
return swap_gt(v, xs.head, xs.tail)
-# SwapGT : U60 -> U60 -> U60 -> List -> List
-def swap_gt(v, x, xs):
+def swap_gt(v: u24, x: u24, xs: List(u24)) -> List(u24):
if x > v:
return List/Cons(v, List/Cons(x, xs))
else:
return List/Cons(x, insert(v, xs))
# Generates a list of 'n' random u24 numbers using xorshift
-def rnd(n):
+def rnd(n: u24) -> List(u24):
bend n, state=1:
when n != 0:
state = state ^ (state << 13)
@@ -33,13 +31,13 @@ def rnd(n):
return List/Nil
# Sums a list of u24 numbers
-def sum(xs):
+def sum(xs: List(u24)) -> u24:
fold xs:
case List/Nil:
return 0
case List/Cons:
return xs.head + xs.tail
-def main:
+def main() -> u24:
n = 100
return sum(sort(rnd(n)))
diff --git a/examples/callcc.bend b/examples/callcc.bend
index 57c484316..c21026062 100644
--- a/examples/callcc.bend
+++ b/examples/callcc.bend
@@ -1,16 +1,18 @@
# This program is an example that shows how scopeless lambdas can be used.
-Seq a b = a
+Seq (a: A) (b: B) : A = a
# Create a program capable of using `callcc`
-CC.lang = λprogram
+unchecked CC.lang : ((((a -> b) -> b) -> c) -> c) -> d =
+λprogram
let callcc = λcallback (λ$garbage($hole) (callback λ$hole(0)));
let result = (program callcc);
let garbage = $garbage; # Discard `$garbage`, which is the value returned by `callback`
(Seq result garbage)
-main = (CC.lang λcallcc
+main: u24 = (CC.lang λcallcc
# This code calls `callcc`, then calls `k` to fill the hole with `42`.
# This means that the call to callcc returns `42`, and the program returns `52`
(+ 10 (callcc λk(+ (k 42) 1729)))
)
+
\ No newline at end of file
diff --git a/examples/example_fun.bend b/examples/example_fun.bend
index 3357091a0..8d701be0c 100644
--- a/examples/example_fun.bend
+++ b/examples/example_fun.bend
@@ -1,23 +1,38 @@
# Example of some things you can do with the 'fun' syntax
-# Write definitions like this
+# Define functions like this:
+# By default they accept and return any type
(Def1) = ((λa a) (λb b))
-# You can call a definition by just referencing its name
-# It will be substituted in place of the reference
+# You can call a definition by just referencing its name.
+# It will be substituted in place of the reference.
(Def2) = ((λa a) Def1)
-# Definitions and variables can have names in upper and lower case and contain numbers
-# Names defined in a more inner position shadow names in an outer position
+# Definitions and variables can have names in upper and lower case and
+# contain numbers, '.', '-', '_' and '/'.
+# Names defined in a more inner position shadow names in an outer position.
(def3) = ((λDef1 Def1) (λx λx x))
-# The language is affine, but if you use a variable more than once the compiler inserts duplications for you
-# Of course you can always do them manually
-(def4) = λz let {z1 z2} = z; (z1 ((λx (x x x x x)) z2))
+# You can annotate a function with the expected types and Bend will check them.
+# The parentheses on the left side of the definition are optional.
+const (a: A) (b: B) : A = a
-# You can use machine numbers and some native numeric operations
-# Numeric operations can only reduce numbers, doing (+ (λx x) 1) will not do anything
-(nums) = λx1 λx2 (* (+ x1 1) (/ (- x2 2) 1))
+# There are three types of native numbers available: u24, i24 and f24.
+# u24: Unsigned 24-bit integers
+# i24: Signed 24-bit integers
+# f24: Floating point numbers with 24-bit precision
+(unsigneds (x1: u24) (x2: u24)) : u24 = (* (+ x1 1) (/ (- x2 2) 1))
+
+# '+' or '-' are mandatory for i24.
+(signeds (x1: i24) (x2: i24)) : i24 = (* (+ x1 +1) (/ (- x2 -2) +1))
+
+# The '.' is mandatory for f24.
+(floats (x1: f24) (x2: f24)) : f24 = (* (+ x1 1.0) (/ (- x2 -2.0) +1.0))
+
+# Numeric operations are only meaningful on native numbers.
+# You can force the compiler to do it anyway by using untyped values.
+id = λx x # 'id' wasn't given a type so it's inferred as 'Any'.
+bad_nums : Any = (+ id 1)
# You can use numbers on the native match expression
# The `+` arm binds the `scrutinee`-1 variable to the value of the number -1
@@ -34,7 +49,7 @@ type Bool = True | False
# You can have pattern matching on definitions
# Use `*` to ignore a pattern
(Option.unwrap_or (Option/Some val) *) = val
-(Option.unwrap_or Option/None or) = or
+(Option.unwrap_or Option/None or) = or
(Bool.or Bool/True *) = Bool/True
(Bool.or * Bool/True) = Bool/True
@@ -45,17 +60,16 @@ type Bool = True | False
match bool {
Bool/True: Bool/False
Bool/False: Bool/True
- }
+ }
# Data types can store values
-type Boxed = (Box val)
+type Boxed T = (Box (val: T))
-# Types with only one constructor can be destructured using `let` or a single matching definition
+# Types with only one constructor can be destructured using `open`,
+# a single matching definition or a 'match'.
(Box.map (Boxed/Box val) f) = (Boxed/Box (f val))
-(Box.unbox) = λbox match box {
- Boxed/Box: box.val
-}
+(Box.unbox (box: (Boxed T))): T = open Boxed box; box.val
# Use tuples to store two values together without needing to create a new data type
(Tuple.new fst snd) =
@@ -69,6 +83,68 @@ type Boxed = (Box val)
let (fst, snd) = pair
snd
+# You can give type annotations to type definitions as well.
+# The recursive fields should be annotated with a '~'.
+type ListList T =
+ (Cons (head: (List T)) ~(tail: (ListList T))) |
+ Nil
+
+# Bend functions usually center around recursion
+sum (List/Nil) = 0
+sum (List/Cons x xs) = (+ x (sum xs))
+
+sum_list (ListList/Nil) = List/Nil
+sum_list (ListList/Cons x xs) = (List/Cons (sum x) (sum_list xs))
+
+# To create local recursive functions that consume a recursive type, you can use 'fold'.
+sum_list2 ll = fold ll {
+ # The fold is implicitly called for fields marked with '~' in their definition.
+ # In this case, 'll.tail' is replaced with a recursive call to the fold.
+ ListList/Cons: (List/Cons (sum ll.head) ll.tail)
+ ListList/Nil: List/Nil
+}
+
+# To do the opposite and create a recursive structure, you can use 'bend'.
+# 'bend' can be seen as a tree-like generalization of a while loop.
+new_list = bend x = 0 {
+ when (< x 10):
+ # 'fork' calls the bend recursively with the provided values.
+ (List/Cons x (fork (+ x 1)))
+ else:
+ List/Nil
+}
+
+# To make programs that are more parallelizable, you generally want to
+# avoid lists and use tree-like structures with multiple recursion instead.
+sum_nums from to =
+ if (< from to) {
+ (+
+ (sum_nums from (/ 2 (+ from to)))
+ (sum_nums (+ 1 (/ 2 (+ from to))) to))
+ } else {
+ from
+ }
+
+# Internally, each variable is only used once. If you use a variable
+# is used more than once, the compiler will insert duplications for you.
+#
+# You can also write them manually with 'let {a b} = ...', but then
+# your function needs to be unchecked, either by not annotating it
+# with types or by marking it as unchecked.
+unchecked (def4) = λz let {z1 z2} = z; (z1 ((λx (x x x x x)) z2))
+
+# Duplicating a term that duplicates a variable is not allowed and will break the program.
+map f (List/Cons x xs) = (List/Cons (f x) (map f xs)) # 'f' is duplicated here
+map f (List/Nil) = List/Nil
+
+# 'map' duplicated the lambda which duplicates 'a'.
+# Although this is well defined, it does not produce a sound lambda-calculus result.
+VeryBad (a: u24) (xs: (List u24)) : (List u24) =
+(map
+ λ x (+ (* a x) a) # 'a' is duplicated here
+ [1, 2, 3, 4, 5])
+
+
# All files must have a main definition to run.
# You can execute a program in Bend with "bend run "
# Other options are "check" to just see if the file is well formed
@@ -83,4 +159,4 @@ type Boxed = (Box val)
let map = (Box.map box Option.unwrap_or)
let unboxed = ((Box.unbox map) snd)
- (nums 3 unboxed)
+ (unsigneds 3 unboxed)
diff --git a/examples/fib.bend b/examples/fib.bend
index 070c42090..6e37c19be 100644
--- a/examples/fib.bend
+++ b/examples/fib.bend
@@ -3,7 +3,7 @@
# Calculates fibonacci numbers recursively.
# Although branching recursion is usually a good idea to parallelize,
# it makes this code run in exponential time.
-def fib_recursive(n):
+def fib_recursive(n: u24) -> u24:
switch n:
case 0:
return 0
@@ -14,14 +14,14 @@ def fib_recursive(n):
# Calculates fibonacci numbers iteratively (tail-recursively).
# This function is inherently sequential, but runs in linear time.
-def fib_iterative(n):
+def fib_iterative(n: u24) -> u24:
bend a=0, b=1, n:
when n != 0:
return fork(b, a + b, n - 1)
else:
return a
-def main():
+def main() -> u24:
# With the iterative version, we can calculate large fibonacci numbers
# While with the recursive version, we will quickly run out of memory.
# Note that for numbers larger than 36 the result will overflow the space of the 24-bit integer.
diff --git a/examples/fusing_not.bend b/examples/fusing_not.bend
index b6fd4909b..50b535021 100644
--- a/examples/fusing_not.bend
+++ b/examples/fusing_not.bend
@@ -1,16 +1,19 @@
# Example of a boolean 'not' function that fuses inifinitely through composition..
-true = λt λf t
-false = λt λf f
+true : a -> b -> a = λt λf t
+false : a -> b -> b = λt λf f
-not = λboolean (boolean false true)
-fusing_not = λboolean λt λf (boolean f t)
+not : ((a -> b -> b) -> (c -> d -> c) -> e) -> e =
+ λboolean (boolean false true)
+
+fusing_not : (b -> a -> c) -> a -> b -> c =
+ λboolean λt λf (boolean f t)
# Creates a Church numeral out of a native number
-to_church n = switch n {
+to_church (n: u24) : (a -> a) -> a -> a = switch n {
0: λf λx x
_: λf λx (f (to_church n-1 f x))
}
-main =
+main: _ =
# Self-composes `not` 2^23-1 times and prints the result.
- ((to_church 0x7FFFFF) fusing_not) # try replacing 'fusing_not' by 'not'. Will it still work?
+ ((to_church 0x7FFFF) fusing_not) # try replacing 'fusing_not' by 'not'. Will it still work?
diff --git a/examples/gen_tree.bend b/examples/gen_tree.bend
index f433a5b97..ea2e72ad5 100644
--- a/examples/gen_tree.bend
+++ b/examples/gen_tree.bend
@@ -1,16 +1,16 @@
# Generates a tree with numbers in the nodes using 'bend'
-type MyTree:
- Node { val, ~left, ~right }
+type MyTree(t):
+ Node { val: t, ~left: MyTree(t), ~right: MyTree(t) }
Leaf
-def tree_gen(n, x):
+def tree_gen(n: u24, x: u24) -> MyTree(u24):
bend n, x:
when n != 0:
return MyTree/Node(x, fork(n - 1, x*2+1), fork(n - 1, x*2+2))
else:
return MyTree/Leaf
-def main:
+def main -> MyTree(u24):
depth = 4
first_val = 1
return tree_gen(depth, first_val)
diff --git a/examples/hello_world.bend b/examples/hello_world.bend
index 81ad13e50..60f8d13a5 100644
--- a/examples/hello_world.bend
+++ b/examples/hello_world.bend
@@ -1,4 +1,4 @@
-def main():
+def main() -> IO(u24):
with IO:
* <- IO/print("Hello, world!\n")
return wrap(0)
\ No newline at end of file
diff --git a/examples/insertion_sort.bend b/examples/insertion_sort.bend
index 1119eeca8..667f52178 100644
--- a/examples/insertion_sort.bend
+++ b/examples/insertion_sort.bend
@@ -1,4 +1,4 @@
-def insertion_sort(xs):
+def insertion_sort(xs: List(u24)) -> List(u24):
match xs:
case List/Nil:
return List/Nil
@@ -6,32 +6,32 @@ def insertion_sort(xs):
return insertion_sort.insert(xs.head, insertion_sort(xs.tail))
# Inserts a value into a partially sorted list
-def insertion_sort.insert(v, xs):
+def insertion_sort.insert(v: u24, xs: List(u24)) -> List(u24):
match xs:
case List/Nil:
return List/Cons(v, List/Nil)
case List/Cons:
return insert_aux(v > xs.head, v, xs.head, xs.tail)
-def insert_aux(n, v, x, xs):
+def insert_aux(n: u24, v: u24, x: u24, xs: List(u24)) -> List(u24):
if n == 0:
return List/Cons(v, List/Cons(x, xs))
else:
return List/Cons(x, insertion_sort.insert(v, xs))
# Generates a list of random numbers
-def rnd(n):
+def rnd(n: u24) -> List(u24):
if n == 0:
return List/Nil
else:
return List/Cons(random(10000 - n), rnd(n - 1))
# Generates a pseudo-random number (not very good)
-def random(n):
+def random(n: u24) -> u24:
if n == 0:
return 0
else:
return (random(n - 1) * 16 + 101387) % 429453
-def main():
+def main() -> List(u24):
return insertion_sort(rnd(10))
diff --git a/examples/list.bend b/examples/list.bend
index c3c0c487f..7ce66da29 100644
--- a/examples/list.bend
+++ b/examples/list.bend
@@ -12,173 +12,159 @@
###########################################
# List clear:
-# List l -> list l
# clears all elements from list l. This is equivalent to initializing an empty list.
-clear = @l []
+clear : (List t) -> (List t) = @l []
# List concat:
-# List l -> List l
# combines two lists (l1, l2) from left to right.
-concat = @l1 @l2
+concat : (List t) -> (List t) -> (List t) =
+ @l1 @l2
match l1 {
List/Cons: (List/Cons l1.head (concat l1.tail l2))
List/Nil: l2
}
# List add_front:
-# List l -> List l
-# adds a non-List element e to the front of list l.
-add_front = @l @e
+# adds an element e to the front of list l.
+add_front : (List t) -> t -> (List t) =
+ @l @e
match l {
List/Cons: (List/Cons e l)
List/Nil: (List/Cons e List/Nil)
}
# List append (add_back):
-# List l -> List l
-# adds a non-list element e to the back of list l.
-append = @l @e
- (concat l (List/Cons e List/Nil))
+# adds an element e to the back of list l.
+append : (List t) -> t -> (List t) =
+ @l @e (concat l (List/Cons e List/Nil))
# list sum:
-# List l -> uint
# returns the sum of all items in the list.
-sum = @l
+sum : (List u24) -> u24 = @l
match l {
List/Cons: (+ l.head (sum l.tail))
List/Nil: 0
}
# List reverse:
-# List l -> List l
# reverses the order of elements in list l.
-reverse.aux = @acc @l
+reverse.aux : (List t) -> (List t) -> (List t) =
+ @acc @l
match l {
List/Nil: acc
List/Cons: (reverse.aux (List/Cons l.head acc) l.tail)
}
-reverse = @l
- (reverse.aux [] l)
+reverse : (List t) -> (List t) =
+ @l (reverse.aux [] l)
# List length:
-# List l -> uint
# returns the number of elements in list l.
-len = @l
+len : (List t) -> u24 =
+ @l
match l {
List/Nil: 0
List/Cons: (+ 1 (len l.tail))
}
# List count:
-# List l -> uint -> uint
-# returns the number of instances of Some s in list l.
-count.aux = @acc @l @s
+# returns the number of instances of some number n in list l.
+count.aux : u24 -> (List u24) -> u24 -> u24 =
+ @acc @l @n
match l {
List/Nil: acc
- List/Cons: use acc = switch (== l.head s) {
- 0: acc;
- _: (+ acc 1);
- }
- (count.aux acc l.tail s)
+ List/Cons:
+ let acc = if (== l.head n) { (+ acc 1) } else { acc }
+ (count.aux acc l.tail n)
}
-count = @l @s
- (count.aux 0 l s)
+count = @l @n
+ (count.aux 0 l n)
# List index:
-# List l -> Some s
# returns the value of a specific list index i, or * if the index doesn't exist.
-index = @l @i
+index : (List t) -> u24 -> (Result t None) =
+ @l @i
match l {
List/Cons:
switch i {
- 0: l.head
+ 0: (Result/Ok l.head)
_: (index l.tail (i-1))
}
- List/Nil: *
+ List/Nil: (Result/Err *)
}
# List head:
-# List l -> Some s
# returns the first item in the list, or [] if the list is empty.
-head = @l
+head : (List t) -> (Result t None) =
+ @l
match l {
- List/Cons: l.head
- List/Nil: []
+ List/Cons: (Result/Ok l.head)
+ List/Nil : (Result/Err *)
}
# List tail:
-# List l -> List
-# returns the list except for the first item in it, or [] if the list is empty.
-def tail(l):
- match l:
- case List/Cons:
- return l.tail
- case List/Nil:
- return []
+# returns the list whithout the first item, or [] if the list is empty.
+tail : (List t) -> (List t) =
+ @l
+ match l {
+ List/Cons: l.tail
+ List/Nil: []
+ }
# List equals:
-# List xs, List ys, function cmp -> 1|0
# Compares the elements in two lists and returns 1 if they're equal, and 0 otherwise.
# The function cmp compares two values and returns 1 if they're equal, and 0 otherwise.
-equals xs ys cmp = match xs {
- List/Cons: match ys {
- List/Cons: if (cmp xs.head ys.head) {
- (equals xs.tail ys.tail cmp)
- } else {
- 0
- }
- List/Nil: 0
- }
- List/Nil: match ys {
- List/Cons: 0
- List/Nil: 1
- }
-}
+equals (xs: (List a)) (ys: (List b)) (cmp: a -> b -> u24) : u24
+equals (List/Cons x xs) (List/Cons y ys) cmp = if (cmp x y) { (equals xs ys cmp) } else { 0 }
+equals (List/Cons x xs) List/Nil cmp = 0
+equals List/Nil (List/Cons y ys) cmp = 0
+equals List/Nil List/Nil cmp = 1
# List pop_front:
-# List l -> List l
# removes and discards the first item of list l.
# The new list is returned, or [] if the list is empty.
-pop_front = @l
+pop_front : (List t) -> (List t) =
+ @l
match l {
List/Cons: l.tail
List/Nil: []
}
# List pop_back:
-# List l -> List l
# removes and discards the the last item of list l.
+pop_back : (List t) -> (List t)
pop_back (List/Nil) = List/Nil
pop_back (List/Cons x List/Nil) = List/Nil
pop_back (List/Cons head tail) = (List/Cons head (pop_back tail))
# List remove:
-# List l -> Some s -> List l
# removes the first occurrence of element e from list l.
-remove = @l @s
+remove : (List u24) -> u24 -> (List u24) =
+ @l @s
match l {
List/Cons:
- switch (== l.head s) {
- 0: (List/Cons l.head (remove l.tail s))
- _: l.tail
+ if (== l.head s) {
+ l.tail
+ } else {
+ (List/Cons l.head (remove l.tail s))
}
List/Nil: List/Nil
}
# List split:
-# list l -> uint i -> (List l, list l)
# splits list l into two lists (l1, l2) at index i.
# the second list takes the element at index i during the split.
-split = @l @i (split.aux [] l i)
+split : (List t) -> u24 -> ((List t), (List t)) =
+ @l @i (split.aux [] l i)
-split.aux = @acc @l @i
+split.aux : (List t) -> (List t) -> u24 -> ((List t), (List t)) =
+ @acc @l @i
match l {
List/Cons:
switch i {
0: (acc, l)
_: (split.aux (append acc l.head) l.tail i-1)
}
- List/Nil: *
+ List/Nil: (acc, [])
}
diff --git a/examples/parallel_and.bend b/examples/parallel_and.bend
index 07fd6830d..bd41552da 100644
--- a/examples/parallel_and.bend
+++ b/examples/parallel_and.bend
@@ -3,26 +3,27 @@ type Bool:
True
False
-def and(a, b):
+def and(a: Bool, b: Bool) -> Bool:
match a:
case Bool/True:
return b
case Bool/False:
return Bool/False
-def all(tree):
+# Trees of tuples are not typeable
+def all(tree: Tree(Bool)) -> Bool:
fold tree:
case Tree/Node:
return and(tree.left, tree.right)
case Tree/Leaf:
return tree.value
-def gen(n):
+def gen(n: u24) -> Tree(Bool):
switch n:
case 0:
return Tree/Leaf(Bool/True)
case _:
return Tree/Node { left: gen(n-1), right: gen(n-1) }
-def main():
+def main() -> Bool:
return all(gen(8))
diff --git a/examples/parallel_sum.bend b/examples/parallel_sum.bend
index 321d24fc9..b6fb578f1 100644
--- a/examples/parallel_sum.bend
+++ b/examples/parallel_sum.bend
@@ -2,12 +2,12 @@
# Creates a tree with numbers and then sums all values in parallel
# a binary tree
-type MyTree:
- Node { val, ~left, ~right }
+type MyTree(t):
+ Node { val: t, ~left: MyTree(t), ~right: MyTree(t) }
Leaf
# sums all values in a tree
-def sum(tree):
+def sum(tree: MyTree(u24)) -> u24:
fold tree:
case MyTree/Node:
return tree.val + tree.left + tree.right
@@ -15,7 +15,7 @@ def sum(tree):
return 0
# generates a binary tree of given depth
-def gen(depth):
+def gen(depth: u24) -> MyTree(u24):
bend height=0, val = 1:
when height < depth:
tree = MyTree/Node { val: val, left: fork(height+1, 2*val), right: fork(height+1, 2*val+1) }
@@ -24,5 +24,5 @@ def gen(depth):
return tree
# returns the sum of [1 .. 2^16), truncated to 24 bits
-def main:
+def main() -> u24:
return sum(gen(16))
\ No newline at end of file
diff --git a/examples/queue.bend b/examples/queue.bend
index 346651174..b43281b5b 100644
--- a/examples/queue.bend
+++ b/examples/queue.bend
@@ -2,16 +2,16 @@
# Implements constant-time queues with just lambdas
# Qnew : Queue a
-Qnew = λx x
+Qnew: _ = λx x
# Qadd : a -> Queue a -> Queue a
-Qadd = λx λq λk (q λc (c x k))
+Qadd: _ = λx λq λk (q λc (c x k))
# Qrem : Queue a -> Pair a (Queue a)
Qrem = λq (q $k λx λxs λp(p x λ$k xs))
# Output: [1, 2, 3]
-main =
+main: (List u24) =
let q = Qnew
let q = (Qadd 1 q)
let q = (Qadd 2 q)
diff --git a/examples/quick_sort.bend b/examples/quick_sort.bend
index 84f0296f2..9fc39d92e 100644
--- a/examples/quick_sort.bend
+++ b/examples/quick_sort.bend
@@ -1,22 +1,26 @@
-type MyTree = Leaf | (Node lft val rgt)
+type MyTree t = Leaf | (Node ~(lft: (MyTree t)) (val: t) ~(rgt: (MyTree t)))
# Parallel QuickSort
-(Sort List/Nil) = MyTree/Leaf
+(Sort) : (List u24) -> (MyTree u24)
+(Sort List/Nil) = MyTree/Leaf
(Sort (List/Cons head tail)) =
- ((Part head tail) λmin λmax
- let lft = (Sort min)
- let rgt = (Sort max)
- (MyTree/Node lft head rgt))
+ let (min, max) = (Part head tail)
+ let lft = (Sort min)
+ let rgt = (Sort max)
+ (MyTree/Node lft head rgt)
- # Partitions a list in two halves, less-than-p and greater-than-p
- (Part p List/Nil) = λt (t List/Nil List/Nil)
- (Part p (List/Cons head tail)) = (Push (> head p) head (Part p tail))
+# Partitions a list in two halves, less-than-p and greater-than-p
+(Part) : u24 -> (List u24) -> ((List u24), (List u24))
+(Part p List/Nil) = (List/Nil, List/Nil)
+(Part p (List/Cons head tail)) = (Push (> head p) head (Part p tail))
- # Pushes a value to the first or second list of a pair
- (Push 0 x pair) = (pair λmin λmax λp (p (List/Cons x min) max))
- (Push _ x pair) = (pair λmin λmax λp (p min (List/Cons x max)))
+# Pushes a value to the first or second list of a pair
+(Push) : u24 -> u24 -> ((List u24), (List u24)) -> ((List u24), (List u24))
+(Push 0 x (min, max)) = ((List/Cons x min), max)
+(Push _ x (min, max)) = (min, (List/Cons x max))
# Generates a random list with xorshift
+(Rnd) : u24 -> (u24) -> (List u24)
(Rnd 0 state) = List/Nil
(Rnd n state) =
let state = (^ state (<< state 13))
@@ -25,11 +29,12 @@ type MyTree = Leaf | (Node lft val rgt)
(List/Cons state (Rnd (- n 1) state))
# Sums all elements in a concatenation tree
+(Sum) : (MyTree u24) -> u24
(Sum MyTree/Leaf) = 0
(Sum (MyTree/Node lft val rgt)) = (+ val (+ (Sum lft) (Sum rgt)))
# Sorts and sums n random numbers
-(Main) =
+(Main) : u24 =
(Sum (Sort (Rnd 0x100 1)))
# Use an argument from cli
diff --git a/examples/radix_sort.bend b/examples/radix_sort.bend
index f92525c2f..8ea735c5f 100644
--- a/examples/radix_sort.bend
+++ b/examples/radix_sort.bend
@@ -1,100 +1,95 @@
-type Map_:
+type MyMap:
Free
Used
- Both {~a, ~b}
+ Both { ~a: MyMap, ~b: MyMap }
-type Arr:
+type Arr(t):
Null
- Leaf {~a}
- Node {~a, ~b}
+ Leaf { a: t }
+ Node { ~a: Arr(t), ~b: Arr(t) }
-def swap(s, a, b):
+def swap(s: u24, a: MyMap, b: MyMap) -> MyMap:
switch s:
case 0:
- return Map_/Both{ a: a, b: b }
+ return MyMap/Both{ a: a, b: b }
case _:
- return Map_/Both{ a: b, b: a }
+ return MyMap/Both{ a: b, b: a }
-# Sort : Arr -> Arr
-def sort(t):
+def sort(t: Arr(u24)) -> Arr(u24):
return to_arr(0, to_map(t))
-# ToMap : Arr -> Map
-def to_map(t):
+def to_map(t: Arr(u24)) -> MyMap:
match t:
case Arr/Null:
- return Map_/Free
+ return MyMap/Free
case Arr/Leaf:
return radix(t.a)
case Arr/Node:
return merge(to_map(t.a), to_map(t.b))
-# ToArr : U60 -> Map -> Arr
-def to_arr(x, m):
+def to_arr(x: u24, m: MyMap) -> Arr(u24):
match m:
- case Map_/Free:
+ case MyMap/Free:
return Arr/Null
- case Map_/Used:
+ case MyMap/Used:
return Arr/Leaf{ a: x }
- case Map_/Both:
+ case MyMap/Both:
return Arr/Node{ a: to_arr(x * 2, m.a), b: to_arr(x * 2 + 1, m.b) }
-# Merge : Map -> Map -> Map
-def merge(a, b):
+def merge(a: MyMap, b: MyMap) -> MyMap:
match a:
- case Map_/Free:
+ case MyMap/Free:
return b
- case Map_/Used:
- return Map_/Used
- case Map_/Both:
+ case MyMap/Used:
+ return MyMap/Used
+ case MyMap/Both:
match b:
- case Map_/Free:
+ case MyMap/Free:
return a
- case Map_/Used:
- return Map_/Used
- case Map_/Both:
- return Map_/Both{ a: merge(a.a, b.a), b: merge(a.b, b.b) }
+ case MyMap/Used:
+ return MyMap/Used
+ case MyMap/Both:
+ return MyMap/Both{ a: merge(a.a, b.a), b: merge(a.b, b.b) }
-# Radix : U60 -> Map
-def radix(n):
- r = Map_/Used
- r = swap(n & 1, r, Map_/Free)
- r = swap(n & 2, r, Map_/Free)
- r = swap(n & 4, r, Map_/Free)
- r = swap(n & 8, r, Map_/Free)
- r = swap(n & 16, r, Map_/Free)
- r = swap(n & 32, r, Map_/Free)
- r = swap(n & 64, r, Map_/Free)
- r = swap(n & 128, r, Map_/Free)
- r = swap(n & 256, r, Map_/Free)
- r = swap(n & 512, r, Map_/Free)
+def radix(n: u24) -> MyMap:
+ r = MyMap/Used
+ r = swap(n & 1, r, MyMap/Free)
+ r = swap(n & 2, r, MyMap/Free)
+ r = swap(n & 4, r, MyMap/Free)
+ r = swap(n & 8, r, MyMap/Free)
+ r = swap(n & 16, r, MyMap/Free)
+ r = swap(n & 32, r, MyMap/Free)
+ r = swap(n & 64, r, MyMap/Free)
+ r = swap(n & 128, r, MyMap/Free)
+ r = swap(n & 256, r, MyMap/Free)
+ r = swap(n & 512, r, MyMap/Free)
return radix2(n, r)
# At the moment, we need to manually break very large functions into smaller ones
# if we want to run this program on the GPU.
# In a future version of Bend, we will be able to do this automatically.
-def radix2(n, r):
- r = swap(n & 1024, r, Map_/Free)
- r = swap(n & 2048, r, Map_/Free)
- r = swap(n & 4096, r, Map_/Free)
- r = swap(n & 8192, r, Map_/Free)
- r = swap(n & 16384, r, Map_/Free)
- r = swap(n & 32768, r, Map_/Free)
- r = swap(n & 65536, r, Map_/Free)
- r = swap(n & 131072, r, Map_/Free)
- r = swap(n & 262144, r, Map_/Free)
- r = swap(n & 524288, r, Map_/Free)
+def radix2(n: u24, r: MyMap) -> MyMap:
+ r = swap(n & 1024, r, MyMap/Free)
+ r = swap(n & 2048, r, MyMap/Free)
+ r = swap(n & 4096, r, MyMap/Free)
+ r = swap(n & 8192, r, MyMap/Free)
+ r = swap(n & 16384, r, MyMap/Free)
+ r = swap(n & 32768, r, MyMap/Free)
+ r = swap(n & 65536, r, MyMap/Free)
+ r = swap(n & 131072, r, MyMap/Free)
+ r = swap(n & 262144, r, MyMap/Free)
+ r = swap(n & 524288, r, MyMap/Free)
return radix3(n, r)
-def radix3(n, r):
- r = swap(n & 1048576, r, Map_/Free)
- r = swap(n & 2097152, r, Map_/Free)
- r = swap(n & 4194304, r, Map_/Free)
- r = swap(n & 8388608, r, Map_/Free)
+def radix3(n: u24, r: MyMap) -> MyMap:
+ r = swap(n & 1048576, r, MyMap/Free)
+ r = swap(n & 2097152, r, MyMap/Free)
+ r = swap(n & 4194304, r, MyMap/Free)
+ r = swap(n & 8388608, r, MyMap/Free)
return r
-def reverse(t):
+def reverse(t: Arr(u24)) -> Arr(u24):
match t:
case Arr/Null:
return Arr/Null
@@ -103,8 +98,7 @@ def reverse(t):
case Arr/Node:
return Arr/Node{ a: reverse(t.b), b: reverse(t.a) }
-# Sum : Arr -> U60
-def sum(t):
+def sum(t: Arr(u24)) -> u24:
match t:
case Arr/Null:
return 0
@@ -113,11 +107,10 @@ def sum(t):
case Arr/Node:
return sum(t.a) + sum(t.b)
-# Gen : U60 -> Arr
-def gen(n):
+def gen(n: u24) -> Arr(u24):
return gen_go(n, 0)
-def gen_go(n, x):
+def gen_go(n: u24, x: u24) -> Arr(u24):
switch n:
case 0:
return Arr/Leaf{ a: x }
@@ -126,4 +119,4 @@ def gen_go(n, x):
b = x * 2 + 1
return Arr/Node{ a: gen_go(n-1, a), b: gen_go(n-1, b) }
-Main = (sum (sort(reverse(gen 4))))
+Main: u24 = (sum (sort(reverse(gen 4))))
diff --git a/src/diagnostics.rs b/src/diagnostics.rs
index c8264ae37..088a81d8d 100644
--- a/src/diagnostics.rs
+++ b/src/diagnostics.rs
@@ -11,7 +11,6 @@ pub const ERR_INDENT_SIZE: usize = 2;
#[derive(Debug, Clone, Default)]
pub struct Diagnostics {
- err_counter: usize,
pub diagnostics: BTreeMap>,
pub config: DiagnosticsConfig,
}
@@ -71,21 +70,18 @@ pub enum WarningType {
impl Diagnostics {
pub fn new(config: DiagnosticsConfig) -> Self {
- Self { err_counter: 0, diagnostics: Default::default(), config }
+ Self { diagnostics: Default::default(), config }
}
pub fn add_parsing_error(&mut self, err: impl std::fmt::Display, source: Source) {
- self.err_counter += 1;
self.add_diagnostic(err, Severity::Error, DiagnosticOrigin::Parsing, source);
}
pub fn add_book_error(&mut self, err: impl std::fmt::Display) {
- self.err_counter += 1;
self.add_diagnostic(err, Severity::Error, DiagnosticOrigin::Book, Default::default());
}
pub fn add_function_error(&mut self, err: impl std::fmt::Display, name: Name, source: Source) {
- self.err_counter += 1;
self.add_diagnostic(
err,
Severity::Error,
@@ -95,7 +91,6 @@ impl Diagnostics {
}
pub fn add_inet_error(&mut self, err: impl std::fmt::Display, def_name: String) {
- self.err_counter += 1;
self.add_diagnostic(err, Severity::Error, DiagnosticOrigin::Inet(def_name), Default::default());
}
@@ -107,9 +102,6 @@ impl Diagnostics {
source: Source,
) {
let severity = self.config.warning_severity(warn_type);
- if severity == Severity::Error {
- self.err_counter += 1;
- }
self.add_diagnostic(
warn,
severity,
@@ -120,9 +112,6 @@ impl Diagnostics {
pub fn add_book_warning(&mut self, warn: impl std::fmt::Display, warn_type: WarningType) {
let severity = self.config.warning_severity(warn_type);
- if severity == Severity::Error {
- self.err_counter += 1;
- }
self.add_diagnostic(warn, severity, DiagnosticOrigin::Book, Default::default());
}
@@ -173,16 +162,11 @@ impl Diagnostics {
self.has_severity(Severity::Error)
}
- /// Resets the internal counter
- pub fn start_pass(&mut self) {
- self.err_counter = 0;
- }
-
/// Checks if any error was emitted since the start of the pass,
/// Returning all the current information as a `Err(Info)`, replacing `&mut self` with an empty one.
/// Otherwise, returns the given arg as an `Ok(T)`.
pub fn fatal(&mut self, t: T) -> Result {
- if self.err_counter == 0 {
+ if !self.has_errors() {
Ok(t)
} else {
Err(std::mem::take(self))
diff --git a/src/fun/builtins.bend b/src/fun/builtins.bend
index cca33de52..542047d26 100644
--- a/src/fun/builtins.bend
+++ b/src/fun/builtins.bend
@@ -1,44 +1,61 @@
-type String = (Nil) | (Cons head ~tail)
+type String:
+ Nil
+ Cons { head: u24, ~tail: String }
-type List = (Nil) | (Cons head ~tail)
+type List(T):
+ Nil
+ Cons { head: T, ~tail: List(T) }
-# List/length(xs: List(T)) -> (u24, List(T))
# Returns the length of a list and the list itself.
-List/length xs = fold xs with len=0, acc=DiffList/new {
- List/Nil: (len, (DiffList/to_list acc))
- List/Cons: (xs.tail (+ len 1) (DiffList/append acc xs.head))
-}
+def List/length(xs: List(T)) -> (u24, List(T)):
+ fold xs with len=0, acc=DiffList/new:
+ case List/Nil:
+ return (len, DiffList/to_list(acc))
+ case List/Cons:
+ return xs.tail(len + 1, DiffList/append(acc, xs.head))
-# List/reverse(xs: List(T)) -> List(T)
# Reverses a list.
-List/reverse xs = fold xs with acc=[] {
- List/Nil: acc
- List/Cons: (xs.tail (List/Cons xs.head acc))
-}
+def List/reverse(xs: List(T)) -> List(T):
+ fold xs with acc=[]:
+ case List/Nil:
+ return acc
+ case List/Cons:
+ return xs.tail(List/Cons(xs.head, acc))
-# List/flatten(xs: List(List(T))) -> List(T)
# Flattens a list of lists.
+List/flatten (xs: (List (List T))) : (List T)
List/flatten (List/Cons x xs) = (List/concat x (List/flatten xs))
List/flatten (List/Nil) = (List/Nil)
-# List/concat(xs: List(T), ys: List(T)) -> List(T)
# Concatenates two lists.
+List/concat(xs: (List T)) (ys: (List T)) : (List T)
List/concat (List/Cons x xs) ys = (List/Cons x (List/concat xs ys))
List/concat (List/Nil) ys = ys
-# List/split_once(xs: List(T), val: T) -> (Result(List(T), List(T)))
-# Splits a list into two lists at the first occurrence of a value.
-List/split_once xs val = (List/split_once.go xs val @x x)
- List/split_once.go List/Nil val acc = (Result/Err (acc List/Nil))
- List/split_once.go (List/Cons x xs) val acc =
- if (== val x) {
- (Result/Ok ((acc List/Nil), xs))
- } else {
- (List/split_once.go xs val @y (acc (List/Cons x y)))
- }
+# Splits a list into two lists at the first value that passes a condition.
+# Returns the original list if the value is not found
+def List/split_once(
+ xs: List(T),
+ cond: T -> u24
+) -> (Result((List(T), List(T)), List(T))):
+ return List/split_once.go(xs, cond, DiffList/new)
+
+def List/split_once.go(
+ xs: List(T),
+ cond: T -> u24,
+ acc: List(T) -> List(T)
+) -> Result((List(T), List(T)), List(T)):
+ match xs:
+ case List/Nil:
+ return Result/Err(DiffList/to_list(acc))
+ case List/Cons:
+ if cond(xs.head):
+ return Result/Ok((DiffList/to_list(acc), xs.tail))
+ else:
+ return List/split_once.go(xs.tail, cond, DiffList/append(acc, xs.head))
-# List/filter(xs: List(T), pred: T -> Bool) -> List(T)
# Filters a list based on a predicate function.
+List/filter (xs: (List T)) (pred: T -> u24) : (List T)
List/filter (List/Nil) _ = List/Nil
List/filter (List/Cons x xs) pred =
if (pred x) {
@@ -47,8 +64,8 @@ List/filter (List/Cons x xs) pred =
(List/filter xs pred)
}
-# String/equals(s1: String, s2: String) -> u24
# Checks if two strings are equal.
+String/equals (s1: String) (s2: String) : u24
String/equals (String/Nil) (String/Nil) = 1
String/equals (String/Cons x xs) (String/Cons y ys) =
if (== x y) {
@@ -58,61 +75,86 @@ String/equals (String/Cons x xs) (String/Cons y ys) =
}
String/equals * * = 0
-# String/split(s: String, delimiter: u24) -> List(String)
# Splits a list into two lists at the first occurrence of a value.
-String/split s delim = (String/split.go s delim (List/Cons String/Nil List/Nil))
- String/split.go (String/Nil) _ acc = (List/reverse acc)
- String/split.go (String/Cons c cs) delim acc =
- if (== c delim) {
- (String/split.go cs delim (List/Cons String/Nil acc))
- } else {
- match acc {
- List/Cons: (String/split.go cs delim (List/Cons (String/Cons c acc.head) acc.tail))
- List/Nil: []
- }
+String/split (s: String) (delimiter: u24) : (List String)
+String/split s delim = (String/split.go s delim [""])
+
+String/split.go (cs: String) (delim: u24) (acc: (List String)) : (List String)
+String/split.go (String/Nil) _ acc = (List/reverse acc)
+String/split.go (String/Cons c cs) delim acc =
+ if (== c delim) {
+ # Start a new split string
+ (String/split.go cs delim (List/Cons String/Nil acc))
+ } else {
+ match acc {
+ # Add the current character to the current split string
+ List/Cons: (String/split.go cs delim (List/Cons (String/Cons c acc.head) acc.tail))
+ # Should be unreachable
+ List/Nil: []
}
+ }
-# DiffList/new() -> (List(T) -> List(T))
# Create a new difference list
-DiffList/new = λx x
+def DiffList/new() -> (List(T) -> List(T)):
+ return lambda x: x
-# DiffList/wrap(head: T) -> (List(T) -> List(T)
# Creates a new difference list with just the given value.
-def DiffList/wrap(head):
+def DiffList/wrap(head: T) -> (List(T) -> List(T)):
return lambda tail: List/Cons(head, tail)
-# DiffList/append(diff: List(T) -> List(T), val: T) -> (List(T) -> List(T))
# Append a value to the end of the difference list
-DiffList/append diff val = λx (diff (List/Cons val x))
+def DiffList/append(diff: List(T) -> List(T), val: T) -> (List(T) -> List(T)):
+ return lambda x: diff(List/Cons(val, x))
-# DiffList/append(left: List(T) -> List(T), right: List(T) -> List(T)) -> (List(T) -> List(T))
# Concatenates two difference lists.
-def DiffList/concat(left, right):
+def DiffList/concat(
+ left: List(T) -> List(T),
+ right: List(T) -> List(T)
+) -> (List(T) -> List(T)):
return lambda x: left(right(x))
-# DiffList/cons(diff: List(T) -> List(T), val: T) -> (List(T) -> List(T))
# Append a value to the beginning of the difference list
-DiffList/cons diff val = λx (List/Cons val (diff x))
+def DiffList/cons(diff: List(T) -> List(T), val: T) -> (List(T) -> List(T)):
+ return lambda x: List/Cons(val, diff(x))
-# DiffList/to_list(diff: List(T) -> List(T)) -> (List(T))
# Convert a difference list to a list
-DiffList/to_list diff = (diff List/Nil)
-
-type Nat = (Succ ~pred) | (Zero)
-
-type Result = (Ok val) | (Err val)
-
-Result/unwrap res = match res {
- Result/Ok: res.val;
- Result/Err: res.val;
-}
-
-type Tree:
- Node { ~left, ~right }
- Leaf { value }
+def DiffList/to_list(diff: List(T) -> List(T)) -> (List(T)):
+ return diff(List/Nil)
+
+type Nat = (Succ ~(pred: Nat)) | (Zero)
+
+type (Result o e) = (Ok (val: o)) | (Err (val: e))
+
+def Result/unwrap(res: Result(T, E)) -> Any:
+ match res:
+ case Result/Ok:
+ return res.val
+ case Result/Err:
+ return res.val
+
+# Returns the second result if the first one is `Ok`.
+# Otherwise, returns the `Err` of the first result.
+def Result/and(fst: Result(A, E), snd: Result(B, E)) -> Result(B, E):
+ match fst:
+ case Result/Ok:
+ return snd
+ case Result/Err:
+ return fst
+
+# Maps the error value of a result.
+def Result/map_err(res: Result(T, E), f: E -> F) -> Result(T, F):
+ match res:
+ case Result/Ok:
+ return Result/Ok(res.val)
+ case Result/Err:
+ return Result/Err(f(res.val))
+
+type Tree(T):
+ Node { ~left: Tree(T), ~right: Tree(T) }
+ Leaf { value: T }
# Returns a List converted from a Tree.
-def Tree/to_list(tree):
+def Tree/to_list(tree: Tree(T)) -> List(T):
fold tree:
case Tree/Leaf:
list = DiffList/wrap(tree.value)
@@ -121,7 +163,7 @@ def Tree/to_list(tree):
return DiffList/to_list(list)
# Reverses a tree swapping right and left leaves.
-def Tree/reverse(tree):
+def Tree/reverse(tree: Tree(T)) -> Tree(T):
fold tree:
case Tree/Leaf:
return !tree.value
@@ -130,13 +172,13 @@ def Tree/reverse(tree):
# MAP Impl
-type Map = (Node value ~left ~right) | (Leaf)
+type Map T = (Node (value: T) ~(left: (Map T)) ~(right: (Map T))) | (Leaf)
-Map/empty = Map/Leaf
+Map/empty : (Map T) = Map/Leaf
-Map/get map key =
+Map/get (map: (Map T)) (key: u24) : (T, (Map T)) =
match map {
- Map/Leaf: (*, map)
+ Map/Leaf: (unreachable, map)
Map/Node:
switch _ = (== 0 key) {
0: switch _ = (% key 2) {
@@ -151,7 +193,7 @@ Map/get map key =
}
}
-Map/set map key value =
+Map/set (map: (Map T)) (key: u24) (value: T) : (Map T) =
match map {
Map/Node:
switch _ = (== 0 key) {
@@ -164,13 +206,14 @@ Map/set map key value =
Map/Leaf:
switch _ = (== 0 key) {
0: switch _ = (% key 2) {
- 0: (Map/Node * (Map/set Map/Leaf (/ key 2) value) Map/Leaf)
- _: (Map/Node * Map/Leaf (Map/set Map/Leaf (/ key 2) value))
+ 0: (Map/Node unreachable (Map/set Map/Leaf (/ key 2) value) Map/Leaf)
+ _: (Map/Node unreachable Map/Leaf (Map/set Map/Leaf (/ key 2) value))
}
_: (Map/Node value Map/Leaf Map/Leaf)
}
}
+Map/map (map: (Map T)) (key: u24) (f: T -> T) : (Map T)
Map/map (Map/Leaf) key f = Map/Leaf
Map/map (Map/Node value left right) key f =
switch _ = (== 0 key) {
@@ -186,266 +229,348 @@ Map/map (Map/Node value left right) key f =
# IO Impl
-type IO:
- Done { magic, expr }
- Call { magic, func, argm, cont }
+type IO(T):
+ Done { magic: (u24, u24), expr: T }
+ Call { magic: (u24, u24), func: String, argm: Any, cont: Result(Any, IOError(Any)) -> IO(T) }
-type IOError:
+type IOError(T):
Type
Name
- Inner { value }
-
-def IO/MAGIC:
+ Inner { value: T }
+
+def IOError/unwrap_inner(err: IOError(T)) -> T:
+ match err:
+ case IOError/Type:
+ return unreachable()
+ case IOError/Name:
+ return unreachable()
+ case IOError/Inner:
+ return err.value
+
+def IO/MAGIC() -> (u24, u24):
return (0xD0CA11, 0xFF1FF1)
-def IO/wrap(x):
+def IO/wrap(x: T) -> IO(T):
return IO/Done(IO/MAGIC, x)
-def IO/bind(a, b):
+def IO/bind(a: IO(A), b: ((Id -> Id) -> A -> IO(B))) -> IO(B):
match a:
case IO/Done:
- b = undefer(b)
- return b(a.expr)
+ return undefer(b, a.expr)
case IO/Call:
- return IO/Call(IO/MAGIC, a.func, a.argm, lambda x: IO/bind(a.cont(x), b))
-
-def call(func, argm):
+ return IO/Call(a.magic, a.func, a.argm, lambda x: IO/bind(a.cont(x), b))
+
+# Calls an IO by its name with the given arguments.
+#
+# The arguments are untyped and not checked for type correctness.
+# If type safety is desired, this function should be wrapped with
+# another that checks the types of the arguments and of the return.
+#
+# Always returns a `Result` where the error is an `IOError`, a type
+# that either contains an internal error of the IO function, like an
+# `errno` in the case of FS functions, or a general Bend IO error,
+# like a type error if the arguments are invalid or a name error if
+# the called IO is not found.
+def IO/call(func: String, argm: Any) -> IO(Result(Any, IOError(Any))):
return IO/Call(IO/MAGIC, func, argm, lambda x: IO/Done(IO/MAGIC, x))
-IO/done_on_err (IO/Call magic func argm cont) = (IO/Call magic func argm @res match res {
- Result/Ok: (cont res.val)
- Result/Err: (IO/Done IO/MAGIC (Result/Err res.val))
-})
-IO/done_on_err done = done
+# Maps the result of an IO.
+def IO/map(io: IO(A), f: A -> B) -> IO(B):
+ with IO:
+ a <- io
+ return wrap(f(a))
+
+# Unwraps the `IOError` of the result of an IO, returning the `Inner` variant.
+#
+# Should only be called if the other `IOError` variants are unreachable.
+def IO/unwrap_inner(io: IO(Result(A, IOError(B)))) -> IO(Result(A, B)):
+ with IO:
+ res <- io
+ match res:
+ case Result/Ok:
+ return wrap(Result/Ok(res.val))
+ case Result/Err:
+ return wrap(Result/Err(IOError/unwrap_inner(res.val)))
## Time and sleep
-# Returns a monotonically increasing nanosecond timestamp as an u48 encoded as a pair of u24s.
-IO/get_time = with IO {
- ask res = (IO/Call IO/MAGIC "GET_TIME" * @x (IO/Done IO/MAGIC x))
- (wrap (Result/unwrap res))
- }
+
+# Returns a monotonically increasing nanosecond timestamp as an u48
+# encoded as a pair of u24s.
+def IO/get_time() -> IO((u24, u24)):
+ with IO:
+ res <- IO/call("GET_TIME", *)
+ return wrap(Result/unwrap(res))
# Sleeps for the given number of nanoseconds, given by an u48 encoded as a pair of u24s.
-IO/nanosleep hi_lo = (IO/Call IO/MAGIC "SLEEP" hi_lo @x (IO/Done IO/MAGIC x))
+def IO/nanosleep(hi_lo: (u24, u24)) -> IO(None):
+ with IO:
+ res <- IO/call("SLEEP", hi_lo)
+ return wrap(Result/unwrap(res))
# Sleeps for a given amount of seconds as a float.
-def IO/sleep(seconds):
+def IO/sleep(seconds: f24) -> IO(None):
nanos = seconds * 1_000_000_000.0
- lo = to_u24(nanos % 0x1_000_000.0)
- hi = to_u24(nanos / 0x1_000_000.0)
- with IO:
- res <- IO/nanosleep((hi, lo))
- return wrap(Result/unwrap(res))
+ lo = f24/to_u24(nanos % 0x1_000_000.0)
+ hi = f24/to_u24(nanos / 0x1_000_000.0)
+ return IO/nanosleep((hi, lo))
## File IO
### File IO primitives
-# IO/FS/open(path: String, mode: u24) -> (IO u24)
-IO/FS/open path mode = (IO/Call IO/MAGIC "OPEN" (path, mode) IO/wrap)
+def IO/FS/open(path: String, mode: String) -> IO(Result(u24, u24)):
+ return IO/unwrap_inner(IO/call("OPEN", (path, mode)))
-# IO/FS/close(file: u24) -> (IO None)
-IO/FS/close file = (IO/Call IO/MAGIC "CLOSE" file IO/wrap)
+def IO/FS/close(file: u24) -> IO(Result(None, u24)):
+ return IO/unwrap_inner(IO/call("CLOSE", file))
-# IO/FS/read(file: u24, num_bytes: u24) -> (IO (List u24))
-IO/FS/read file num_bytes = (IO/Call IO/MAGIC "READ" (file, num_bytes) IO/wrap)
+def IO/FS/read(file: u24, num_bytes: u24) -> IO(Result(List(u24), u24)):
+ return IO/unwrap_inner(IO/call("READ", (file, num_bytes)))
-# IO/FS/write(file: u24, bytes: (List u24)) -> (IO None)
-IO/FS/write file bytes = (IO/Call IO/MAGIC "WRITE" (file, bytes) IO/wrap)
+def IO/FS/write(file: u24, bytes: List(u24)) -> IO(Result(None, u24)):
+ return IO/unwrap_inner(IO/call("WRITE", (file, bytes)))
-# IO/FS/seek(file: u24, offset: i24, mode: u24) -> (IO None)
-IO/FS/seek file offset mode = (IO/Call IO/MAGIC "SEEK" (file, (offset, mode)) IO/wrap)
+def IO/FS/seek(file: u24, offset: i24, mode: i24) -> IO(Result(None, u24)):
+ return IO/unwrap_inner(IO/call("SEEK", (file, (offset, mode))))
-# IO/FS/flush(file: u24) -> (IO None)
-IO/FS/flush file = (IO/Call IO/MAGIC "FLUSH" file IO/wrap)
+def IO/FS/flush(file: u24) -> IO(Result(None, u24)):
+ return IO/unwrap_inner(IO/call("FLUSH", file))
### Always available files
-IO/FS/STDIN = 0
-IO/FS/STDOUT = 1
-IO/FS/STDERR = 2
+IO/FS/STDIN : u24 = 0
+IO/FS/STDOUT : u24 = 1
+IO/FS/STDERR : u24 = 2
### Seek modes
# Seek from start of file.
-IO/FS/SEEK_SET = +0
+IO/FS/SEEK_SET : i24 = +0
# Seek from current position.
-IO/FS/SEEK_CUR = +1
+IO/FS/SEEK_CUR : i24 = +1
# Seek from end of file.
-IO/FS/SEEK_END = +2
+IO/FS/SEEK_END : i24 = +2
### File utilities
-# IO/FS/read_file(path: String) -> (IO (List u24))
# Reads an entire file, returning a list of bytes.
-def IO/FS/read_file(path):
+def IO/FS/read_file(path: String) -> IO(Result(List(u24), u24)):
with IO:
- fd <- IO/done_on_err(IO/FS/open(path, "r"))
- bytes <- IO/FS/read_to_end(fd)
- * <- IO/done_on_err(IO/FS/close(fd))
- return wrap(bytes)
+ res_fd <- IO/FS/open(path, "r")
+ match res_fd:
+ case Result/Ok:
+ fd = res_fd.val
+ res1 <- IO/FS/read_to_end(fd)
+ res2 <- IO/FS/close(fd)
+ return wrap(Result/and(res2, res1))
+ case Result/Err:
+ return wrap(Result/Err(res_fd.val))
-# IO/FS/read_to_end(fd: u24) -> (IO (List u24))
# Reads the remaining contents of a file, returning a list of read bytes.
-def IO/FS/read_to_end(fd):
+def IO/FS/read_to_end(fd: u24) -> IO(Result(List(u24), u24)):
return IO/FS/read_to_end.read_chunks(fd, [])
-def IO/FS/read_to_end.read_chunks(fd, chunks):
+def IO/FS/read_to_end.read_chunks(fd: u24, chunks: List(List(u24))) -> IO(Result(List(u24), u24)):
with IO:
# Read file in 1MB chunks
- chunk <- IO/done_on_err(IO/FS/read(fd, 1048576))
- match chunk:
- case List/Nil:
- return wrap(List/flatten(chunks))
- case List/Cons:
- return IO/FS/read_to_end.read_chunks(fd, List/Cons(chunk, chunks))
-
-# IO/FS/read_line(fd: u24) -> (IO (List u24))
+ res_chunk <- IO/FS/read(fd, 1048576)
+ match res_chunk:
+ case Result/Ok:
+ chunk = res_chunk.val
+ match chunk:
+ case List/Nil:
+ return wrap(Result/Ok(List/flatten(chunks)))
+ case List/Cons:
+ return IO/FS/read_to_end.read_chunks(fd, List/Cons(chunk, chunks))
+ case Result/Err:
+ return wrap(Result/Err(res_chunk.val))
+
# Reads a single line from a file, returning a list of bytes.
-def IO/FS/read_line(fd):
+def IO/FS/read_line(fd: u24) -> IO(Result(List(u24), u24)):
return IO/FS/read_line.read_chunks(fd, [])
-def IO/FS/read_line.read_chunks(fd, chunks):
+def IO/FS/read_line.read_chunks(fd: u24, chunks: List(List(u24))) -> IO(Result(List(u24), u24)):
with IO:
# Read line in 1kB chunks
- chunk <- IO/done_on_err(IO/FS/read(fd, 1024))
- match res = List/split_once(chunk, '\n'):
- # Found a newline, backtrack and join chunks
+ res_chunk <- IO/FS/read(fd, 1024)
+ match res_chunk:
case Result/Ok:
- (line, rest) = res.val
- (length, *) = List/length(rest)
- * <- IO/FS/seek(fd, to_i24(length) * -1, IO/FS/SEEK_CUR)
- chunks = List/Cons(line, chunks)
- bytes = List/flatten(chunks)
- return wrap(bytes)
- # Newline not found
+ chunk = res_chunk.val
+ match res = List/split_once(chunk, lambda x: x == '\n'):
+ # Found a newline, backtrack and join chunks
+ case Result/Ok:
+ (line, rest) = res.val
+ (length, *) = List/length(rest)
+ res_seek <- IO/FS/seek(fd, u24/to_i24(length) * -1, IO/FS/SEEK_CUR)
+ match res_seek:
+ case Result/Ok:
+ chunks = List/Cons(line, chunks)
+ bytes = List/flatten(chunks)
+ return wrap(Result/Ok(bytes))
+ case Result/Err:
+ return wrap(Result/Err(res_seek.val))
+ # Newline not found
+ case Result/Err:
+ line = res.val
+ (length, line) = List/length(line)
+ # If length is 0, the end of the file was reached, return as if it was a newline
+ if length == 0:
+ bytes = List/flatten(chunks)
+ return wrap(Result/Ok(bytes))
+ # Otherwise, the line is still ongoing, read more chunks
+ else:
+ chunks = List/Cons(line, chunks)
+ return IO/FS/read_line.read_chunks(fd, chunks)
case Result/Err:
- line = res.val
- (length, line) = List/length(line)
- # If length is 0, the end of the file was reached, return as if it was a newline
- if length == 0:
- bytes = List/flatten(chunks)
- return wrap(bytes)
- # Otherwise, the line is still ongoing, read more chunks
- else:
- chunks = List/Cons(line, chunks)
- return IO/FS/read_line.read_chunks(fd, chunks)
-
-# IO/FS/write_file(path: String, bytes: (List u24)) -> (IO None)
+ return wrap(Result/Err(res_chunk.val))
+
# Writes a list of bytes to a file given by a path.
-def IO/FS/write_file(path, bytes):
+def IO/FS/write_file(path: String, bytes: List(u24)) -> IO(Result(None, u24)):
with IO:
- f <- IO/FS/open(path, "w")
- match f:
- case Result/Err:
- return wrap(Result/Err(f.val))
+ res_f <- IO/FS/open(path, "w")
+ match res_f:
case Result/Ok:
- * <- IO/done_on_err(IO/FS/write(f.val, bytes))
- * <- IO/done_on_err(IO/FS/close(f.val))
- return wrap(Result/Ok(bytes))
+ f = res_f.val
+ res1 <- IO/FS/write(f, bytes)
+ res2 <- IO/FS/close(f)
+ return wrap(Result/and(res2, res1))
+ case Result/Err:
+ return wrap(Result/Err(res_f.val))
### Standard input and output utilities
-# IO/print(text: String) -> (IO *)
# Prints a string to stdout, encoding it with utf-8.
-IO/print text = with IO {
- ask res = (IO/FS/write IO/FS/STDOUT (String/encode_utf8 text))
- (wrap (Result/unwrap res))
- }
+def IO/print(text: String) -> IO(None):
+ with IO:
+ res <- IO/FS/write(IO/FS/STDOUT, String/encode_utf8(text))
+ return wrap(Result/unwrap(res))
# IO/input() -> IO String
# Read characters from stdin until a newline is found.
# Returns the read input decoded as utf-8.
-IO/input = (IO/input.go DiffList/new)
-def IO/input.go(acc):
+def IO/input() -> IO(Result(String, u24)):
+ return IO/input.go(DiffList/new)
+
+def IO/input.go(acc: List(u24) -> List(u24)) -> IO(Result(String, u24)):
# TODO: This is slow and inefficient, should be done in hvm using fgets.
with IO:
- byte <- IO/done_on_err(IO/FS/read(IO/FS/STDIN, 1))
- match byte:
- case List/Nil:
- # Nothing read, try again (to simulate blocking a read)
- return IO/input.go(acc)
- case List/Cons:
- if byte.head == '\n':
- bytes = DiffList/to_list(acc)
- text = String/decode_utf8(bytes)
- return wrap(text)
- else:
- acc = DiffList/append(acc, byte.head)
- return IO/input.go(acc)
+ res_byte <- IO/FS/read(IO/FS/STDIN, 1)
+ match res_byte:
+ case Result/Ok:
+ byte = res_byte.val
+ match byte:
+ case List/Nil:
+ # Nothing read, try again (to simulate blocking a read)
+ return IO/input.go(acc)
+ case List/Cons:
+ if byte.head == '\n':
+ bytes = DiffList/to_list(acc)
+ text = String/decode_utf8(bytes)
+ return wrap(Result/Ok(text))
+ else:
+ acc = DiffList/append(acc, byte.head)
+ return IO/input.go(acc)
+ case Result/Err:
+ return wrap(Result/Err(res_byte.val))
### Dynamically linked libraries
-# IO/DyLib/open(path: String, lazy: u24) -> u24
+# Returns an unique id to the library object encoded as a u24
# 'path' is the path to the library file.
# 'lazy' is a boolean encoded as a u24 that determines if all functions are loaded lazily or upfront.
-# Returns an unique id to the library object encoded as a u24
-def IO/DyLib/open(path, lazy):
- return IO/Call(IO/MAGIC, "DL_OPEN", (path, lazy), IO/wrap)
+def IO/DyLib/open(path: String, lazy: u24) -> IO(Result(u24, String)):
+ return IO/unwrap_inner(IO/call("DL_OPEN", (path, lazy)))
-# IO/DyLib/call(dl: u24, fn: String, args: Any) -> Any
# Calls a function of a previously opened library.
+# The returned value is determined by the called function.
# 'dl' is the id of the library object.
# 'fn' is the name of the function in the library.
# 'args' are the arguments to the function. The expected values depend on the called function.
-# The returned value is determined by the called function.
-def IO/DyLib/call(dl, fn, args):
- return IO/Call(IO/MAGIC, "DL_CALL", (dl, fn, args), IO/wrap)
+def IO/DyLib/call(dl: u24, fn: String, args: Any) -> IO(Result(Any, String)):
+ return IO/unwrap_inner(IO/call("DL_CALL", (dl, (fn, args))))
-# IO/DyLib/close(dl: u24) -> None
# Closes a previously open library.
-# 'dl' is the id of the library object.
# Returns nothing.
-def IO/DyLib/close(dl):
- return IO/Call(IO/MAGIC, "DL_CLOSE", (dl), IO/wrap)
+# 'dl' is the id of the library object.
+def IO/DyLib/close(dl: u24) -> IO(Result(None, String)):
+ return IO/unwrap_inner(IO/call("DL_CLOSE", dl))
# Lazy thunks
-# defer(val: T) -> ((T -> T) -> T)
-# We can defer the evaluation of a function by wrapping it in a thunk
+
+# We can defer the evaluation of a function by wrapping it in a thunk.
# Ex: @x (x @arg1 @arg2 @arg3 (f arg1 arg2 arg3) arg1 arg2 arg3)
-# This is only evaluated when we call it with 'undefer' (undefer my_thunk)
-# We can build a defered call directly or by by using defer and defer_arg
+#
+# This is only evaluated when we call it with `(undefer my_thunk)`.
+# We can build a defered call directly or by by using `defer` and `defer_arg`.
+#
# The example above can be written as:
+#
# (defer_arg (defer_arg (defer_arg (defer @arg1 @arg2 @arg3 (f arg1 arg2 arg3)) arg1) arg2) arg3)
-defer val = @x (x val)
+def defer(val: T) -> (T -> T) -> T:
+ return lambda x: x(val)
-# defer_arg(defered: A -> B -> C, arg: B) -> (A -> C)
-defer_arg defered arg = @x (defered x arg)
+def defer_arg(defered: (Id -> Id) -> A -> B, arg: A) -> ((Id -> Id) -> B):
+ return lambda x: defered(x, arg)
-# undefer(defered: (A -> A) -> B) -> B
-undefer defered = (defered @x x)
+def undefer(defered: (Id -> Id) -> T) -> T:
+ return defered(lambda x: x)
+# A function that can be used in unreachable code.
+#
+# Is not type safe and if used in code that is actually reachable, will corrupt the program.
+def unreachable() -> Any:
+ return *
# Native number casts
-# to_f24(x: native number) -> f24
-# Casts any native number to an f24.
-hvm to_f24:
- ($([f24] ret) ret)
+# Casts a f24 number to a u24.
+hvm f24/to_u24 -> (f24 -> u24):
+ ($([u24] ret) ret)
-# to_u24(x: native number) -> u24
-# Casts any native number to a u24.
-hvm to_u24:
+# Casts an i24 number to a u24.
+hvm i24/to_u24 -> (i24 -> u24):
($([u24] ret) ret)
-# to_i24(x: native number) -> i24
-# Casts any native number to an i24.
-hvm to_i24:
+# Casts a u24 number to an i24.
+hvm u24/to_i24 -> (u24 -> i24):
($([i24] ret) ret)
+# Casts a f24 number to an i24.
+hvm f24/to_i24 -> (f24 -> i24):
+ ($([i24] ret) ret)
+
+# Casts a u24 number to a f24.
+hvm u24/to_f24 -> (u24 -> f24):
+ ($([f24] ret) ret)
+
+# Casts an i24 number to a f24.
+hvm i24/to_f24 -> (i24 -> f24):
+ ($([f24] ret) ret)
+
+def u24/to_string(n: u24) -> String:
+ def go(n: u24) -> String -> String:
+ r = n % 10
+ d = n / 10
+ c = '0' + r
+ if d == 0:
+ return lambda t: String/Cons(c, t)
+ else:
+ return lambda t: go(d, String/Cons(c, t))
+ return go(n, String/Nil)
+
# String Encoding and Decoding
-Utf8/REPLACEMENT_CHARACTER = '\u{FFFD}'
+Utf8/REPLACEMENT_CHARACTER : u24 = '\u{FFFD}'
-# String/decode_utf8(List u24) -> String
# Decodes a sequence of bytes to a String using utf-8 encoding.
-String/decode_utf8 bytes =
+# Invalid utf-8 sequences are replaced with Utf8/REPLACEMENT_CHARACTER.
+String/decode_utf8 (bytes: (List u24)) : String =
let (got, rest) = (Utf8/decode_character bytes)
match rest {
List/Nil: (String/Cons got String/Nil)
List/Cons: (String/Cons got (String/decode_utf8 rest))
}
-# Utf8/decode_character(List u24) -> (u24, List u24)
# Decodes one utf-8 character from the start of a sequence of bytes.
# Returns the decoded character and the remaining bytes.
+Utf8/decode_character (bytes: (List u24)) : (u24, (List u24))
Utf8/decode_character [] = (0, [])
Utf8/decode_character [a] = if (<= a 0x7F) { (a, []) } else { (Utf8/REPLACEMENT_CHARACTER, []) }
Utf8/decode_character [a, b] =
@@ -506,8 +631,8 @@ Utf8/decode_character (List/Cons a (List/Cons b (List/Cons c (List/Cons d rest))
}
}
-# String/encode_utf8(String) -> (List u24)
# Encodes a string to a sequence of bytes using utf-8 encoding.
+String/encode_utf8 (str: String) : (List u24)
String/encode_utf8 (String/Nil) = (List/Nil)
String/encode_utf8 (String/Cons x xs) =
use Utf8/rune1max = 0b01111111
@@ -541,13 +666,13 @@ String/encode_utf8 (String/Cons x xs) =
}
}
-# String/decode_ascii(List u24) -> String
# Decodes a sequence of bytes to a String using ascii encoding.
+String/decode_ascii (bytes: (List u24)) : String
String/decode_ascii (List/Cons x xs) = (String/Cons x (String/decode_ascii xs))
String/decode_ascii (List/Nil) = (String/Nil)
-# String/encode_ascii(String) -> (List u24)
# Encodes a string to a sequence of bytes using ascii encoding.
+String/encode_ascii (str: String) : (List u24)
String/encode_ascii (String/Cons x xs) = (List/Cons x (String/encode_ascii xs))
String/encode_ascii (String/Nil) = (List/Nil)
@@ -555,95 +680,92 @@ String/encode_ascii (String/Nil) = (List/Nil)
# Math/PI() -> f24
# The Pi (π) constant.
-def Math/PI():
+def Math/PI() -> f24:
return 3.1415926535
-def Math/E():
+def Math/E() -> f24:
return 2.718281828
# Math/log(x: f24, base: f24) -> f24
# Computes the logarithm of `x` with the specified `base`.
-hvm Math/log:
+hvm Math/log -> (f24 -> f24 -> f24):
(x ($([|] $(x ret)) ret))
# Math/atan2(x: f24, y: f24) -> f24
# Has the same behaviour as `atan2f` in the C math lib.
# Computes the arctangent of the quotient of its two arguments.
-hvm Math/atan2:
+hvm Math/atan2 -> (f24 -> f24 -> f24):
($([&] $(y ret)) (y ret))
# Math/sin(a: f24) -> f24
# Computes the sine of the given angle in radians.
-hvm Math/sin:
+hvm Math/sin -> (f24 -> f24):
($([<<0x0] a) a)
# Math/cos(a: f24) -> f24
# Computes the cosine of the given angle in radians.
-hvm Math/cos:
+hvm Math/cos -> (f24 -> f24):
(a b)
& @Math/PI ~ $([:/2.0] $([-] $(a $([<<0x0] b))))
# Math/tan(a: f24) -> f24
# Computes the tangent of the given angle in radians.
-hvm Math/tan:
+hvm Math/tan -> (f24 -> f24):
($([>>0x0] a) a)
-# Math/cot(a: f24) -> f24
# Computes the cotangent of the given angle in radians.
-Math/cot a = (/ 1.0 (Math/tan a))
+Math/cot (a: f24) : f24 =
+ (/ 1.0 (Math/tan a))
-# Math/sec(a: f24) -> f24
# Computes the secant of the given angle in radians.
-Math/sec a = (/ 1.0 (Math/cos a))
+Math/sec (a: f24) : f24 =
+ (/ 1.0 (Math/cos a))
-# Math/csc(a: f24) -> f24
# Computes the cosecant of the given angle in radians.
-Math/csc a = (/ 1.0 (Math/sin a))
+Math/csc (a: f24) : f24 =
+ (/ 1.0 (Math/sin a))
-# Math/atan(a: f24) -> f24
# Computes the arctangent of the given angle.
-Math/atan a = (Math/atan2 a 1.0)
+Math/atan (a: f24) : f24 =
+ (Math/atan2 a 1.0)
-# Math/asin(a: f24) -> f24
# Computes the arcsine of the given angle.
-Math/asin a = (Math/atan2 a (Math/sqrt (- 1.0 (* a a))))
+Math/asin (a: f24) : f24 =
+ (Math/atan2 a (Math/sqrt (- 1.0 (* a a))))
-# Math/acos(a: f24) -> f24
# Computes the arccosine of the given angle.
-Math/acos a = (Math/atan2 (Math/sqrt (- 1.0 (* a a))) a)
+Math/acos (a: f24) : f24 =
+ (Math/atan2 (Math/sqrt (- 1.0 (* a a))) a)
-# Math/radians(a: f24) -> f24
# Converts degrees to radians.
-Math/radians a = (* a (/ Math/PI 180.0))
+Math/radians (a: f24) : f24 =
+ (* a (/ Math/PI 180.0))
-# Math/sqrt(x: f24) -> f24
# Computes the square root of the given number.
-Math/sqrt n = (** n 0.5)
+Math/sqrt (n: f24) : f24 =
+ (** n 0.5)
-# Math/ceil(n: f24) -> f24
# Round float up to the nearest integer.
-def Math/ceil(n):
- i_n = to_f24(to_i24(n))
+def Math/ceil(n: f24) -> f24:
+ i_n = i24/to_f24(f24/to_i24(n))
if n <= i_n:
return i_n
else:
return i_n + 1.0
-# Math/floor(n: f24) -> f24
# Round float down to the nearest integer.
-def Math/floor(n):
- i_n = to_f24(to_i24(n))
+def Math/floor(n: f24) -> f24:
+ i_n = i24/to_f24(f24/to_i24(n))
if n < i_n:
return i_n - 1.0
else:
return i_n
-# Math/round(n: f24) -> f24
# Round float to the nearest integer.
-def Math/round(n):
- i_n = to_f24(to_i24(n))
- if n - i_n < 0.5:
+def Math/round(n: f24) -> f24:
+ i_n = i24/to_f24(f24/to_i24(n))
+ if (n - i_n) < 0.5:
return Math/floor(n)
else:
return Math/ceil(n)
diff --git a/src/fun/builtins.rs b/src/fun/builtins.rs
index d9489ffef..10d650874 100644
--- a/src/fun/builtins.rs
+++ b/src/fun/builtins.rs
@@ -1,5 +1,5 @@
use super::{
- parser::{ParseBook, TermParser},
+ parser::{FunParser, ParseBook},
Book, Name, Num, Pattern, Term,
};
use crate::maybe_grow;
@@ -47,7 +47,8 @@ pub const BUILTIN_TYPES: &[&str] = &[LIST, STRING, NAT, TREE, MAP, IO];
impl ParseBook {
pub fn builtins() -> Self {
- let book = TermParser::new(BUILTINS).parse_book(Self::default(), true);
+ let book =
+ FunParser::new(Name::new("/src/fun/builtins.bend"), BUILTINS, true).parse_book(Self::default());
book.unwrap_or_else(|e| panic!("Error parsing builtin file, this should not happen:\n{e}"))
}
}
diff --git a/src/fun/check/check_untyped.rs b/src/fun/check/check_untyped.rs
new file mode 100644
index 000000000..9f74e80a2
--- /dev/null
+++ b/src/fun/check/check_untyped.rs
@@ -0,0 +1,81 @@
+use crate::{
+ diagnostics::Diagnostics,
+ fun::{Ctx, FanKind, Pattern, Tag, Term},
+ maybe_grow,
+};
+
+impl Ctx<'_> {
+ /// Checks that terms that cannot be typed are only used inside untyped functions.
+ pub fn check_untyped_terms(&mut self) -> Result<(), Diagnostics> {
+ for def in self.book.defs.values() {
+ if def.check {
+ for rule in def.rules.iter() {
+ if let Err(e) = rule.body.check_untyped_terms() {
+ self.info.add_function_error(e, def.name.clone(), def.source.clone());
+ }
+ }
+ }
+ }
+ self.info.fatal(())
+ }
+}
+
+impl Term {
+ fn check_untyped_terms(&self) -> Result<(), String> {
+ maybe_grow(|| {
+ match self {
+ Term::Lam { tag: Tag::Static, pat, .. } => pat.check_untyped_patterns()?,
+ Term::Lam { tag: _, .. } => {
+ return Err("Tagged lambda in type-checked function".to_string());
+ }
+ Term::Link { nam } => {
+ return Err(format!("Unscoped variable '${nam}' in type-checked function"));
+ }
+ Term::App { tag: Tag::Static, .. } => {}
+ Term::App { tag: _, .. } => {
+ return Err("Tagged application in type-checked function".to_string());
+ }
+ Term::Fan { fan: FanKind::Dup, .. } => {
+ return Err("Superposition term in type-checked function".to_string());
+ }
+ Term::Fan { fan: FanKind::Tup, tag: Tag::Static, .. } => {}
+ Term::Fan { fan: FanKind::Tup, tag: _, .. } => {
+ return Err("Tagged tuple in type-checked function".to_string());
+ }
+ Term::Let { pat, .. } => {
+ pat.check_untyped_patterns()?;
+ }
+ _ => {}
+ }
+ for child in self.children() {
+ child.check_untyped_terms()?;
+ }
+ Ok(())
+ })
+ }
+}
+
+impl Pattern {
+ fn check_untyped_patterns(&self) -> Result<(), String> {
+ maybe_grow(|| {
+ match self {
+ Pattern::Chn(x) => {
+ return Err(format!("Unscoped variable bind '${x}' in type-checked function"));
+ }
+ Pattern::Fan(FanKind::Dup, Tag::Auto, _) => {}
+ Pattern::Fan(FanKind::Dup, _, _) => {
+ return Err("Tagged duplication in type-checked function".to_string());
+ }
+ Pattern::Fan(FanKind::Tup, Tag::Static, _) => {}
+ Pattern::Fan(FanKind::Tup, _, _) => {
+ return Err("Tagged tuple elimination in type-checked function".to_string());
+ }
+ _ => {}
+ }
+ for pat in self.children() {
+ pat.check_untyped_patterns()?;
+ }
+ Ok(())
+ })
+ }
+}
diff --git a/src/fun/check/mod.rs b/src/fun/check/mod.rs
index e54bdbd3f..21a8e2c8f 100644
--- a/src/fun/check/mod.rs
+++ b/src/fun/check/mod.rs
@@ -1,4 +1,6 @@
+pub mod check_untyped;
pub mod set_entrypoint;
pub mod shared_names;
+pub mod type_check;
pub mod unbound_refs;
pub mod unbound_vars;
diff --git a/src/fun/check/type_check.rs b/src/fun/check/type_check.rs
new file mode 100644
index 000000000..a06935c11
--- /dev/null
+++ b/src/fun/check/type_check.rs
@@ -0,0 +1,785 @@
+//! Optional Hindley-Milner-like type system.
+//!
+//! Based on https://github.com/developedby/algorithm-w-rs
+//! and https://github.com/mgrabmueller/AlgorithmW.
+use crate::{
+ diagnostics::Diagnostics,
+ fun::{num_to_name, Adt, Book, Ctx, FanKind, MatchRule, Name, Num, Op, Pattern, Tag, Term, Type},
+ maybe_grow,
+};
+use std::collections::{BTreeMap, BTreeSet, HashMap};
+
+impl Ctx<'_> {
+ pub fn type_check(&mut self) -> Result<(), Diagnostics> {
+ let types = infer_book(self.book, &mut self.info)?;
+
+ for def in self.book.defs.values_mut() {
+ def.typ = types[&def.name].instantiate(&mut VarGen::default());
+ }
+
+ Ok(())
+ }
+}
+
+type ProgramTypes = HashMap;
+
+/// A type scheme, aka a polymorphic type.
+#[derive(Clone)]
+struct Scheme(Vec, Type);
+
+/// A finite mapping from type variables to types.
+#[derive(Clone, Default)]
+struct Subst(BTreeMap);
+
+/// A mapping from term variables to type schemes.
+#[derive(Clone, Default)]
+struct TypeEnv(BTreeMap);
+
+/// Variable generator for type variables.
+#[derive(Default)]
+struct VarGen(usize);
+
+/// Topologically ordered set of mutually recursive groups of functions.
+struct RecGroups(Vec>);
+
+/* Implementations */
+
+impl Type {
+ fn free_type_vars(&self) -> BTreeSet {
+ maybe_grow(|| match self {
+ Type::Var(x) => BTreeSet::from([x.clone()]),
+ Type::Ctr(_, ts) | Type::Tup(ts) => ts.iter().flat_map(|t| t.free_type_vars()).collect(),
+ Type::Arr(t1, t2) => t1.free_type_vars().union(&t2.free_type_vars()).cloned().collect(),
+ Type::Number(t) | Type::Integer(t) => t.free_type_vars(),
+ Type::U24 | Type::F24 | Type::I24 | Type::None | Type::Any | Type::Hole => BTreeSet::new(),
+ })
+ }
+
+ fn subst(&self, subst: &Subst) -> Type {
+ maybe_grow(|| match self {
+ Type::Var(nam) => match subst.0.get(nam) {
+ Some(new) => new.clone(),
+ None => self.clone(),
+ },
+ Type::Ctr(name, ts) => Type::Ctr(name.clone(), ts.iter().map(|t| t.subst(subst)).collect()),
+ Type::Arr(t1, t2) => Type::Arr(Box::new(t1.subst(subst)), Box::new(t2.subst(subst))),
+ Type::Tup(els) => Type::Tup(els.iter().map(|t| t.subst(subst)).collect()),
+ Type::Number(t) => Type::Number(Box::new(t.subst(subst))),
+ Type::Integer(t) => Type::Integer(Box::new(t.subst(subst))),
+ t @ (Type::U24 | Type::F24 | Type::I24 | Type::None | Type::Any | Type::Hole) => t.clone(),
+ })
+ }
+
+ /// Converts a monomorphic type into a type scheme by abstracting
+ /// over the type variables free in `t`, but not free in the type
+ /// environment.
+ fn generalize(&self, env: &TypeEnv) -> Scheme {
+ let vars_env = env.free_type_vars();
+ let vars_t = self.free_type_vars();
+ let vars = vars_t.difference(&vars_env).cloned().collect();
+ Scheme(vars, self.clone())
+ }
+}
+
+impl Scheme {
+ fn free_type_vars(&self) -> BTreeSet {
+ let vars = self.1.free_type_vars();
+ let bound_vars = self.0.iter().cloned().collect();
+ vars.difference(&bound_vars).cloned().collect()
+ }
+
+ fn subst(&self, subst: &Subst) -> Scheme {
+ let mut subst = subst.clone();
+ for x in self.0.iter() {
+ subst.0.remove(x);
+ }
+ let t = self.1.subst(&subst);
+ Scheme(self.0.clone(), t)
+ }
+
+ /// Converts a type scheme into a monomorphic type by assigning
+ /// fresh type variables to each variable bound by the scheme.
+ fn instantiate(&self, var_gen: &mut VarGen) -> Type {
+ let new_vars = self.0.iter().map(|_| var_gen.fresh());
+ let subst = Subst(self.0.iter().cloned().zip(new_vars).collect());
+ self.1.subst(&subst)
+ }
+}
+
+impl Subst {
+ /// Compose two substitutions.
+ ///
+ /// Applies the first substitution to the second, and then inserts the result into the first.
+ fn compose(mut self, other: Subst) -> Subst {
+ let other = other.0.into_iter().map(|(x, t)| (x, t.subst(&self))).collect::>();
+ self.0.extend(other);
+ self
+ }
+}
+
+impl TypeEnv {
+ fn free_type_vars(&self) -> BTreeSet {
+ let mut vars = BTreeSet::new();
+ for scheme in self.0.values() {
+ let scheme_vars = scheme.free_type_vars();
+ vars = vars.union(&scheme_vars).cloned().collect();
+ }
+ vars
+ }
+
+ fn subst(&self, subst: &Subst) -> TypeEnv {
+ let env = self.0.iter().map(|(x, scheme)| (x.clone(), scheme.subst(subst))).collect();
+ TypeEnv(env)
+ }
+
+ fn insert(&mut self, name: Name, scheme: Scheme) {
+ self.0.insert(name, scheme);
+ }
+
+ fn add_binds<'a>(
+ &mut self,
+ bnd: impl IntoIterator, Scheme)>,
+ ) -> Vec<(Name, Option)> {
+ let mut old_bnd = vec![];
+ for (name, scheme) in bnd {
+ if let Some(name) = name {
+ let old = self.0.insert(name.clone(), scheme);
+ old_bnd.push((name.clone(), old));
+ }
+ }
+ old_bnd
+ }
+
+ fn pop_binds(&mut self, old_bnd: Vec<(Name, Option)>) {
+ for (name, scheme) in old_bnd {
+ if let Some(scheme) = scheme {
+ self.0.insert(name, scheme);
+ }
+ }
+ }
+}
+
+impl VarGen {
+ fn fresh(&mut self) -> Type {
+ let x = self.fresh_name();
+ Type::Var(x)
+ }
+
+ fn fresh_name(&mut self) -> Name {
+ let x = num_to_name(self.0 as u64);
+ self.0 += 1;
+ Name::new(x)
+ }
+}
+
+impl RecGroups {
+ fn from_book(book: &Book) -> RecGroups {
+ type DependencyGraph<'a> = BTreeMap<&'a Name, BTreeSet<&'a Name>>;
+
+ fn collect_dependencies<'a>(
+ term: &'a Term,
+ book: &'a Book,
+ scope: &mut Vec,
+ deps: &mut BTreeSet<&'a Name>,
+ ) {
+ if let Term::Ref { nam } = term {
+ if book.ctrs.contains_key(nam) || book.hvm_defs.contains_key(nam) || !book.defs[nam].check {
+ // Don't infer types for constructors or unchecked functions
+ } else {
+ deps.insert(nam);
+ }
+ }
+ for (child, binds) in term.children_with_binds() {
+ scope.extend(binds.clone().flatten().cloned());
+ collect_dependencies(child, book, scope, deps);
+ scope.truncate(scope.len() - binds.flatten().count());
+ }
+ }
+
+ /// Tarjan's algorithm for finding strongly connected components.
+ fn strong_connect<'a>(
+ v: &'a Name,
+ deps: &DependencyGraph<'a>,
+ index: &mut usize,
+ index_map: &mut BTreeMap<&'a Name, usize>,
+ low_link: &mut BTreeMap<&'a Name, usize>,
+ stack: &mut Vec<&'a Name>,
+ components: &mut Vec>,
+ ) {
+ maybe_grow(|| {
+ index_map.insert(v, *index);
+ low_link.insert(v, *index);
+ *index += 1;
+ stack.push(v);
+
+ if let Some(neighbors) = deps.get(v) {
+ for w in neighbors {
+ if !index_map.contains_key(w) {
+ // Successor w has not yet been visited, recurse on it.
+ strong_connect(w, deps, index, index_map, low_link, stack, components);
+ low_link.insert(v, low_link[v].min(low_link[w]));
+ } else if stack.contains(w) {
+ // Successor w is in stack S and hence in the current SCC.
+ low_link.insert(v, low_link[v].min(index_map[w]));
+ } else {
+ // If w is not on stack, then (v, w) is an edge pointing
+ // to an SCC already found and must be ignored.
+ }
+ }
+ }
+
+ // If v is a root node, pop the stack and generate an SCC.
+ if low_link[v] == index_map[v] {
+ let mut component = BTreeSet::new();
+ while let Some(w) = stack.pop() {
+ component.insert(w.clone());
+ if w == v {
+ break;
+ }
+ }
+ components.push(component);
+ }
+ })
+ }
+
+ // Build the dependency graph
+ let mut deps = DependencyGraph::default();
+ for (name, def) in &book.defs {
+ if book.ctrs.contains_key(name) || !def.check {
+ // Don't infer types for constructors or unchecked functions
+ continue;
+ }
+ let mut fn_deps = Default::default();
+ collect_dependencies(&def.rule().body, book, &mut vec![], &mut fn_deps);
+ deps.insert(name, fn_deps);
+ }
+
+ let mut index = 0;
+ let mut stack = Vec::new();
+ let mut index_map = BTreeMap::new();
+ let mut low_link = BTreeMap::new();
+ let mut components = Vec::new();
+ for name in deps.keys() {
+ if !index_map.contains_key(name) {
+ strong_connect(name, &deps, &mut index, &mut index_map, &mut low_link, &mut stack, &mut components);
+ }
+ }
+ let components = components.into_iter().map(|x| x.into_iter().collect()).collect();
+ RecGroups(components)
+ }
+}
+
+/* Inference, unification and type checking */
+fn infer_book(book: &Book, diags: &mut Diagnostics) -> Result {
+ let groups = RecGroups::from_book(book);
+ let mut env = TypeEnv::default();
+ // Note: We store the inferred and generalized types in a separate
+ // environment, to avoid unnecessary cloning (since no immutable data).
+ let mut types = ProgramTypes::default();
+
+ // Add the constructors to the environment.
+ for adt in book.adts.values() {
+ for ctr in adt.ctrs.values() {
+ types.insert(ctr.name.clone(), ctr.typ.generalize(&TypeEnv::default()));
+ }
+ }
+ // Add the types of unchecked functions to the environment.
+ for def in book.defs.values() {
+ if !def.check {
+ types.insert(def.name.clone(), def.typ.generalize(&TypeEnv::default()));
+ }
+ }
+ // Add the types of hvm functions to the environment.
+ for def in book.hvm_defs.values() {
+ types.insert(def.name.clone(), def.typ.generalize(&TypeEnv::default()));
+ }
+
+ // Infer the types of regular functions.
+ for group in &groups.0 {
+ infer_group(&mut env, book, group, &mut types, diags)?;
+ }
+ Ok(types)
+}
+
+fn infer_group(
+ env: &mut TypeEnv,
+ book: &Book,
+ group: &[Name],
+ types: &mut ProgramTypes,
+ diags: &mut Diagnostics,
+) -> Result<(), Diagnostics> {
+ let var_gen = &mut VarGen::default();
+ // Generate fresh type variables for each function in the group.
+ let tvs = group.iter().map(|_| var_gen.fresh()).collect::>();
+ for (name, tv) in group.iter().zip(tvs.iter()) {
+ env.insert(name.clone(), Scheme(vec![], tv.clone()));
+ }
+
+ // Infer the types of the functions in the group.
+ let mut ss = vec![];
+ let mut inf_ts = vec![];
+ let mut exp_ts = vec![];
+ for name in group {
+ let def = &book.defs[name];
+ let (s, t) = infer(env, book, types, &def.rule().body, var_gen).map_err(|e| {
+ diags.add_function_error(e, name.clone(), def.source.clone());
+ std::mem::take(diags)
+ })?;
+ let t = t.subst(&s);
+ ss.push(s);
+ inf_ts.push(t);
+ exp_ts.push(&def.typ);
+ }
+
+ // Remove the type variables of the group from the environment.
+ // This avoids cloning of already generalized types.
+ for name in group.iter() {
+ env.0.remove(name);
+ }
+
+ // Unify the inferred body with the corresponding type variable.
+ let mut s = ss.into_iter().fold(Subst::default(), |acc, s| acc.compose(s));
+ let mut ts = vec![];
+ for ((bod_t, tv), nam) in inf_ts.into_iter().zip(tvs.iter()).zip(group.iter()) {
+ let (t, s2) = unify_term(&tv.subst(&s), &bod_t, &book.defs[nam].rule().body)?;
+ ts.push(t);
+ s = s.compose(s2);
+ }
+ let ts = ts.into_iter().map(|t| t.subst(&s)).collect::>();
+
+ // Specialize against the expected type, then generalize and store.
+ for ((name, exp_t), inf_t) in group.iter().zip(exp_ts.iter()).zip(ts.iter()) {
+ let t = specialize(inf_t, exp_t).map_err(|e| {
+ diags.add_function_error(e, name.clone(), book.defs[name].source.clone());
+ std::mem::take(diags)
+ })?;
+ types.insert(name.clone(), t.generalize(&TypeEnv::default()));
+ }
+
+ diags.fatal(())
+}
+
+/// Infer the type of a term in the given environment.
+///
+/// The type environment must contain bindings for all the free variables of the term.
+///
+/// The returned substitution records the type constraints imposed on type variables by the term.
+/// The returned type is the type of the term.
+fn infer(
+ env: &mut TypeEnv,
+ book: &Book,
+ types: &ProgramTypes,
+ term: &Term,
+ var_gen: &mut VarGen,
+) -> Result<(Subst, Type), String> {
+ let res = maybe_grow(|| match term {
+ Term::Var { nam } | Term::Ref { nam } => {
+ if let Some(scheme) = env.0.get(nam) {
+ Ok::<_, String>((Subst::default(), scheme.instantiate(var_gen)))
+ } else if let Some(scheme) = types.get(nam) {
+ Ok((Subst::default(), scheme.instantiate(var_gen)))
+ } else {
+ unreachable!("unbound name '{}'", nam)
+ }
+ }
+ Term::Lam { tag: Tag::Static, pat, bod } => match pat.as_ref() {
+ Pattern::Var(nam) => {
+ let tv = var_gen.fresh();
+ let old_bnd = env.add_binds([(nam, Scheme(vec![], tv.clone()))]);
+ let (s, bod_t) = infer(env, book, types, bod, var_gen)?;
+ env.pop_binds(old_bnd);
+ let var_t = tv.subst(&s);
+ Ok((s, Type::Arr(Box::new(var_t), Box::new(bod_t))))
+ }
+ _ => unreachable!("{}", term),
+ },
+ Term::App { tag: Tag::Static, fun, arg } => {
+ let (s1, fun_t) = infer(env, book, types, fun, var_gen)?;
+ let (s2, arg_t) = infer(&mut env.subst(&s1), book, types, arg, var_gen)?;
+ let app_t = var_gen.fresh();
+ let (_, s3) = unify_term(&fun_t.subst(&s2), &Type::Arr(Box::new(arg_t), Box::new(app_t.clone())), fun)?;
+ let t = app_t.subst(&s3);
+ Ok((s3.compose(s2).compose(s1), t))
+ }
+ Term::Let { pat, val, nxt } => match pat.as_ref() {
+ Pattern::Var(nam) => {
+ let (s1, val_t) = infer(env, book, types, val, var_gen)?;
+ let old_bnd = env.add_binds([(nam, val_t.generalize(&env.subst(&s1)))]);
+ let (s2, nxt_t) = infer(&mut env.subst(&s1), book, types, nxt, var_gen)?;
+ env.pop_binds(old_bnd);
+ Ok((s2.compose(s1), nxt_t))
+ }
+ Pattern::Fan(FanKind::Tup, Tag::Static, _) => {
+ // Tuple elimination behaves like pattern matching.
+ // Variables from tuple patterns don't get generalized.
+ debug_assert!(!(pat.has_unscoped() || pat.has_nested()));
+ let (s1, val_t) = infer(env, book, types, val, var_gen)?;
+
+ let tvs = pat.binds().map(|_| var_gen.fresh()).collect::>();
+ let old_bnd = env.add_binds(pat.binds().zip(tvs.iter().map(|tv| Scheme(vec![], tv.clone()))));
+ let (s2, nxt_t) = infer(&mut env.subst(&s1), book, types, nxt, var_gen)?;
+ env.pop_binds(old_bnd);
+ let tvs = tvs.into_iter().map(|tv| tv.subst(&s2)).collect::>();
+ let (_, s3) = unify_term(&val_t, &Type::Tup(tvs), val)?;
+ Ok((s3.compose(s2).compose(s1), nxt_t))
+ }
+ Pattern::Fan(FanKind::Dup, Tag::Auto, _) => {
+ // We pretend that sups don't exist and dups don't collide.
+ // All variables must have the same type as the body of the dup.
+ debug_assert!(!(pat.has_unscoped() || pat.has_nested()));
+ let (s1, mut val_t) = infer(env, book, types, val, var_gen)?;
+ let tvs = pat.binds().map(|_| var_gen.fresh()).collect::>();
+ let old_bnd = env.add_binds(pat.binds().zip(tvs.iter().map(|tv| Scheme(vec![], tv.clone()))));
+ let (mut s2, nxt_t) = infer(&mut env.subst(&s1), book, types, nxt, var_gen)?;
+ env.pop_binds(old_bnd);
+ for tv in tvs {
+ let (val_t_, s) = unify_term(&val_t, &tv.subst(&s2), val)?;
+ val_t = val_t_;
+ s2 = s2.compose(s);
+ }
+ Ok((s2.compose(s1), nxt_t))
+ }
+ _ => unreachable!(),
+ },
+
+ Term::Mat { bnd: _, arg, with_bnd: _, with_arg: _, arms } => {
+ // Infer type of the scrutinee
+ let (s1, t1) = infer(env, book, types, arg, var_gen)?;
+
+ // Instantiate the expected type of the scrutinee
+ let adt_name = book.ctrs.get(arms[0].0.as_ref().unwrap()).unwrap();
+ let adt = &book.adts[adt_name];
+ let (adt_s, adt_t) = instantiate_adt(adt, var_gen)?;
+
+ // For each case, infer the types and unify them all.
+ // Unify the inferred type of the destructured fields with the
+ // expected from what we inferred from the scrutinee.
+ let (s2, nxt_t) = infer_match_cases(env.subst(&s1), book, types, adt, arms, &adt_s, var_gen)?;
+
+ // Unify the inferred type with the expected type
+ let (_, s3) = unify_term(&t1, &adt_t.subst(&s2), arg)?;
+ Ok((s3.compose(s2).compose(s1), nxt_t))
+ }
+
+ Term::Num { val } => {
+ let t = match val {
+ Num::U24(_) => Type::U24,
+ Num::I24(_) => Type::I24,
+ Num::F24(_) => Type::F24,
+ };
+ Ok((Subst::default(), t))
+ }
+ Term::Oper { opr, fst, snd } => {
+ let (s1, t1) = infer(env, book, types, fst, var_gen)?;
+ let (s2, t2) = infer(&mut env.subst(&s1), book, types, snd, var_gen)?;
+ let (t2, s3) = unify_term(&t2.subst(&s1), &t1.subst(&s2), term)?;
+ let s_args = s3.compose(s2).compose(s1);
+ let t_args = t2.subst(&s_args);
+ // Check numeric type matches the operation
+ let tv = var_gen.fresh();
+ let (t_opr, s_opr) = match opr {
+ // Any numeric type
+ Op::ADD | Op::SUB | Op::MUL | Op::DIV => {
+ unify_term(&t_args, &Type::Number(Box::new(tv.clone())), term)?
+ }
+ Op::EQ | Op::NEQ | Op::LT | Op::GT | Op::GE | Op::LE => {
+ let (_, s) = unify_term(&t_args, &Type::Number(Box::new(tv.clone())), term)?;
+ (Type::U24, s)
+ }
+ // Integers
+ Op::REM | Op::AND | Op::OR | Op::XOR | Op::SHL | Op::SHR => {
+ unify_term(&t_args, &Type::Integer(Box::new(tv.clone())), term)?
+ }
+ // Floating
+ Op::POW => unify_term(&t_args, &Type::F24, term)?,
+ };
+ let t = t_opr.subst(&s_opr);
+ Ok((s_opr.compose(s_args), t))
+ }
+ Term::Swt { bnd: _, arg, with_bnd: _, with_arg: _, pred, arms } => {
+ let (s1, t1) = infer(env, book, types, arg, var_gen)?;
+ let (_, s2) = unify_term(&t1, &Type::U24, arg)?;
+ let s_arg = s2.compose(s1);
+ let mut env = env.subst(&s_arg);
+
+ let mut ss_nums = vec![];
+ let mut ts_nums = vec![];
+ for arm in arms.iter().rev().skip(1) {
+ let (s, t) = infer(&mut env, book, types, arm, var_gen)?;
+ env = env.subst(&s);
+ ss_nums.push(s);
+ ts_nums.push(t);
+ }
+ let old_bnd = env.add_binds([(pred, Scheme(vec![], Type::U24))]);
+ let (s_succ, t_succ) = infer(&mut env, book, types, &arms[1], var_gen)?;
+ env.pop_binds(old_bnd);
+
+ let s_arms = ss_nums.into_iter().fold(s_succ, |acc, s| acc.compose(s));
+ let mut t_swt = t_succ;
+ let mut s_swt = Subst::default();
+ for t_num in ts_nums {
+ let (t, s) = unify_term(&t_swt, &t_num, term)?;
+ t_swt = t;
+ s_swt = s.compose(s_swt);
+ }
+
+ let s = s_swt.compose(s_arms).compose(s_arg);
+ let t = t_swt.subst(&s);
+ Ok((s, t))
+ }
+
+ Term::Fan { fan: FanKind::Tup, tag: Tag::Static, els } => {
+ let res = els.iter().map(|el| infer(env, book, types, el, var_gen)).collect::, _>>()?;
+ let (ss, ts): (Vec, Vec) = res.into_iter().unzip();
+ let t = Type::Tup(ts);
+ let s = ss.into_iter().fold(Subst::default(), |acc, s| acc.compose(s));
+ Ok((s, t))
+ }
+ Term::Era => Ok((Subst::default(), Type::None)),
+ Term::Fan { .. } | Term::Lam { tag: _, .. } | Term::App { tag: _, .. } | Term::Link { .. } => {
+ unreachable!("'{term}' while type checking. Should never occur in checked functions")
+ }
+ Term::Use { .. }
+ | Term::With { .. }
+ | Term::Ask { .. }
+ | Term::Nat { .. }
+ | Term::Str { .. }
+ | Term::List { .. }
+ | Term::Fold { .. }
+ | Term::Bend { .. }
+ | Term::Open { .. }
+ | Term::Def { .. }
+ | Term::Err => unreachable!("'{term}' while type checking. Should have been removed in earlier pass"),
+ })?;
+ Ok(res)
+}
+
+/// Instantiates the type constructor of an ADT, also returning the
+/// ADT var to instantiated var substitution, to be used when
+/// instantiating the types of the fields of the eliminated constructors.
+fn instantiate_adt(adt: &Adt, var_gen: &mut VarGen) -> Result<(Subst, Type), String> {
+ let tvs = adt.vars.iter().map(|_| var_gen.fresh());
+ let s = Subst(adt.vars.iter().zip(tvs).map(|(x, t)| (x.clone(), t)).collect());
+ let t = Type::Ctr(adt.name.clone(), adt.vars.iter().cloned().map(Type::Var).collect());
+ let t = t.subst(&s);
+ Ok((s, t))
+}
+
+fn infer_match_cases(
+ mut env: TypeEnv,
+ book: &Book,
+ types: &ProgramTypes,
+ adt: &Adt,
+ arms: &[MatchRule],
+ adt_s: &Subst,
+ var_gen: &mut VarGen,
+) -> Result<(Subst, Type), String> {
+ maybe_grow(|| {
+ if let Some(((ctr_nam, vars, bod), rest)) = arms.split_first() {
+ let ctr = &adt.ctrs[ctr_nam.as_ref().unwrap()];
+ // One fresh var per field, we later unify with the expected type.
+ let tvs = vars.iter().map(|_| var_gen.fresh()).collect::>();
+
+ // Infer the body and unify the inferred field types with the expected.
+ let old_bnd = env.add_binds(vars.iter().zip(tvs.iter().map(|tv| Scheme(vec![], tv.clone()))));
+ let (s1, t1) = infer(&mut env, book, types, bod, var_gen)?;
+ env.pop_binds(old_bnd);
+ let inf_ts = tvs.into_iter().map(|tv| tv.subst(&s1)).collect::>();
+ let exp_ts = ctr.fields.iter().map(|f| f.typ.subst(adt_s)).collect::>();
+ let s2 = unify_fields(inf_ts.iter().zip(exp_ts.iter()), bod)?;
+
+ // Recurse and unify with the other arms.
+ let s = s2.compose(s1);
+ let (s_rest, t_rest) = infer_match_cases(env.subst(&s), book, types, adt, rest, adt_s, var_gen)?;
+ let (t_final, s_final) = unify_term(&t1, &t_rest, bod)?;
+
+ Ok((s_final.compose(s_rest).compose(s), t_final))
+ } else {
+ Ok((Subst::default(), var_gen.fresh()))
+ }
+ })
+}
+
+fn unify_fields<'a>(ts: impl Iterator, ctx: &Term) -> Result {
+ let ss = ts.map(|(inf, exp)| unify_term(inf, exp, ctx)).collect::, _>>()?;
+ let mut s = Subst::default();
+ for (_, s2) in ss.into_iter().rev() {
+ s = s.compose(s2);
+ }
+ Ok(s)
+}
+
+fn unify_term(t1: &Type, t2: &Type, ctx: &Term) -> Result<(Type, Subst), String> {
+ match unify(t1, t2) {
+ Ok((t, s)) => Ok((t, s)),
+ Err(msg) => Err(format!("In {ctx}:\n Can't unify '{t1}' and '{t2}'.{msg}")),
+ }
+}
+
+fn unify(t1: &Type, t2: &Type) -> Result<(Type, Subst), String> {
+ maybe_grow(|| match (t1, t2) {
+ (t, Type::Hole) | (Type::Hole, t) => Ok((t.clone(), Subst::default())),
+ (t, Type::Var(x)) | (Type::Var(x), t) => {
+ // Try to bind variable `x` to `t`
+ if let Type::Var(y) = t {
+ if y == x {
+ // Don't bind a variable to itself
+ return Ok((t.clone(), Subst::default()));
+ }
+ }
+ // Occurs check
+ if t.free_type_vars().contains(x) {
+ return Err(format!(" Variable '{x}' occurs in '{t}'"));
+ }
+ Ok((t.clone(), Subst(BTreeMap::from([(x.clone(), t.clone())]))))
+ }
+ (Type::Arr(l1, r1), Type::Arr(l2, r2)) => {
+ let (t1, s1) = unify(l1, l2)?;
+ let (t2, s2) = unify(&r1.subst(&s1), &r2.subst(&s1))?;
+ Ok((Type::Arr(Box::new(t1), Box::new(t2)), s2.compose(s1)))
+ }
+ (Type::Ctr(name1, ts1), Type::Ctr(name2, ts2)) if name1 == name2 && ts1.len() == ts2.len() => {
+ let mut s = Subst::default();
+ let mut ts = vec![];
+ for (t1, t2) in ts1.iter().zip(ts2.iter()) {
+ let (t, s2) = unify(t1, t2)?;
+ ts.push(t);
+ s = s.compose(s2);
+ }
+ Ok((Type::Ctr(name1.clone(), ts), s))
+ }
+ (Type::Tup(els1), Type::Tup(els2)) if els1.len() == els2.len() => {
+ let mut s = Subst::default();
+ let mut ts = vec![];
+ for (t1, t2) in els1.iter().zip(els2.iter()) {
+ let (t, s2) = unify(t1, t2)?;
+ ts.push(t);
+ s = s.compose(s2);
+ }
+ Ok((Type::Tup(ts), s))
+ }
+ t @ ((Type::U24, Type::U24)
+ | (Type::F24, Type::F24)
+ | (Type::I24, Type::I24)
+ | (Type::None, Type::None)) => Ok((t.0.clone(), Subst::default())),
+ (Type::Number(t1), Type::Number(t2)) => {
+ let (t, s) = unify(t1, t2)?;
+ Ok((Type::Number(Box::new(t)), s))
+ }
+ (Type::Number(tn), Type::Integer(ti)) | (Type::Integer(ti), Type::Number(tn)) => {
+ let (t, s) = unify(ti, tn)?;
+ Ok((Type::Integer(Box::new(t)), s))
+ }
+ (Type::Integer(t1), Type::Integer(t2)) => {
+ let (t, s) = unify(t1, t2)?;
+ Ok((Type::Integer(Box::new(t)), s))
+ }
+ (Type::Number(t1) | Type::Integer(t1), t2 @ (Type::U24 | Type::I24 | Type::F24))
+ | (t2 @ (Type::U24 | Type::I24 | Type::F24), Type::Number(t1) | Type::Integer(t1)) => {
+ let (t, s) = unify(t1, t2)?;
+ Ok((t, s))
+ }
+
+ (Type::Any, t) | (t, Type::Any) => {
+ let mut s = Subst::default();
+ // Recurse to assign variables to `Any` as well
+ for child in t.children() {
+ let (_, s2) = unify(&Type::Any, child)?;
+ s = s2.compose(s);
+ }
+ Ok((Type::Any, s))
+ }
+
+ _ => Err(String::new()),
+ })
+}
+
+/// Specializes the inferred type against the type annotation.
+/// This way, the annotation can be less general than the inferred type.
+///
+/// It also forces inferred 'Any' to the annotated, inferred types to
+/// annotated 'Any' and fills 'Hole' with the inferred type.
+///
+/// Errors if the first type is not a superset of the second type.
+fn specialize(inf: &Type, ann: &Type) -> Result {
+ fn merge_specialization(inf: &Type, exp: &Type, s: &mut Subst) -> Result {
+ maybe_grow(|| match (inf, exp) {
+ // These rules have to come before
+ (t, Type::Hole) => Ok(t.clone()),
+ (Type::Hole, _) => unreachable!("Hole should never appear in the inferred type"),
+
+ (_inf, Type::Any) => Ok(Type::Any),
+ (Type::Any, exp) => Ok(exp.clone()),
+
+ (Type::Var(x), new) => {
+ if let Some(old) = s.0.get(x) {
+ if old == new {
+ Ok(new.clone())
+ } else {
+ Err(format!(" Inferred type variable '{x}' must be both '{old}' and '{new}'"))
+ }
+ } else {
+ s.0.insert(x.clone(), new.clone());
+ Ok(new.clone())
+ }
+ }
+
+ (Type::Arr(l1, r1), Type::Arr(l2, r2)) => {
+ let l = merge_specialization(l1, l2, s)?;
+ let r = merge_specialization(r1, r2, s)?;
+ Ok(Type::Arr(Box::new(l), Box::new(r)))
+ }
+ (Type::Ctr(name1, ts1), Type::Ctr(name2, ts2)) if name1 == name2 && ts1.len() == ts2.len() => {
+ let mut ts = vec![];
+ for (t1, t2) in ts1.iter().zip(ts2.iter()) {
+ let t = merge_specialization(t1, t2, s)?;
+ ts.push(t);
+ }
+ Ok(Type::Ctr(name1.clone(), ts))
+ }
+ (Type::Tup(ts1), Type::Tup(ts2)) if ts1.len() == ts2.len() => {
+ let mut ts = vec![];
+ for (t1, t2) in ts1.iter().zip(ts2.iter()) {
+ let t = merge_specialization(t1, t2, s)?;
+ ts.push(t);
+ }
+ Ok(Type::Tup(ts))
+ }
+ (Type::Number(t1), Type::Number(t2)) => Ok(Type::Number(Box::new(merge_specialization(t1, t2, s)?))),
+ (Type::Integer(t1), Type::Integer(t2)) => Ok(Type::Integer(Box::new(merge_specialization(t1, t2, s)?))),
+ (Type::U24, Type::U24) | (Type::F24, Type::F24) | (Type::I24, Type::I24) | (Type::None, Type::None) => {
+ Ok(inf.clone())
+ }
+ _ => Err(String::new()),
+ })
+ }
+
+ // Refresh the variable names to avoid conflicts when unifying
+ // Names of type vars in the annotation have nothing to do with names in the inferred type.
+ let var_gen = &mut VarGen::default();
+ let inf2 = inf.generalize(&TypeEnv::default()).instantiate(var_gen);
+ let ann2 = ann.generalize(&TypeEnv::default()).instantiate(var_gen);
+
+ let (t, s) = unify(&inf2, &ann2)
+ .map_err(|e| format!("Type Error: Expected function type '{ann}' but found '{inf}'.{e}"))?;
+ let t = t.subst(&s);
+
+ // Merge the inferred specialization with the expected type.
+ // This is done to cast to/from `Any` and `_` types.
+ let mut merge_s = Subst::default();
+ let t2 = merge_specialization(&t, ann, &mut merge_s).map_err(|e| {
+ format!("Type Error: Annotated type '{ann}' is not a subtype of inferred type '{inf2}'.{e}")
+ })?;
+
+ Ok(t2.subst(&merge_s))
+}
+
+impl std::fmt::Display for Subst {
+ fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+ writeln!(f, "Subst {{")?;
+ for (x, y) in &self.0 {
+ writeln!(f, " {x} => {y},")?;
+ }
+ write!(f, "}}")
+ }
+}
diff --git a/src/fun/check/unbound_refs.rs b/src/fun/check/unbound_refs.rs
index 1aa4cd5e5..f78fee9de 100644
--- a/src/fun/check/unbound_refs.rs
+++ b/src/fun/check/unbound_refs.rs
@@ -7,7 +7,6 @@ use std::collections::HashSet;
impl Ctx<'_> {
pub fn check_unbound_refs(&mut self) -> Result<(), Diagnostics> {
- self.info.start_pass();
for def in self.book.defs.values() {
let mut unbounds = HashSet::new();
for rule in def.rules.iter() {
diff --git a/src/fun/check/unbound_vars.rs b/src/fun/check/unbound_vars.rs
index 61b6a36e1..41b744890 100644
--- a/src/fun/check/unbound_vars.rs
+++ b/src/fun/check/unbound_vars.rs
@@ -3,7 +3,7 @@ use crate::{
fun::{transform::desugar_bend, Ctx, Name, Pattern, Term},
maybe_grow,
};
-use std::collections::{hash_map::Entry, HashMap};
+use std::collections::HashMap;
#[derive(Debug, Clone)]
pub enum UnboundVarErr {
@@ -14,16 +14,11 @@ pub enum UnboundVarErr {
impl Ctx<'_> {
/// Checks that there are no unbound variables in all definitions.
pub fn check_unbound_vars(&mut self) -> Result<(), Diagnostics> {
- self.info.start_pass();
-
for (def_name, def) in self.book.defs.iter_mut() {
let mut errs = Vec::new();
for rule in &mut def.rules {
- let mut scope = HashMap::new();
- for pat in &rule.pats {
- pat.binds().for_each(|nam| push_scope(nam.as_ref(), &mut scope));
- }
-
+ // Note: Using a Vec instead of a Map is a deliberate optimization.
+ let mut scope = rule.pats.iter().flat_map(|pat| pat.binds()).map(|x| x.as_ref()).collect::>();
rule.body.check_unbound_vars(&mut scope, &mut errs);
}
@@ -42,7 +37,7 @@ impl Term {
pub fn check_unbound_vars<'a>(
&'a mut self,
- scope: &mut HashMap<&'a Name, u64>,
+ scope: &mut Vec>,
errs: &mut Vec,
) {
let mut globals = HashMap::new();
@@ -59,13 +54,13 @@ impl Term {
/// Globals has how many times a global var name was declared and used.
pub fn check_uses<'a>(
term: &'a mut Term,
- scope: &mut HashMap<&'a Name, u64>,
+ scope: &mut Vec>,
globals: &mut HashMap,
errs: &mut Vec,
) {
maybe_grow(move || match term {
Term::Var { nam } => {
- if !scope.contains_key(nam) {
+ if !scope_contains(nam, scope) {
errs.push(UnboundVarErr::Local(nam.clone()));
*term = Term::Err;
}
@@ -80,11 +75,11 @@ pub fn check_uses<'a>(
}
for (child, binds) in term.children_mut_with_binds() {
for bind in binds.clone() {
- push_scope(bind.as_ref(), scope);
+ scope.push(bind.as_ref());
}
check_uses(child, scope, globals, errs);
- for bind in binds {
- pop_scope(bind.as_ref(), scope);
+ for _ in binds {
+ scope.pop();
}
}
}
@@ -104,20 +99,8 @@ pub fn check_global_binds(pat: &Pattern, globals: &mut HashMap(nam: Option<&'a Name>, scope: &mut HashMap<&'a Name, u64>) {
- if let Some(nam) = nam {
- *scope.entry(nam).or_default() += 1;
- }
-}
-
-fn pop_scope<'a>(nam: Option<&'a Name>, scope: &mut HashMap<&'a Name, u64>) {
- if let Some(nam) = nam {
- let Entry::Occupied(n_declarations) = scope.entry(nam).and_modify(|e| *e -= 1) else { unreachable!() };
-
- if *n_declarations.get() == 0 {
- n_declarations.remove();
- }
- }
+fn scope_contains(nam: &Name, scope: &[Option<&Name>]) -> bool {
+ scope.iter().rev().any(|scope_nam| scope_nam == nam)
}
impl std::fmt::Display for UnboundVarErr {
diff --git a/src/fun/display.rs b/src/fun/display.rs
index ad54a761e..36ee63d88 100644
--- a/src/fun/display.rs
+++ b/src/fun/display.rs
@@ -1,4 +1,4 @@
-use super::{Book, Definition, FanKind, Name, Num, Op, Pattern, Rule, Tag, Term};
+use super::{Book, Definition, FanKind, Name, Num, Op, Pattern, Rule, Tag, Term, Type};
use crate::maybe_grow;
use std::{fmt, ops::Deref, sync::atomic::AtomicU64};
@@ -222,6 +222,7 @@ impl Rule {
impl fmt::Display for Definition {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
namegen_reset();
+ writeln!(f, "{}{}: {}", if !self.check { "unchecked " } else { "" }, self.name, self.typ)?;
write!(f, "{}", DisplayJoin(|| self.rules.iter().map(|x| x.display(&self.name)), "\n"))
}
}
@@ -273,8 +274,6 @@ impl fmt::Display for Op {
Op::POW => write!(f, "**"),
Op::SHR => write!(f, ">>"),
Op::SHL => write!(f, "<<"),
- Op::LOG => todo!(),
- Op::ATN => todo!(),
Op::LE => write!(f, "<="),
Op::GE => write!(f, ">="),
}
@@ -292,6 +291,44 @@ impl Tag {
}
}
+impl fmt::Display for Type {
+ fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+ maybe_grow(|| match self {
+ Type::Hole => write!(f, "_"),
+ Type::Var(nam) => write!(f, "{nam}"),
+ Type::Arr(lft, rgt) => write!(f, "({} -> {})", lft, rgt.display_arrow()),
+ Type::Ctr(nam, args) => {
+ if args.is_empty() {
+ write!(f, "{nam}")
+ } else {
+ write!(f, "({nam} {})", DisplayJoin(|| args.iter(), " "))
+ }
+ }
+ Type::Number(t) => write!(f, "(Number {t})"),
+ Type::Integer(t) => write!(f, "(Integer {t})"),
+ Type::U24 => write!(f, "u24"),
+ Type::I24 => write!(f, "i24"),
+ Type::F24 => write!(f, "f24"),
+ Type::Any => write!(f, "Any"),
+ Type::None => write!(f, "None"),
+ Type::Tup(els) => write!(f, "({})", DisplayJoin(|| els.iter(), ", ")),
+ })
+ }
+}
+
+impl Type {
+ pub fn display_arrow(&self) -> impl fmt::Display + '_ {
+ maybe_grow(|| {
+ DisplayFn(move |f| match self {
+ Type::Arr(lft, rgt) => {
+ write!(f, "{} -> {}", lft, rgt.display_arrow())
+ }
+ _ => write!(f, "{}", self),
+ })
+ })
+ }
+}
+
fn var_as_str(nam: &Option) -> &str {
nam.as_ref().map_or("*", Name::deref)
}
diff --git a/src/fun/load_book.rs b/src/fun/load_book.rs
index a88c45097..1f084c591 100644
--- a/src/fun/load_book.rs
+++ b/src/fun/load_book.rs
@@ -1,5 +1,5 @@
use super::{
- parser::{ParseBook, TermParser},
+ parser::{FunParser, ParseBook},
Book, Name, Source, SourceKind,
};
use crate::{
@@ -41,7 +41,7 @@ pub fn load_to_book(
pub fn do_parse_book(code: &str, origin: &Path, mut book: ParseBook) -> Result {
book.source = Name::new(origin.to_string_lossy());
- TermParser::new(code).parse_book(book, false).map_err(|err| {
+ FunParser::new(book.source.clone(), code, false).parse_book(book).map_err(|err| {
let mut diagnostics = Diagnostics::default();
let span = TextSpan::from_byte_span(code, err.span.0..err.span.1);
let source =
@@ -50,7 +50,3 @@ pub fn do_parse_book(code: &str, origin: &Path, mut book: ParseBook) -> Result