google / google/xls

DSLX: add an `unimplemented` expression that always typechecks

Open
#218 2 comments 0 reactions 0 assignees View on GitHub
dslx long-term-enhancement
Dominant language
C++
Stars
1.9k
Forks
283
Avg merge
2d 10h
Merged PRs (30d)
135

Description

Please add something like Haskell's `error` [(docs)](https://www.stackage.org/haddock/lts-16.23/base-4.13.0.0/Prelude.html#v:error) and Rust's `unimplemented` ([docs](https://doc.rust-lang.org/std/macro.unimplemented.html)).

Below, let's call DSLX's version `unimplemented` for brevity and clarity. Bikeshedding about the name is out of scope in this comment.

#### Why is it useful, what does it do?

It enables the developer to write code gradually, with the code at any given point successfully type checking, because all incomplete portions of the program can be replaced by `unimplemented`. This allows the developer to use the type checker at all phases of program development, not just when a (more or less) complete program is typed in.

For (a very silly) example, let's pretend that we don't yet know how to compute `four`, but we know that we'll need it (for brevity let's also assume that the compiler's HM type inference is completed). We can write this program and ensure that it typechecks (fixing any type checker errors), before moving on to computing `four`, or perhaps moving on to some other part of our program and returning to `four` later.

```
fn seven() -> u32 {
let three = 1 + 2;
let four = unimplemented
three + four
}
```

More examples:

```
fn eight() -> u32 {
unimplemented
}
```

```
struct Foo {...}
struct Bar {...}

fn stuff(foo : Foo) -> Bar {
unimplemented
}
fn more_stuff(foo : Foo) -> Bar {
stuff(unimplemented)
}
```

This program should interpret just fine. I.e. whenever `three` is called it should return `3`.

```
fn three() -> u32 {
3 if true else unimplemented
}
```

#### Key wants

* `unimplemented` should be an expression that always type checks, i.e. the expression is polymorphic and fits whatever type hole it needs to.
* The interpreter should be able to run normally, until an expression with `unimplemented` is actually evaluated. See the last example above, the `three` function.

#### Other semantics

* `unimplemented` should cause immediate failure of synthesis (at least, I can't see any reason it should do otherwise)

#### Open questions

Should the user be able to supply a custom error message? Should the compiler automatically make one, similar to how trace operates today, that includes a snippet of the surrounding code and the line and column numbers?

Contributor guide

Open the contributing guide

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.