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!

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.

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.

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.

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.

This is easily the stupidest thing I've read on HN in quite a while, and your continued arrogance in the rest of the thread doesn't help. Quite an achievement for a site so full of people who have a direct line from their ass to the comment section. Congratulations!

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`.

  myFunc(x: true): number
  myFunc(x: false): string

    foo.ts:1:10 - error TS2393: Duplicate function implementation.

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.

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.

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.

The compilers for Zig, D, Nim, and perhaps other languages contain an interpreter for the whole language that can run at compile time. It's not circular--compiling code and executing code are two quite different things (the interpreter does not contain yet another parser--it works on the AST). You simply can do calculations the results of which can be used in compile-time only contexts such as initializers. The trick in Zig is that the compile-time interpreter supports types as first-class objects, so you can compute types and implement generics this way. In Nim, the interpreter supports computations over the AST. In D, types can be passed as generic arguments, and computed strings can be "mixed in" to the source code and compiled at that point (on-the-fly code generation).

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.)

  getValue : (b : Bool) -> pickType b
  getValue True  = 42
  getValue False = "hello"

  someBool = flipACoinToGetABool
  thingy = getValue someBool

  thingy: (pickType someBool) = getValue someBool

  print (thingy + 3) -- thingy can be an int right?

   print ((if someBool then thingy else 5) + 3)

    const std = @import("std");
    
    fn get_value(comptime b: bool) if (b) u32 else []const u8 {
        if (b) return 12
        else return "string";
    }
    
    fn do_thing(b: bool) void {
        switch (b) {
            inline true => |known_b| std.log.info("{d}", .{get_value(known_b)}),
            inline false => |known_b| std.log.info("{s}", .{get_value(known_b)}),
        }
    }
    
    pub fn main() void {
        do_thing(true);
        do_thing(false);
    }

    fn pick_type(comptime b: bool) type {
        if (b) return u32 else return []const u8;
    }

    fn get_value(comptime b: bool) pick_type(b)

    fn do_thing(b: bool) void {
        inline for (0..2) |i| { // go through all bool variants
            const known_b = (i != 0);
            
            if (known_b == b) {
                // Essentially what we have now is a known_b which is proven
                // at compile-time to be equal to whatever runtime b we have.
                // So we're free to do any kind of dependent type things we'd like
                // with this value.
                
                const value = get_value(known_b);
                // Here we know the type of value but it still depends on the runtime b.
                
                if (known_b) std.log.info("{d}", .{value}) // treated as an int
                else std.log.info("{s}", .{value}); // treated as a string
                
                // We can also just decide based on the type of value at this point.
                if (@TypeOf(value) == u32) ... else ...;
                // Or, a switch
                switch (@TypeOf(value)) {
                    u32 => ...,
                    []const u8 => ...,
                }
            }
        }
    }

You could probably say that. AFAIK there isn't a single valid definition of a dependently typed language any more than there is a single valid definition of a functional language.

I usually go with "you can make a dependent pair", which is two terms where the type of the second depends on the value of the first; I think you could do that in Zig with a bit of handwaving around whether the comptime expression really is the first value or not.

What Zig's doing is also, as best I understand it all, the only real path to anything like dependent types in imperative languages: make a separate sub-language for constant expressions that has its own evaluation rules that run at compile time. See also C++ constexpr, or the constants permitted in a Rust static array size parameter (practically a dependent type itself!)

A functional language's basic building block is an expression and terms are built out of composed expressions; normalisation means reducing a term as far as possible, and equality is (handwaving!) when two terms reduce to exactly the same thing. So you can do your dependent terms in the usual source language with the usual evaluation rules, and those terms are freely usable at runtime or compile time, it's all the same code.

An imperative language's basic building block is a memory peek or poke, with programs composed of sequences of peeks and pokes scheduled by control flow operators. It's much less clear what "normalisation" looks like here, so imperative languages need that separate constant-value embedded language.

Not really. With dependent types, you can have a function that returns a type that depends on a runtime value; with Zig's comptime, it can only depend on a compile-time value.

Note that a language with dependent types doesn't actually "generate" types at runtime (as Zig does at compile-time). It's really about managing proofs that certain runtime objects are instances of certain types. E.g. you could have a "prime number" type, and functions that compute integers would need to include a proof that their result is a prime number if they want to return an instance of the prime number type.

Using dependent types well can be a lot of work in practice. You basically need to write correctness proofs of arbitrary properties.