4 ms·

> Dependent types are hard to retrofit onto an existing language. Dependent types are hard to retrofit onto existing problems. Software everywhere wants to wo

by 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.
      - rowanG077 4y ago
        If statements are boilerplate? How else would you do branching? Gotos? There are definitely cases where dependent types add a lot of boilerplate. But it's not these simple cases. And guess what. You pay for what you use. If you don't want to prove something and just run your program then you can just do it.
      - mcguire 4y ago
        By "boilerplate nonsense" do you mean input validation? Because that is all that is.
        ajross 4y ago
        It isn't, though. "Write a program to sort the words you find in the input file" is something everyone here learns in leetcode training, and when done "properly" requires no "validation" of the input (beyond stuff like runtime error checking of allocations I guess). I shouldn't have gotten involved. And I think I need to retract my hedging above: this is exactly like monads. People caught up in the mania just can't understand why the rest of the world doesn't like their solution and insist on it being some kind of failure on the part of humanity to understand it.
        Tainnor 4y ago
        > "Write a program to sort the words you find in the input file" That's as trivial to write in a dependently typed language as it is in, say, Python (leaving aside the fact that you don't like monads), e.g. Idris: main : IO () main = do Right contents <- readFile "myfile.txt" let theLines = lines contents let sorted = sort theLines -- do something with sorted Of course, that doesn't use any dependent types, but nobody says that you have to use dependent types for a program so trivial you're unlikely to screw anything up. (And also: the standard library could have instead defined the functions "lines" such that it does use a dependent type. In that case, almost nothing about the program would change, except you would now write "let (n * theLines)" because the length is now part of the return value.) Dependent types are for where it makes sense to encode invariants, e.g. matMult : Matrix k m -> Matrix m n -> Matrix k n And of course, that function works for matrices of arbitrary dimensions, so the argument "we can't know the size of the matrices at compile time" doesn't apply.
  - haskellandchill 4y ago
    > Not if the input data isn't known at compile time it can't look at the idris example of printf (https://gist.github.com/chrisdone/672efcd784528b7d0b7e17ad9c115292 https://gist.github.com/chrisdone/672efcd784528b7d0b7e17ad9c...) for how to do this, the idris book has some really good example of how you can handle what you would think is "not known at compile time" but can actually be parameterized
- Tainnor 4y ago
  A dependent type can also just be "list of n warehouse_t", where n is completely unconstrained. I feel the constraint on the size of the input has made the discussion much more complicated than necessary, because now we need to carry around proof types, which are a more advanced use case.
  - mcguire 4y ago
    True, but at that point you're not using dependent types.
    - Tainnor 4y ago
      You are, because the type still depends on the value of n. It's just that that value is unconstrained. It can still be used parametrically in type signatures, though, e.g. append : Vect n a -> Vect m a -> Vect (n+m) a That's not possible without dependent types.
deleted 4y ago
[deleted]
Tainnor 4y ago
> 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. Dependent types allow you to make that stuff part of your type system. But of course, Idris (and any other dependently typed language) still has "List" as a datatype which does not encode the length as part of its type - and if it didn't, it would be trivial to define. And it's easy enough to convert between the two types, should there be any need to either increase or decrease the precision of your types at different points in your program, depending on the need. There may not be a need to know at a type level how many items are in your cart, but there's surely a value in knowing, for example, that sorting a list doesn't change the number of elements, or that matrix multiplication is well-defined. You may argue that merely having the capability to use dependent types will lead to people abusing and overcomplicating things - but somehow we're already doing a very good job overcomplicating things with much simpler languages, e.g. Java reflection magic, or Ruby metaprogramming, so I'm not sure the "we shouldn't give people the rope to hang themselves" argument is valid. This is a bit different from the monad example in that it's practically impossible to write Haskell without understanding monads, since you can't do IO without it.

by ajross 4y ago

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.
    - rowanG077 4y ago
      If statements are boilerplate? How else would you do branching? Gotos? There are definitely cases where dependent types add a lot of boilerplate. But it's not these simple cases. And guess what. You pay for what you use. If you don't want to prove something and just run your program then you can just do it.
    - mcguire 4y ago
      By "boilerplate nonsense" do you mean input validation? Because that is all that is.
      - ajross 4y ago
        It isn't, though. "Write a program to sort the words you find in the input file" is something everyone here learns in leetcode training, and when done "properly" requires no "validation" of the input (beyond stuff like runtime error checking of allocations I guess). I shouldn't have gotten involved. And I think I need to retract my hedging above: this is exactly like monads. People caught up in the mania just can't understand why the rest of the world doesn't like their solution and insist on it being some kind of failure on the part of humanity to understand it.
        Tainnor 4y ago
        > "Write a program to sort the words you find in the input file" That's as trivial to write in a dependently typed language as it is in, say, Python (leaving aside the fact that you don't like monads), e.g. Idris: main : IO () main = do Right contents <- readFile "myfile.txt" let theLines = lines contents let sorted = sort theLines -- do something with sorted Of course, that doesn't use any dependent types, but nobody says that you have to use dependent types for a program so trivial you're unlikely to screw anything up. (And also: the standard library could have instead defined the functions "lines" such that it does use a dependent type. In that case, almost nothing about the program would change, except you would now write "let (n * theLines)" because the length is now part of the return value.) Dependent types are for where it makes sense to encode invariants, e.g. matMult : Matrix k m -> Matrix m n -> Matrix k n And of course, that function works for matrices of arbitrary dimensions, so the argument "we can't know the size of the matrices at compile time" doesn't apply.
- haskellandchill 4y ago
  > Not if the input data isn't known at compile time it can't look at the idris example of printf (https://gist.github.com/chrisdone/672efcd784528b7d0b7e17ad9c115292 https://gist.github.com/chrisdone/672efcd784528b7d0b7e17ad9c...) for how to do this, the idris book has some really good example of how you can handle what you would think is "not known at compile time" but can actually be parameterized
Tainnor 4y ago
A dependent type can also just be "list of n warehouse_t", where n is completely unconstrained. I feel the constraint on the size of the input has made the discussion much more complicated than necessary, because now we need to carry around proof types, which are a more advanced use case.
- mcguire 4y ago
  True, but at that point you're not using dependent types.
  - Tainnor 4y ago
    You are, because the type still depends on the value of n. It's just that that value is unconstrained. It can still be used parametrically in type signatures, though, e.g. append : Vect n a -> Vect m a -> Vect (n+m) a That's not possible without dependent types.

deleted 4y ago

[deleted]

Tainnor 4y ago

> 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. Dependent types allow you to make that stuff part of your type system. But of course, Idris (and any other dependently typed language) still has "List" as a datatype which does not encode the length as part of its type - and if it didn't, it would be trivial to define. And it's easy enough to convert between the two types, should there be any need to either increase or decrease the precision of your types at different points in your program, depending on the need. There may not be a need to know at a type level how many items are in your cart, but there's surely a value in knowing, for example, that sorting a list doesn't change the number of elements, or that matrix multiplication is well-defined. You may argue that merely having the capability to use dependent types will lead to people abusing and overcomplicating things - but somehow we're already doing a very good job overcomplicating things with much simpler languages, e.g. Java reflection magic, or Ruby metaprogramming, so I'm not sure the "we shouldn't give people the rope to hang themselves" argument is valid. This is a bit different from the monad example in that it's practically impossible to write Haskell without understanding monads, since you can't do IO without it.