6 ms·

Dependently type languages are wonderful in theory and a royal pain in the butt in practice. It's a great example of "devil in the details" kind of thing. For

Dependently type languages are wonderful in theory and a royal pain in the butt in practice. It's a great example of "devil in the details" kind of thing. For example, let's say you define a type of list of size n. Great. You can only assign list of the same size and you can only append an element of the type "n" to a type "n-1" or the compiler will complain. Now you can even prove that your program is formally correct. What's not to like? And then, reality knocks at your door. How do you instantiate such a type? It needs to be instantiated right away with n elements or your program won't compile. But these elements are coming from the runtime, say, a database. How the hell does this work? Dependently typed languages that go just a step beyond prototypes quickly realize how crippling this approach is and they will give you all kinds of escape hatches to weaken the type system just so you can use the darn thing. But it's futile, because at the end of the day, a program is a living thing that relies on side effects and external inputs, and sophisticated systems are just not designed to cope with human fuzziness. The reason why dependently typed systems never became popular is not because the world hasn't realized yet how awesome they are: it's because they just aren't a good fit to solve real problems.

mjcohen 11y ago
That's one of the reasons Pascal failed.
geofft 11y ago
I wish we (both potential users, and developers of these languages) would start seeing these things more like enhanced tests than perfect manifestations of mathematical truth. Nobody would ever question the value of a unit-testing framework because it requires you to instantiate objects and doesn't hit the database and the ORM. (Yes, there are testing strategies that cover all of that, but for unit-testing application logic, you generally want to skip all of that.) Dependent types should let you do the same thing that a test would do, except exhaustively: if you add a new email address to an account with N addresses, you can then index N+1 of those addresses, but no more. The N-address account coming from the ORM isn't considered an "escape hatch" that "weakens the test system": it's just how it works. I want stronger types for exhaustive testing of business logic on individual functions -- the sort of things that a comment would say (e.g. "Returns a subset of this parameter if it is provided, otherwise..."), except machine-checked. I don't need my entire program to have a type that Messrs. Curry and Howard like. In all probability, my entire program is structured as an infinite loop anyway. I don't know that any systems really let you get here (other than maybe extraction of particular functions into Haskell or ML, but really the people who would voluntarily write their entire app in Haskell or ML are not the right target audience).
clhodapp 11y ago
Your "I-can't-work-with-this-unsized-list-because-I-need-to-pass-it-to-something-that-takes-a-sized-list" problem seems like something that one might _think_ would be a problem if one understood advanced types on a conceptual or theoretical level but not how to use them in real-world code. It's actually pretty easy to deal with cases like this... At the end of the day, you just end up having to code for both the case where the list matches the size requirements of the code you want to call and the case where it doesn't. For example, you could pass the unsized list to a function which performs validation of its actual runtime size, returning, e.g., an `Option[List[Int] @@ MinSize[_5]]` (if I may use Scala-speak). You'd then have to handle both the case where the `Option` is a `Some` and the case where it's a `None`. Ultimately, it ends up being extremely similar to checked exceptions: you are simply forced to write code to handle all cases, rather than writing code that allows some of them to blow up at runtime (while telling yourself "that case could never happen in the real world" or "that's an edge case, we'll just ignore it").
- incepted 11y ago
  > At the end of the day, you just end up having to code for both the case where the list matches the size requirements of the code you want to call and the case where it doesn't. I don't follow. If your list is not the right size, your program doesn't compile, period. If it does, you're not using a dependently typed language. Am I missing something?
  - clhodapp 11y ago
    I think you are. I think you are missing the possibility to write a total function of type `List[Int] => Option[List[Int]] @@ MinSize[_5]` (I'm still writing Scala-ish types because that's where I feel comfortable). This gets you into a world where you can deal with your previously-unsized `List` as a sized `List` (either you can map over your `Option` or you can fold the `Some` and `None` cases together by providing some default).
  - pathsjs 11y ago
    It depends on the language. For instance in Scala you can simulate collections of fixed size as in https://github.com/milessabin/shapeless/blob/master/core/src/main/scala/shapeless/sized.scala https://github.com/milessabin/shapeless/blob/master/core/src... Then, at runtime, you can cast an unsized list to a sized list giving - say - a function List[A] => Option[Sized[List[A], N5]] that will fail if the list is not of size 5. From then on you can go on letting the compiler keep track of lengths. Of course, this does not work at all if you have no clue what size your input will have
