7 ms·

Dependent types and how to get rid of them

• nixpulvis 1y ago
  I read the first post and thought someone should at the very least post the lambda cube. This isn't my area of expertise, since I've done very little with dependent types (staying firmly on the left side of the cube), but it outlines some useful categories of type systems here. https://en.wikipedia.org/wiki/Lambda_cube https://en.wikipedia.org/wiki/Lambda_cube
  • azdavis 1y ago
    I wrote a small post on that: https://azdavis.net/posts/lambda-cube/ https://azdavis.net/posts/lambda-cube/ Hope it’s helpful!
    • nixpulvis 1y ago
      Cool that you worked on an implementation of the CoC. I've been somewhat wanting to go back and revisit ATAPL and read chapter 2 on this subject: https://www.cis.upenn.edu/~bcpierce/attapl/frontmatter.pdf https://www.cis.upenn.edu/~bcpierce/attapl/frontmatter.pdf
    • ChadNauseam 1y ago
      That is a good post. I've linked to it from mine!
      • azdavis 1y ago
        Thanks! But I don’t think it quite worked?
        • ChadNauseam 1y ago
          Ought to be fixed now
• aatd86 1y ago
  I am slowly trying to understand dependent types but the explanation is a bit confusing to me as, I understand the mathematical terminology of a function that may return a type, but... Since function types take a value and return a value, they are by definition in another universe from say morphisms that would take a type and return a type. The same way, I see a value as a ur-element and types as sets of values. So even if there is syntactic sugar around the value <-> type equivalence, I'd naively think that we could instead define some type morphism and that might be more accurate. The value parameter would merely be declared through a type parameter constrained to be a singleton. The same way a ur-element is not a set but a member of set. Then the question is representation but that could be left as an optimization. Perhaps that it is already what is done. Example: type Nine int = {9} And then the rest is generic functions, parameterizable by 9, or actually, Nine. So nothing too different from a refinement of int. Basically, 'value' would be a special constraint on a type parameter in normal parametric polymorphism implementations. There would probably be derived constraint information such as size etc... But I guess, the same issue of "which refinement types can be defined, while keeping everything decidable" remains as an issue. 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 typeof function could be an example of dependent type though? Even at runtime? Just wondering...
  • pinkmuffinere 1y ago
    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!
  • anon291 1y ago
    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.
• jesse__ 1y ago
  Off the topic of dependent types, but this is way too hilarious to pass up.. > Imagine if pickType did a network request to a server and then returned whatever type the server said. Sounds like a bad idea! Fucking .. isn't this what LSPs are?! Finally something functional programming people and I can agree on. That does sound like a bad idea.
  • ChadNauseam 1y ago
    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.
    • jesse__ 1y ago
      What's the fundamental difference between a syntax highlighter and the frontend of a compiler? I would argue not much, apart from the fact that people are willing to have their syntax highlighter randomly explode, but are much more concerned about their compiler randomly exploding.
      • hyghjiyhu 1y ago
        The fundamental difference is that in his case any conforming compiler has to do the network request. Whereas with LSP it's just an implementation detail of the editor.
        • jesse__ 1y ago
          My point is "why do we tolerate network requests in LSPs, but not compiler frontends"? If you think about it, the LSP is a way of doing libraries, which is dramatically worse than just inventing a binary interface and doing actual dynamic libraries. If you follow the LSP model to it's natural conclusion, everything becomes this horrible, disconnected morass of servers talking to each other on your local machine..
