Scythe

A prototype for a dependently typed programming language; my undergrad honours project.

(Note: this page is under construction. For some more in-depth writing on the topic, you can find the paper I wrote for my project here.)

What is a Dependent Type?

A dependent type, put simply, is a type that depends on a value. There are many kinds of dependent types, such as GADTs, but consider the following function f:

$$\func{(b\is \type{Bool})}{\ifthenelse{b}{5}{\str{hi}}}$$

In What Kinds of Languages Does This Typecheck?

Well, in a dynamically-typed language, there is no "typechecking" in the way that there is for statically typed languages, so you can do stuff like this to your heart's content.

That said, in these languages, there's nothing stopping you from using this function in a place where it'd throw a runtime error, so you'll never really sleep at night without thinking of that Boeing plane you worked on.

In your average statically-typed language, this would throw a type error. That's because all functions for these languages are of the form $$\ftype{A}{B},$$and what could (B) possibly be?

If (B: Nat), then ("hi") doesn't typecheck, and if (B: Str), then (5) doesnt typecheck. They are terms with different types, so this shouldn't typecheck.

But in a dependently-typed language (or, at least the one that I was working on with general dependent types), you could have it so that the type of this function is$$f\is (\ftype{(b\is \Bool)}{\ifthenelse{b}{\Nat}{\Str}}).$$That is, (f)'s return type changes depending on what the value given to (f) is.

What Can We Do With This?

For this to be useful, a couple of things need to be true.

If I write (f(true)), the compiler needs to figure out that the type of this term is (Nat).
If I write (f(false)), it needs to know its type is (Str).
If I write (f(c)) for some variable (c), the type should stay (if b then Nat else Str).

How can we do this? Well, we can evaluate (f)'s type during the typechecking process! We can first evaluate (c) as an expression, and then we can substitute that value in for (b) to get (if c then Nat else Str), and evaluate that! If c is true or false, the type will collapse to either (Nat) or (Str)!

The Implications of Dependent Types

The implication of this is that Scythe has arbitrary compile-time execution, which is generally considered bad.

But would you rather have an infinite loop that never terminates in your compiler, OR an infinite loop on that Boeing plane? Sure, it's not ideal, but if this level of type-expressivity is able to guarantee more correctness, I'd argue it's a feature and not a bug.

However, having a type of types has another issue: you can't erase types by the end of compilation. If a function can return a type, and the type it can return could be the type of types itself, then it's necessary that types have to be available at runtime. And, truth be told, that sucks.

If I was to do this project again, I'd probably do an ATS-style two-level type theory.