4 ms·

> I don't expect dependent types or logic programming to become widely-used in the next couple generations of mainstream languages I do, these are low hanging

> I don't expect dependent types or logic programming to become widely-used in the next couple generations of mainstream languages I do, these are low hanging fruits for improving software engineering practices.

ekidd 4y ago
Here's my reasoning on why dependent types may still be a couple of language generations from the mainstream: - Dependent types are hard to retrofit onto an existing language. (Retrofitting generics has had very mixed results, and dependent types are likely harder to retrofit?) - It takes a good 10 years for a new language to really hit the mainstream, even if everything goes right. (This could change if a big player pushes a language.) - All type systems represent a tradeoff, "Roughly how much extra confidence can I get in this program, and for how little extra time spent learning and coding?" Dependent types give you some very interesting new guarantees, but they require picking up new skills. But a future language in this space might make these tradeoffs more appealing! - I'm not sure that any of the existing dependently-typed languages have hit the magic combination of features and tools that would be needed to break out. In the nearer term, I can imagine dependent typing showing up in at least two niches: 1. If you're currently writing extremely high-assurance software, the sort of thing where you write a proof in Coq and then use that to generate C code, then something similar to Idris might be a win. Ditto for some people using model-checker tools like TLA+? 2. I could imagine a dependent type system being "bolted on" to unsafe Rust to formally verify correctness of code that regular Rust can't verify. This might require using Rust attributes and an external tool. But I could see it happening if somebody loved the The Little Typer and wanted an ambitious thesis project, for example. But even though I don't expect dependent types to go mainstream in the next 5-10 years, they're one of those ideas than might occasionally contribute a major inspiration to a challenging project.
- ajross 4y ago
  > Dependent types are hard to retrofit onto an existing language. Dependent types are hard to retrofit onto existing problems. Software everywhere wants to work with data of indeterminate size/parametrization at runtime. You want your system that tracks inventory stock to work with three warehouses or four, etc... Dependent types make all that stuff part of the type system, so now "list of 3 warehouse_t" and "list of 4 warehouse_t" are no longer equivalent. Obviously that's all "solvable", but not in a way that matches the intuition of generations of hackers who have been building these systems. It's in some sense analogous to Haskell's "Death by a Thousand Monad Tutorials". At some point you just have to recognize that this isn't the right metaphor for the problem areas it's trying to address and move on.
  - mcguire 4y ago
    Your point is good, but your example isn't. :-) A dependent type can easily express "list of n warehouse_t's where 0 < n <= 1,000,000,000".
    - ajross 4y ago
      Not if the input data isn't known at compile time it can't. I get what you're saying, and admit that my example was glib and short, but the point remains: putting "state" data into the type system forces programmers to be explicit about things that were just part of the algorithm before. The word "automagical" is a term of art for a reason. It's an ideal that our ancestors have been baking into the concept of "good code" for decades and decades, and dependent types throw it in the trash in favor of a variant idea of "correctness" that IMHO doesn't correspond to what society actually wants its computers to do for it.
      - rowanG077 4y ago
        Sure it can. It can be as simple as this (pseudo code): warehouses = get_warehouses_via_io() if len(warehouses) == 0: -- Here you have a proof warehouses is empty return Err("Oh no couldn't get warehouses") else if len(warehouses) > 10000: -- Here you have a proof warehouses contains more then 10000 elements. else: -- Here you have a proof that the amount of warehouses is not 0 and not larger then 10000 or you have between 1 and 10000 inclusive warehouses do_stuff(warehouses) Even Haskell which barely has dependent typing can do that. You simply have to introduce a proof that your lists length is between those.
        ajross 4y ago
        Once again, I'm not saying you can't do it. I'm saying that doing it requires filling your app with that sort of boilerplate nonsense when five decades of software engineering have been trying to remove it and considering it good practice to have done so.
        4y ago
