4 ms·

I’m really excited about dependent types. I’m expecting we won’t get them for a while though. Dependent Haskell is progressing but apparently it’s hard to retro

I’m really excited about dependent types. I’m expecting we won’t get them for a while though. Dependent Haskell is progressing but apparently it’s hard to retrofit. Idris’ own creator has said he expects it to be a model for other languages, I don’t think it will ever have mainstream adoption. Coq and Agda, F* aren’t really designed to be general purpose. Although the implementation for the compiler is complex, and the syntax can get complex and verbose, to me my requirement is simple: I want to encode everything about input and output that I know. Right now in mainstream languages I often know more about my arguments or output than the type system will allow me to specify.

valyagolev 3y ago
I totally share your excitement about dependent types, but it seems that, unlike the type systems we're used to, theorems about the dependent types are much harder to prove, which makes them not very comfortable to use for the whole program. If only there was some kind of a gradual, perhaps typescript-like approach to adding arbitrary type-level value-limiting information in random places without having to have everything proven everywhere...
- skulk 3y ago
  Every non-dependent typing relation is also a dependently typed relation so I think things are already the way you want, unless you have a certain example in mind.
  - valyagolev 3y ago
    Sure, in the same sense that every "untyped" program is already typed with some kind of a universal type, but what's the point? What I want is to be able to specify and have (when possible) automatically proven arbitrary assertions anywhere in the code without necessarily making sure that every possible presupposition is proven from the ground up. Just like in Typescript, I can add a type at any point where there was only "any", and have a small portion of the program typed without typing the whole thing
    - skulk 3y ago
      > What I want is to be able to specify and have (when possible) automatically proven arbitrary assertions anywhere in the code This doesn't even exist in TypeScript. If I change function foo(a: any) { return baz(a); } to function foo(a: number) { return baz(a); } whoever calls foo has to still prove (or assert) that the argument is a number. Is that what you're after, asserting a dependent type? For example being able to change: function divByTwo(a: number): number { return a/2; } to function divByTwo(a: even_number): number { return a/2; } You want every place divByTwo is called to also automatically supply a proof that the argument is even?
      - valyagolev 3y ago
        i don't even need it to go beyond the insides of a function. something like a proof of an invariant that's only relevant inside the function's body would be fine. e.g. in Rust, almost every place where you see something like ".unwrap()" with "// unwrap safety:" comment, this comment could be an assertion easily proven from the few lines above
    - dunham 3y ago
      Not sure if it's what you're asking for, but in lean, you can put `sorry` to skip a proof. It's `believe_me` in Idris2, and I think the Agda version is `trustMe`. You can also use stuff like ! when you don't want to prove your array indices (it might crash or substitute a dummy value if you're wrong).
      - deleted 3y ago
        [deleted]
mettamage 3y ago
Eli5 dependent types? Chatgpt: Dependent types are a concept in computer science and programming languages where the type of a variable can depend on the value of another variable. In simpler terms, imagine you have a list of numbers and you also have information about how long that list is. With dependent types, you could create a type for the list that explicitly includes its length, ensuring at compile time that operations respect this length. This makes it possible to catch certain kinds of errors before the code even runs. For example, in a language with dependent types, you could specify a function to take a list of length 3 and no other sizes. If you tried to pass a list of length 4, the program wouldn't compile, preventing this kind of mistake early on. It's a bit like having an extra layer of safety checks, where the types are more expressive and can encode more intricate relationships between variables.
- turndown 3y ago
  It’s simplest explanation is that dependent types are types whose exact type use some kind of parameterized value in the definition. So a dependently typed array would use a parameterized length value as part of it’s definition(this is usually the easiest example to understand). So an array of length 4(of whatever type) could be identified as different from an array of length 5, etc.
- icen 3y ago
  Another classic use case is that you can have expressions in the types of your function, for example this won't compile: stringOrInt : (x : boolean) -> int -> (if x then String else int) stringOrInt true x = toString x stringOrInt false x = x + 1 1 + stringOrInt true 37 # this will error, because it knows you've not returned an int The other example that you can do in depedently typed languages, but is too involved to write out here, is make a type-safe printf, where the format string produces the types for the other arguments.
- howenterprisey 3y ago
  I never care much for chatgpt answers. I don't know why people post them on here. In the first sentence, "another" is wrong because you don't need two variables, you just need one. Final paragraph's wrong for the same reason. The example given is poor given that I can write [i8; 3] or int[3] in Rust or C and those very much do not have "dependent types" in the popular sense (Rust's const generics excepted). To be fair, those examples are technically dependent types, but it would be better to give an example that's impossible in those languages, such as "array with length at most 3" or "even integer". Finally, to nitpick, "a bit like" is unneeded hedging. Stack Overflow did a much better job: https://stackoverflow.com/questions/9338709/what-is-dependent-typing https://stackoverflow.com/questions/9338709/what-is-dependen.... Wikipedia's article is pretty bad and maybe I'll get around to fixing it at some point.