oggy 11y ago
You're misguided. What you describe is not really an issue for dependent types. Your attitude seems to be shared by a lot of people, so I'll try to clear things up a bit. I think it helps if I use refinement types (as used in F), which are just dependent types in disguise. Taking your example, I would have written a function f* that takes a list (with an arbitrary type of elements) and produces an integer. Its basic ML type would be: f : list 'a -> int Now taking your example, assume that, for whichever reason, f only works for lists of length 5. This would probably never arise in practice, but I'm just going with your example. First, we have to say what "works" means. Intuitively, it means that f produces a reasonable output. Let's say we have defined a function p which says whether the output is reasonable. In F, I can state all of that by giving my function f* the type: f : l:list 'a{length l = 5} -> x:int{p x = True} I can only give this type if I can convince the compiler that the result really satisfies p - this is one point I'll get back to later. Now assume I want to use this function later in my code to deal with some user provided input. Assume I have a function read_int_list: read_int_list : () -> list int I can now combine this function with f, but only if I ensure that the length of the read list is 5: val process_input = let inp = read_inst_list (); let res = if length inp = 5 then f inp else -1 // error This will now be accepted by the compiler, since it will be able to deduce that inp is an admissible input to f, because the function call was guarded by the if condition (I'll also get back to this). Note that the code above is absolutely no different than what you would write in any "regular" programming language (including ML). What is different is that in a regular language you could forget to add the condition - but not in F. Of course, the error handling code above is not sensible. So interacting with user input and output is absolutely NOT a problem for dependently typed languages and their ilk. In fact, there is a full-blown implementation of the TLS protocol in F. What is a problem, however, are the two points I hinted at: convincing the compiler that your statements are true. This is done in one of the two ways. First, you can manually give "hints" to the compiler, which is normally very tedious. Second, the compiler can try proving them automatically (F* for example leverages an SMT solver), which is great when it works, but often doesn't work. So the real problem is that producing proofs is quite time consuming, and thus expensive. The world, as you put it, is not completely wrong: very often, a buggy program is cheaper than a correct one. Heck, people still stick to OpenSSL over the above verified TLS implementation - and for good reasons. The exceptions being programs used in NASA rovers and such - which is where you're starting to see dependent types being used. I certainly won't use them for my projects - at least not until the systems get massively better at producing proofs. It's partly happened with the advent of the SMT solvers, but it's nowhere near enough.
jules 11y ago
> How the hell does this work? It's easy, since it works as it always did. You check whether the list coming from the database has the correct size n, and then the type system knows that and lets you pass said list to a function that expects a list of size n. list = GetAListFromTheDatabase() if(list.size == n){ // type checker knows that the size is n here foo(list); }else{ error("Database returned a list of incorrect size."); }
TheCoelacanth 11y ago
In a dependently typed language, an if statement isn't just a run-time check, it also provides a compile-time proof that its condition is true in one branch and false in the other branch. So your insinuation that run-time checks are not possible in dependently typed languages is false; you just have to prove at compile-time that all possible results of the run-time check have a valid execution path. So if you have an unsized array A, you can't just write `return A[5]`, but you can write `if (A.length() > 5) { return A[5]; } else { return 0; }`.

mjcohen 11y ago

That's one of the reasons Pascal failed.

geofft 11y ago

I wish we (both potential users, and developers of these languages) would start seeing these things more like enhanced tests than perfect manifestations of mathematical truth. Nobody would ever question the value of a unit-testing framework because it requires you to instantiate objects and doesn't hit the database and the ORM. (Yes, there are testing strategies that cover all of that, but for unit-testing application logic, you generally want to skip all of that.) Dependent types should let you do the same thing that a test would do, except exhaustively: if you add a new email address to an account with N addresses, you can then index N+1 of those addresses, but no more. The N-address account coming from the ORM isn't considered an "escape hatch" that "weakens the test system": it's just how it works. I want stronger types for exhaustive testing of business logic on individual functions -- the sort of things that a comment would say (e.g. "Returns a subset of this parameter if it is provided, otherwise..."), except machine-checked. I don't need my entire program to have a type that Messrs. Curry and Howard like. In all probability, my entire program is structured as an infinite loop anyway. I don't know that any systems really let you get here (other than maybe extraction of particular functions into Haskell or ML, but really the people who would voluntarily write their entire app in Haskell or ML are not the right target audience).

clhodapp 11y ago

Your "I-can't-work-with-this-unsized-list-because-I-need-to-pass-it-to-something-that-takes-a-sized-list" problem seems like something that one might _think_ would be a problem if one understood advanced types on a conceptual or theoretical level but not how to use them in real-world code. It's actually pretty easy to deal with cases like this... At the end of the day, you just end up having to code for both the case where the list matches the size requirements of the code you want to call and the case where it doesn't. For example, you could pass the unsized list to a function which performs validation of its actual runtime size, returning, e.g., an `Option[List[Int] @@ MinSize[_5]]` (if I may use Scala-speak). You'd then have to handle both the case where the `Option` is a `Some` and the case where it's a `None`. Ultimately, it ends up being extremely similar to checked exceptions: you are simply forced to write code to handle all cases, rather than writing code that allows some of them to blow up at runtime (while telling yourself "that case could never happen in the real world" or "that's an edge case, we'll just ignore it").