- mcguire 4y ago
  The big problem I see with dependent types is that they ultimately require doing proofs whether you're using proof assistants like Coq or model checkers like (normal :-)) TLA+. Proofs are hard, for those who haven't had the training and experience (the coding bootcamp goes right out), and proof software is bizarre, opaque, and normal manual proof techniques don't apply or are difficult to translate. That being said, things like Ada SPARK and Frama-C are the same sort of tools as dependently typed languages, but are more from the assertion model and so use imperative code rather than tossing functional language on top of everything else.
  - chriswarbo 4y ago
    > The big problem I see with dependent types is that they ultimately require doing proofs... Proofs are hard, for those who haven't had the training and experience (the coding bootcamp goes right out), and proof software is bizarre, opaque, and normal manual proof techniques don't apply or are difficult to translate. Proofs are programs (via curry-howard), so it's not completely unrelated to what programmers do day-to-day. Often, the correctness proof is as simple as beta-reduction, which languages like Idris will perform automatically; although this usually relies on a good choice of representation, which is a skill in itself. Outside of the happy-path, things certainly do get harder, but there's always a choice of whether to just skip the proof and say "trust me", which is no worse than other approaches. A nice example is vector concatentation: // Peano encoding of natural numbers; e.g. 3 = Succ (Succ (Succ Zero)) data Nat: Type where Zero: Nat Succ: Nat -> Nat // Addition, by recursing on the first argument plus: Nat -> Nat -> Nat plus Zero y = y plus (Succ x) y = Succ (plus x y) // Lists of a known length data Vec: Nat -> Type -> Type where VNil : (t: Type) -> Vec Zero t VCons: (t: Type) -> (n: Nat) -> (head: t) -> (tail: Vec n t) -> Vec (Succ n) t // Append a Vec of length m to another of length n: // - The resulting Vec has length 'plus m n' // - All elements of the inputs and output have the same type t append: (t: Type) -> (m: Nat) -> (n: Nat) -> Vec m t -> Vec n t -> Vec (plus m n) t append _ _ _ (VNil _) y = y append t _ n (VCons _ l x xs) y = VCons t (plus l n) x (append t l n xs y) The correctness proof of 'append' follows from beta-reduction. In the `VNil` case, we need to prove that the type of y matches the return type, i.e. that for all n and t, Vec n t = Vec (plus m n) t. In this branch the first vector argument is VNil _ (where '_' indicates something we don't care about). According to the definition of Vec, this argument has type 'Vec Zero _', and according to the type of 'append' it has type 'Vec m t'. Hence Vec Zero _ = Vec m t, telling us that m = Zero (and this occurrence of '_' corresponds to t, but we don't care). Hence the context of this first branch contains the binding m = Zero; so our original equation Vec n t = Vec (plus m n) t beta-reduces to Vec n t = Vec (plus Zero n) t. This occurrence of 'plus' matches the first branch of its definition, so we can beta-reduce further to get 'Vec n t = Vec n t', Q.E.D. In the second branch of 'append', we need to show that the type of 'VCons t (plus l n) x (append t l n xs y)' is the same as the return type 'Vec (plus m n) t'. First we can check that the recursive call to 'append' is well-typed, i.e. xs has type Vec l t, and y has type Vec n t, which are both correct. The return type of that recursive call is Vec (plus l n) t, matching the '(plus l n)' argument given to 'VCons'. Hence the type of the 'VCons' call is Vec (Succ (plus l n)) t, so we need to match this with the overall return type of 'append': Vec (Succ (plus l n)) t = Vec (plus m n) t In this branch, the first vector argument is VCons _ l x xs, which (from the definition of Vec) has type Vec (Succ l) t. According to the type of 'append', it also has type Vec m t, so we know that Vec (Succ l) t = Vec m t, and hence m = Succ l. Hence our equation for the return type beta-reduces to Vec (Succ (plus l n)) t = Vec (plus (Succ l) n) t. The occurrence of 'plus' on the right-hand-side matches the second branch of its definition, so we can beta-reduce this to: Vec (Succ (plus l n)) t = Vec (Succ (plus l n)) t. Q.E.D. The steps above correspond exactly to "running the program" (i.e. evaluating/reducing the expressions), and is performed automatically in languages like Idris. Hence we don't need to write out any separate "proof", the definition of the 'append' function is proven correct just by evaluating the expressions which occur in its types (taking into account the context of the branches those expressions occur in). This is the "happy path". The reason I like this is example is that we can completely break it, simply by swapping around the 'plus m n' to 'plus n m' in the type of 'append'. That gives us expressions like 'plus n Zero' and 'plus n (Succ l)', which don't match the branches of 'plus', and hence won't beta-reduce. In order to make this work, we need to prove the general theorem 'plus x y = plus y x', and use that to flip the type into the original order. Proving that theorem requires proving lemmas like 'plus x 0 = x', etc. which is absolutely the sort of thing day-to-day programmers don't want to bother with! On the other hand, it's certainly nice for library developers to have the option of proving such things. Again, we can always skip the proof if we don't feel it's worth the effort, and the result is no less safe than the non-dependent systems already used by those day-to-day programmers!