valyagolev 3y ago

I totally share your excitement about dependent types, but it seems that, unlike the type systems we're used to, theorems about the dependent types are much harder to prove, which makes them not very comfortable to use for the whole program. If only there was some kind of a gradual, perhaps typescript-like approach to adding arbitrary type-level value-limiting information in random places without having to have everything proven everywhere...

skulk 3y ago
Every non-dependent typing relation is also a dependently typed relation so I think things are already the way you want, unless you have a certain example in mind.
- valyagolev 3y ago
  Sure, in the same sense that every "untyped" program is already typed with some kind of a universal type, but what's the point? What I want is to be able to specify and have (when possible) automatically proven arbitrary assertions anywhere in the code without necessarily making sure that every possible presupposition is proven from the ground up. Just like in Typescript, I can add a type at any point where there was only "any", and have a small portion of the program typed without typing the whole thing
  - skulk 3y ago
    > What I want is to be able to specify and have (when possible) automatically proven arbitrary assertions anywhere in the code This doesn't even exist in TypeScript. If I change function foo(a: any) { return baz(a); } to function foo(a: number) { return baz(a); } whoever calls foo has to still prove (or assert) that the argument is a number. Is that what you're after, asserting a dependent type? For example being able to change: function divByTwo(a: number): number { return a/2; } to function divByTwo(a: even_number): number { return a/2; } You want every place divByTwo is called to also automatically supply a proof that the argument is even?
    - valyagolev 3y ago
      i don't even need it to go beyond the insides of a function. something like a proof of an invariant that's only relevant inside the function's body would be fine. e.g. in Rust, almost every place where you see something like ".unwrap()" with "// unwrap safety:" comment, this comment could be an assertion easily proven from the few lines above
  - dunham 3y ago
    Not sure if it's what you're asking for, but in lean, you can put `sorry` to skip a proof. It's `believe_me` in Idris2, and I think the Agda version is `trustMe`. You can also use stuff like ! when you don't want to prove your array indices (it might crash or substitute a dummy value if you're wrong).
    - deleted 3y ago
      [deleted]

mettamage 3y ago

Eli5 dependent types? Chatgpt: Dependent types are a concept in computer science and programming languages where the type of a variable can depend on the value of another variable. In simpler terms, imagine you have a list of numbers and you also have information about how long that list is. With dependent types, you could create a type for the list that explicitly includes its length, ensuring at compile time that operations respect this length. This makes it possible to catch certain kinds of errors before the code even runs. For example, in a language with dependent types, you could specify a function to take a list of length 3 and no other sizes. If you tried to pass a list of length 4, the program wouldn't compile, preventing this kind of mistake early on. It's a bit like having an extra layer of safety checks, where the types are more expressive and can encode more intricate relationships between variables.

turndown 3y ago
It’s simplest explanation is that dependent types are types whose exact type use some kind of parameterized value in the definition. So a dependently typed array would use a parameterized length value as part of it’s definition(this is usually the easiest example to understand). So an array of length 4(of whatever type) could be identified as different from an array of length 5, etc.
icen 3y ago
Another classic use case is that you can have expressions in the types of your function, for example this won't compile: stringOrInt : (x : boolean) -> int -> (if x then String else int) stringOrInt true x = toString x stringOrInt false x = x + 1 1 + stringOrInt true 37 # this will error, because it knows you've not returned an int The other example that you can do in depedently typed languages, but is too involved to write out here, is make a type-safe printf, where the format string produces the types for the other arguments.
howenterprisey 3y ago
I never care much for chatgpt answers. I don't know why people post them on here. In the first sentence, "another" is wrong because you don't need two variables, you just need one. Final paragraph's wrong for the same reason. The example given is poor given that I can write [i8; 3] or int[3] in Rust or C and those very much do not have "dependent types" in the popular sense (Rust's const generics excepted). To be fair, those examples are technically dependent types, but it would be better to give an example that's impossible in those languages, such as "array with length at most 3" or "even integer". Finally, to nitpick, "a bit like" is unneeded hedging. Stack Overflow did a much better job: https://stackoverflow.com/questions/9338709/what-is-dependent-typing https://stackoverflow.com/questions/9338709/what-is-dependen.... Wikipedia's article is pretty bad and maybe I'll get around to fixing it at some point.