• walterburns 1y ago
  "But we'd like to give a type to this function. In most languages (Haskell, Typescript, C++, Rust, C#, etc.) there is no way to do that.[2] " Can't you do this with a GADT? With a GADT, the type of the output can be specified by which branch of the GADT the input matches. Seems quite a similar idea.
  • wk_end 1y ago
    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`.
    • codebje 1y ago
      Isn't that just saying you can do dependent types in TypeScript easily so long as you're willing to give up type checking?
      • mpoteat 1y ago
        Actually, it's even simpler: you should just be able to use signature overloading: myFunc(x: true): number myFunc(x: false): string The article's assertion that TypeScript can't represent this is quite false.
        • codebje 11mo ago
          Alas, no: foo.ts:1:10 - error TS2393: Duplicate function implementation.
          • wk_end 11mo ago
            Like this: https://www.typescriptlang.org/play/?#code/GYVwdgxgLglg9mABAWwJ4DFwQBQA8BciUATiAKYCUhYIyARmcQNwBQoksCKGWehwAQwA2AZ0qERJGGADmrdtHhI0mSH0R04cIWQFgqiGvUaIAPoknFpMxAG8WiR4hjBEeCnYdPvxMlBDESAAsAEys3gC+iGSiZJ7ePn4BSABEABIxQnAp4U4RLPlsWJxIIGIAasLk6prauvrxTi5uuB72CU6+-oGIKQAqABZxRgzERDDIZCJEAO5whCmIANRuKrytiABUiCEUuY5RMWKNHV3JvYNxkyIiAjJxMCILy9yqOK37iPn5QA https://www.typescriptlang.org/play/?#code/GYVwdgxgLglg9mABA... It's a bit of a hack, though - if you incorrectly implement myFunc so that, say, it returns a string even when x is true, it can violate the overloading assertions without any error or warning.
• dcre 1y ago
  This made me realize TypeScript’s conditional types are closer to dependent types than I thought.
  • danvk 1y ago
    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.
    • dcre 11mo ago
      I asked GPT-5 about it before writing the above comment and got a pretty interesting answer about how, for example, you can’t write a function that takes a number as an argument and returns an array of that length (length enforced by the type system). You can partly get there with tuple types but you have to enumerate every length explicitly. And it only works if you pass a number literal to the function. If you pass a variable of type number, it can’t infer the particular number it is.
    • morcus 11mo ago
      I just tried this, and I couldn't quite get it to work. ``` type PickType<B extends Boolean> = B extends true ? number ? string; function foo<T extends Boolean>(t: T): PickType<T> { return t ? 42 : "42; } ``` The compiler doesn't seem to get that the type of T is narrowed in the ternary branches, and thus Pick<T> is determined. The error I get is that a number isn't assignable to a Pick<T>.
• munchler 1y ago
  > Instead of writing the type directly, we're calling pickType and using the type returned. The typechecker evaluates pickType True at compile time, sees it equals Nat, and then it knows you're saying myNat has type Nat. But how does the compiler evaluate `pickType True` at compile time? Does the typechecker contain an interpreter for (some subset of) the language? It seems potentially circular for a compiler to invoke functions defined in the code that it's compiling.
  • Maxatar 1y ago
    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.
    • munchler 1y ago
      Thank you for the explanation. This reminds me somewhat of an F# type provider, which can execute arbitrary code at compile time. https://learn.microsoft.com/en-us/dotnet/fsharp/tutorials/type-providers/ https://learn.microsoft.com/en-us/dotnet/fsharp/tutorials/ty...
  • jibal 1y ago
    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).
• andyferris 1y ago
  I see we need to add special syntax to the signature for dependent type variables. If you take Zig, it's `comptime` parameters are kind of similar. They can be used to create functions that return types or whose output type depends on the inputs, etc. It seems to fulfil the three axioms at the start, no? The erasure stuff seems just as relavant. Can I say that `comptime` is dependent types in imperative clothing? Or is there a missing capability making it strictly weaker?
  • ChadNauseam 1y ago
    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.)
    • spockz 1y ago
      If you don’t know at compile time what the type of the value is that is returned, how do you know whether the remainder of the expression is still correct? The choice is either to have a total function that will be able to deal with every type and check at compile time whether they exist or to defer to the runtime and then throw an exception if the program doesn’t know what to do with the value.
      • ChadNauseam 1y ago
        The value returned by `getValue b` has type `pickType b`. It cannot be used in a way that depends on its type until you check the value of `b`. If `b = True`, then you know that `pickType b = pickType True = Nat` and that therefore `getValue b` has type `Nat`. There is no option to check the type of a value at runtime. You simply cannot use it in such a way as to create a runtime type error. (This is what it means for the types to be erased. The runtime doesn't know what type it's supposed to be!)
• nialv7 1y ago
  Saying dependent types can be erased is like saying math only contains tautologies. Both are _technically_ true.
• scrubs 1y ago
  Well written! I learned stuff. Dependent types was new on me. Cheers.