incepted 11y ago
> At the end of the day, you just end up having to code for both the case where the list matches the size requirements of the code you want to call and the case where it doesn't. I don't follow. If your list is not the right size, your program doesn't compile, period. If it does, you're not using a dependently typed language. Am I missing something?
- clhodapp 11y ago
  I think you are. I think you are missing the possibility to write a total function of type `List[Int] => Option[List[Int]] @@ MinSize[_5]` (I'm still writing Scala-ish types because that's where I feel comfortable). This gets you into a world where you can deal with your previously-unsized `List` as a sized `List` (either you can map over your `Option` or you can fold the `Some` and `None` cases together by providing some default).
- pathsjs 11y ago
  It depends on the language. For instance in Scala you can simulate collections of fixed size as in https://github.com/milessabin/shapeless/blob/master/core/src/main/scala/shapeless/sized.scala https://github.com/milessabin/shapeless/blob/master/core/src... Then, at runtime, you can cast an unsized list to a sized list giving - say - a function List[A] => Option[Sized[List[A], N5]] that will fail if the list is not of size 5. From then on you can go on letting the compiler keep track of lengths. Of course, this does not work at all if you have no clue what size your input will have

oggy 11y ago

You're misguided. What you describe is not really an issue for dependent types. Your attitude seems to be shared by a lot of people, so I'll try to clear things up a bit. I think it helps if I use refinement types (as used in F), which are just dependent types in disguise. Taking your example, I would have written a function f* that takes a list (with an arbitrary type of elements) and produces an integer. Its basic ML type would be: f : list 'a -> int Now taking your example, assume that, for whichever reason, f only works for lists of length 5. This would probably never arise in practice, but I'm just going with your example. First, we have to say what "works" means. Intuitively, it means that f produces a reasonable output. Let's say we have defined a function p which says whether the output is reasonable. In F, I can state all of that by giving my function f* the type: f : l:list 'a{length l = 5} -> x:int{p x = True} I can only give this type if I can convince the compiler that the result really satisfies p - this is one point I'll get back to later. Now assume I want to use this function later in my code to deal with some user provided input. Assume I have a function read_int_list: read_int_list : () -> list int I can now combine this function with f, but only if I ensure that the length of the read list is 5: val process_input = let inp = read_inst_list (); let res = if length inp = 5 then f inp else -1 // error This will now be accepted by the compiler, since it will be able to deduce that inp is an admissible input to f, because the function call was guarded by the if condition (I'll also get back to this). Note that the code above is absolutely no different than what you would write in any "regular" programming language (including ML). What is different is that in a regular language you could forget to add the condition - but not in F. Of course, the error handling code above is not sensible. So interacting with user input and output is absolutely NOT a problem for dependently typed languages and their ilk. In fact, there is a full-blown implementation of the TLS protocol in F. What is a problem, however, are the two points I hinted at: convincing the compiler that your statements are true. This is done in one of the two ways. First, you can manually give "hints" to the compiler, which is normally very tedious. Second, the compiler can try proving them automatically (F* for example leverages an SMT solver), which is great when it works, but often doesn't work. So the real problem is that producing proofs is quite time consuming, and thus expensive. The world, as you put it, is not completely wrong: very often, a buggy program is cheaper than a correct one. Heck, people still stick to OpenSSL over the above verified TLS implementation - and for good reasons. The exceptions being programs used in NASA rovers and such - which is where you're starting to see dependent types being used. I certainly won't use them for my projects - at least not until the systems get massively better at producing proofs. It's partly happened with the advent of the SMT solvers, but it's nowhere near enough.

jules 11y ago

> How the hell does this work? It's easy, since it works as it always did. You check whether the list coming from the database has the correct size n, and then the type system knows that and lets you pass said list to a function that expects a list of size n. list = GetAListFromTheDatabase() if(list.size == n){ // type checker knows that the size is n here foo(list); }else{ error("Database returned a list of incorrect size."); }

TheCoelacanth 11y ago

In a dependently typed language, an if statement isn't just a run-time check, it also provides a compile-time proof that its condition is true in one branch and false in the other branch. So your insinuation that run-time checks are not possible in dependently typed languages is false; you just have to prove at compile-time that all possible results of the run-time check have a valid execution path. So if you have an unsized array A, you can't just write `return A[5]`, but you can write `if (A.length() > 5) { return A[5]; } else { return 0; }`.