ekidd 4y ago

Here's my reasoning on why dependent types may still be a couple of language generations from the mainstream: - Dependent types are hard to retrofit onto an existing language. (Retrofitting generics has had very mixed results, and dependent types are likely harder to retrofit?) - It takes a good 10 years for a new language to really hit the mainstream, even if everything goes right. (This could change if a big player pushes a language.) - All type systems represent a tradeoff, "Roughly how much extra confidence can I get in this program, and for how little extra time spent learning and coding?" Dependent types give you some very interesting new guarantees, but they require picking up new skills. But a future language in this space might make these tradeoffs more appealing! - I'm not sure that any of the existing dependently-typed languages have hit the magic combination of features and tools that would be needed to break out. In the nearer term, I can imagine dependent typing showing up in at least two niches: 1. If you're currently writing extremely high-assurance software, the sort of thing where you write a proof in Coq and then use that to generate C code, then something similar to Idris might be a win. Ditto for some people using model-checker tools like TLA+? 2. I could imagine a dependent type system being "bolted on" to unsafe Rust to formally verify correctness of code that regular Rust can't verify. This might require using Rust attributes and an external tool. But I could see it happening if somebody loved the The Little Typer and wanted an ambitious thesis project, for example. But even though I don't expect dependent types to go mainstream in the next 5-10 years, they're one of those ideas than might occasionally contribute a major inspiration to a challenging project.

ajross 4y ago
> Dependent types are hard to retrofit onto an existing language. Dependent types are hard to retrofit onto existing problems. Software everywhere wants to work with data of indeterminate size/parametrization at runtime. You want your system that tracks inventory stock to work with three warehouses or four, etc... Dependent types make all that stuff part of the type system, so now "list of 3 warehouse_t" and "list of 4 warehouse_t" are no longer equivalent. Obviously that's all "solvable", but not in a way that matches the intuition of generations of hackers who have been building these systems. It's in some sense analogous to Haskell's "Death by a Thousand Monad Tutorials". At some point you just have to recognize that this isn't the right metaphor for the problem areas it's trying to address and move on.
- mcguire 4y ago
  Your point is good, but your example isn't. :-) A dependent type can easily express "list of n warehouse_t's where 0 < n <= 1,000,000,000".
  - ajross 4y ago
    Not if the input data isn't known at compile time it can't. I get what you're saying, and admit that my example was glib and short, but the point remains: putting "state" data into the type system forces programmers to be explicit about things that were just part of the algorithm before. The word "automagical" is a term of art for a reason. It's an ideal that our ancestors have been baking into the concept of "good code" for decades and decades, and dependent types throw it in the trash in favor of a variant idea of "correctness" that IMHO doesn't correspond to what society actually wants its computers to do for it.
    - rowanG077 4y ago
      Sure it can. It can be as simple as this (pseudo code): warehouses = get_warehouses_via_io() if len(warehouses) == 0: -- Here you have a proof warehouses is empty return Err("Oh no couldn't get warehouses") else if len(warehouses) > 10000: -- Here you have a proof warehouses contains more then 10000 elements. else: -- Here you have a proof that the amount of warehouses is not 0 and not larger then 10000 or you have between 1 and 10000 inclusive warehouses do_stuff(warehouses) Even Haskell which barely has dependent typing can do that. You simply have to introduce a proof that your lists length is between those.
      - ajross 4y ago
        Once again, I'm not saying you can't do it. I'm saying that doing it requires filling your app with that sort of boilerplate nonsense when five decades of software engineering have been trying to remove it and considering it good practice to have done so.
        4y ago
