Dependent types and how to get rid of them

I wrote a small post on that: https://azdavis.net/posts/lambda-cube/

Hope it’s helpful!

I'm not familiar with Zig, but I'm pretty sure comptime is not quite as powerful.

In the post, I didn't give any examples of situations where the input to a dependent function was not known at compile time. However, that was just due to the lack of time when writing the post.

I gave this example:

    useValue : Bool -> String
    useValue True = "The number is: " ++ natToString (getValue True)
    useValue False = "The message is: " ++ getValue False

The difference is that nothing in dependent types requires that the depended-on value `b` is known at compile time. You could pass any Bool to `getValue`, including one that was read as input from the user. It would just be the case that, before using the value returned by `getValue b`, you'd have to check (at runtime) the value of `b`. Only then would you know `pickType b`, which would tell you the type of `getValue b`. My apologies that the post was unclear about this. (I've just updated it.)

Yes, the compiler contains an interpreter for the entire language, not just a subset. It is circular as you rightly point out, but there's no contradiction here.

Typically the interpreter limits itself to only evaluating pure functions or functions that do not perform any kind of IO, but in principle this restriction is not necessary. For example Jai's compiler allows completely arbitrary execution at compile time including even downloading arbitrary data from the Internet and using that data to make decisions about how to compile code.

In type theory, all singleton types are isomorphic and have no useful distinguishing characteristics (indeed, this is true of all types of the same cardinality – and even then, comparing cardinalities is always undecidable and thus irrelevant at runtime). So your Nine type doesn’t really make sense, because you may as well just write Unit. In general, there is no amount of introspection into the “internal structure” of a type offered; even though parametricity does not hold in general (unless you postulate anticlassical axioms), all your functions that can run at runtime are required to be parametric.

In the style of the linked post, you'd probably define a generic type (well, one of two generic types):

type ExactlyStatic : (0 t: Type) -> (0 v: t) -> Type

type ExactlyRuntime : (0 t: Type) -> (v: t) -> Type

Then you could have the type (ExactlyStatic Int 9) or the type (ExactlyRuntime Int 9).

The difference is that ExactlyStatic Int 9 doesn't expose the value 9 to the runtime, so it would be fully erased, while (ExactlyRuntime Int 9) does.

This means that the runtime representation of the first would be (), and the second would be Int.

> Also how to handle runtime values? That will require type assertions, just like union types?

The compiler doesn't insert any kind of runtime checks that you aren't writing in your code. The difference is that now when you write e.g. `if condition(x) then ABC else DEF` inside of the two expressions, you can obtain a proof that condition(x) is true/false, and propagate this.

Value representations will typically be algebraic-data-type flavored (so, often a tagged union) but you can use erasure to get more efficient representations if needed.

Hi aatd86! We had a different thread about existence a couple days ago, and I'm just curious -- is English your second language? What's your first language? I'm guessing French, or something from Central Europe.

Thanks for humoring me!

Functions that return types are indeed at a higher level than those that don't.

Values can be seen as Singleton types. The key difference is the universe they live in. In the universe of types, the level one level below is perceived as a value. Similarly, in the universe of kinds, types appear to be values.

> Basically, 'value' would be a special constraint on a type parameter in normal parametric polymorphism implementations

Yes this is a level constraint.

> But I guess, the same issue of "which refinement types can be defined, while keeping everything decidable" remains as an issue.

If you're dealing with fully computable types. Nothing is decidable.

> Also how to handle runtime values? That will require type assertions, just like union types? Or is it only a compile time concept and there is no runtime instantiations. Only some kind of const generics?

A compiler with dependent types is essentially producing programs that are itself embedded with its input. There cannot be a distinction between runtime and compel time. Because in general type checking requires you to be able to run a program. The compilation essentially becomes deciding which parts you want to evaluate and which parts you want to defer until later.

> A typeof function could be an example of dependent type though? Even at runtime?

Typeof is just const.

Typeof: (T : type) -> (x:T) -> Type

Final note: I've written some compilers for toy dependently typed languages. By far dependent typing makes both the language and the compiler easier not harder. This is because Haskell and c++ and other languages with type systems and metaprogramming or generics actually have several languages: the value language that we are familiar with, but also the type language.

In Haskell, this is the class/instance language which is another logic programming language atop the lambda calculus language. This means to write a Haskell compiler you have to write a compiler for Haskell and the logic programming language (which is turing complete btw) that is the type language

Similarly in c++, you have to implement c++ AND the template system which is a functional programming language with incredibly confusing semantics.

On the other hand for a dependently typed language, you just write one language... The types are talked about in the same way as values. The only difficulty is type inference. However, an explicit dependently typed language is actually the easiest typed compiler to write because it's literally just checking for term equality which is very easy! On the other hand with a dependent language, type inference is never going to be perfect so you're a lot freer to make your own heuristic decisions and forego HM-like perfection.

Yes. You can give pickType a type in TS. Something like pickType<B extends boolean>(b: B): B extends true ? string : number.

I’d love to read a post explaining how TS conditional types are or are not a form of dependent types. Or, I’d like to understand dependent types well enough to write that post.

GADTs let you do similar things in the simplest cases, they just don't work as well for complex constraints.

Like, append: Vector n t -> Vector m t -> Vector (n+m) t. With GADTs you need to manually lift (+) to work on the types, and then provide proofs that it's compatible with the value-level.

Then you often need singletons for the cases that are more complex- if I have a set of integers, and an int x, and I want to constrain that the item is in the set and is also even, the GADT approach looks like:

doThing :: Singleton Int x -> Singleton (Set Int) s -> IsInSet x s -> IsEven x -> SomeOutput

Which looks reasonable, until you remember that the Singleton type has to have a representation which is convenient to prove things about, not a representation that is convenient/efficient to operate on, which means your proofs will be annoying or your function itself will hardly resemble a "naive" untyped implementation.

Dependent types fix this because your values are "just" values, so it would be something like

doThing :: (x : int) -> (s : set int) -> so (is_in s x) -> so (even x) -> SomeOutput

Here, x and s are just plain values, not a weird wrapper, and is_in and event are ordinary (and arbitrary) library functions.

I mean, you can trivially do it with a (non-G) ADT, if you're content with wrapping the return value.

OTOH you can do this in TypeScript easily without wrapping; it could return a union type `number | string`.

I think it's a bit apples and oranges. I was suggesting that compilation itself should probably not involve nondeterministic network requests. If I understand LSP correctly, it only uses network requests to allow your editor to communicate with a binary that provides type information. But the compiler behavior is unchanged. Honestly LSPs seem pretty reasonable to me.

No, LSPs return the name/metadata of a concrete type. Dependent typing means that the return type of any given function in your (static) program can depend on a runtime value, e.g. user input... In well-defined ways ofc.