mcguire 4y ago
The big problem I see with dependent types is that they ultimately require doing proofs whether you're using proof assistants like Coq or model checkers like (normal :-)) TLA+. Proofs are hard, for those who haven't had the training and experience (the coding bootcamp goes right out), and proof software is bizarre, opaque, and normal manual proof techniques don't apply or are difficult to translate. That being said, things like Ada SPARK and Frama-C are the same sort of tools as dependently typed languages, but are more from the assertion model and so use imperative code rather than tossing functional language on top of everything else.
- chriswarbo 4y ago
  > The big problem I see with dependent types is that they ultimately require doing proofs... Proofs are hard, for those who haven't had the training and experience (the coding bootcamp goes right out), and proof software is bizarre, opaque, and normal manual proof techniques don't apply or are difficult to translate. Proofs are programs (via curry-howard), so it's not completely unrelated to what programmers do day-to-day. Often, the correctness proof is as simple as beta-reduction, which languages like Idris will perform automatically; although this usually relies on a good choice of representation, which is a skill in itself. Outside of the happy-path, things certainly do get harder, but there's always a choice of whether to just skip the proof and say "trust me", which is no worse than other approaches. A nice example is vector concatentation: // Peano encoding of natural numbers; e.g. 3 = Succ (Succ (Succ Zero)) data Nat: Type where Zero: Nat Succ: Nat -> Nat // Addition, by recursing on the first argument plus: Nat -> Nat -> Nat plus Zero y = y plus (Succ x) y = Succ (plus x y) // Lists of a known length data Vec: Nat -> Type -> Type where VNil : (t: Type) -> Vec Zero t VCons: (t: Type) -> (n: Nat) -> (head: t) -> (tail: Vec n t) -> Vec (Succ n) t // Append a Vec of length m to another of length n: // - The resulting Vec has length 'plus m n' // - All elements of the inputs and output have the same type t append: (t: Type) -> (m: Nat) -> (n: Nat) -> Vec m t -> Vec n t -> Vec (plus m n) t append _ _ _ (VNil _) y = y append t _ n (VCons _ l x xs) y = VCons t (plus l n) x (append t l n xs y) The correctness proof of 'append' follows from beta-reduction. In the `VNil` case, we need to prove that the type of y matches the return type, i.e. that for all n and t, Vec n t = Vec (plus m n) t. In this branch the first vector argument is VNil _ (where '_' indicates something we don't care about). According to the definition of Vec, this argument has type 'Vec Zero _', and according to the type of 'append' it has type 'Vec m t'. Hence Vec Zero _ = Vec m t, telling us that m = Zero (and this occurrence of '_' corresponds to t, but we don't care). Hence the context of this first branch contains the binding m = Zero; so our original equation Vec n t = Vec (plus m n) t beta-reduces to Vec n t = Vec (plus Zero n) t. This occurrence of 'plus' matches the first branch of its definition, so we can beta-reduce further to get 'Vec n t = Vec n t', Q.E.D. In the second branch of 'append', we need to show that the type of 'VCons t (plus l n) x (append t l n xs y)' is the same as the return type 'Vec (plus m n) t'. First we can check that the recursive call to 'append' is well-typed, i.e. xs has type Vec l t, and y has type Vec n t, which are both correct. The return type of that recursive call is Vec (plus l n) t, matching the '(plus l n)' argument given to 'VCons'. Hence the type of the 'VCons' call is Vec (Succ (plus l n)) t, so we need to match this with the overall return type of 'append': Vec (Succ (plus l n)) t = Vec (plus m n) t In this branch, the first vector argument is VCons _ l x xs, which (from the definition of Vec) has type Vec (Succ l) t. According to the type of 'append', it also has type Vec m t, so we know that Vec (Succ l) t = Vec m t, and hence m = Succ l. Hence our equation for the return type beta-reduces to Vec (Succ (plus l n)) t = Vec (plus (Succ l) n) t. The occurrence of 'plus' on the right-hand-side matches the second branch of its definition, so we can beta-reduce this to: Vec (Succ (plus l n)) t = Vec (Succ (plus l n)) t. Q.E.D. The steps above correspond exactly to "running the program" (i.e. evaluating/reducing the expressions), and is performed automatically in languages like Idris. Hence we don't need to write out any separate "proof", the definition of the 'append' function is proven correct just by evaluating the expressions which occur in its types (taking into account the context of the branches those expressions occur in). This is the "happy path". The reason I like this is example is that we can completely break it, simply by swapping around the 'plus m n' to 'plus n m' in the type of 'append'. That gives us expressions like 'plus n Zero' and 'plus n (Succ l)', which don't match the branches of 'plus', and hence won't beta-reduce. In order to make this work, we need to prove the general theorem 'plus x y = plus y x', and use that to flip the type into the original order. Proving that theorem requires proving lemmas like 'plus x 0 = x', etc. which is absolutely the sort of thing day-to-day programmers don't want to bother with! On the other hand, it's certainly nice for library developers to have the option of proving such things. Again, we can always skip the proof if we don't feel it's worth the effort, and the result is no less safe than the non-dependent systems already used by those day-to-day programmers!