5 ms·

1. No type inference (unlike ML-style types). 2. Oracle problem: In practise you never have full specifications (let me be provocative: Facebook has no speci

by 9q9 7y ago

1. No type inference (unlike ML-style types). 2. Oracle problem: In practise you never have full specifications (let me be provocative: Facebook has no specification in principle, only its ever changing code), and often, especially in early phases you rarely have specifications. 3. You pay the price for dependent types always (e.g. having to prove termination), even if you don't use interesting specifications. 4. Like Java's exception specifications, dependent types are 'non local', meaning that a change in one part of the code may ripple through the entire code bases, this stands in the way of quick code evolution, which is important -- at least in early parts of large-scale software projects. 5. Despite dependent types being 1/2 century old by now, and despite intensive effort, dependent types have not really been successfully been generalised to other forms of computing (OO, stateful, concurrecy, parallel, distributed, timed) -- unlike competing approaches. Summary: dependent types are wonderful as a foundations of mathematics, but have failed to live up to their promise as general purpose languages.

hope-striker 7y ago
1. Bidirectional typing can be easily generalized to dependent types. You can't always infer the type, but an 80% solution is definitely good enough for inference. 2. Your types don't have to be full specifications, and you can refine them later, no? 3. Idris, at least, doesn't force you to make all your functions total, and functions are actually partial by default. 4. Again, in Idris, implementations are hidden by default across modules. Maybe there's a nice middle-ground between hiding everything and exposing everything, but I don't know what that would look like. 5. What are the competing approaches and how are they better at dealing with, for example, distributed computing? I'm not very familiar with dependent types, but none of these seem like fundamental restrictions.
- 9q9 7y ago
  1. BIdirectional isn't magic. If I program MergeSort or Quicksort, and give it the signature forall T. Array[T] -> (T -> T -> Bool) -> Array[T] Bidirectional will not infer what's missing towards a full spec. 2. Yes, you can refine later, but if you want to refine later (and in practise you almost always have the full spec -- if it exists at all -- only at the end), then why pay the cost of dependent types from the start? Once you have the full spec, verify with Hoare logic. 3, 4: I'm not sufficiently familiar with Idris to comment. 5. Alternative approaches, in addition owhat "pron" mentioned includes program logic, e.g. TLA.
  - hope-striker 7y ago
    1. Yes, but the situation regarding type inference is only a bit worse than the situation in non-dependently-typed languages. Of course the compiler can't magically figure out what theorems you want to prove.
    - 9q9 7y ago
      This is my point. Adding dependent types comes with costs that you will always have to pay, even if you don't use the power of dependent types. If you verify with e.g. program logic in the few real-world cases where formal verification is financially viable, then you only pay the price when you do the verification.
chongli 7y ago
Every single one of your claims is addressed by the programming language Idris [1], which has dependent types. This is not to say that Idris is the only dependently typed language which solves these issues, only that it exists as a counterexample to your claims. 1. Idris does not have type inference at the top level, but it does infer types within the body of functions. It can even disambiguate identically-named functions with different types, something Haskell cannot do. Moreover, Idris (and other dependently typed languages) can perform implementation inference, something which is much more powerful and useful to the programmer than type inference. It lets you work interactively with the Idris compiler whereby you specify a type and Idris creates a skeleton of the function for you, filled with holes that you replace with expressions. You can ask Idris what the type of a hole is and it will helpfully tell you the types of all other identifiers in scope. You can even ask Idris to attempt to fill in the hole for you, something it can usually do when there is only one possible expression with that type (occurs extremely often in practice). Watch Edwin Brady's demo of Idris 2 [2] to see this form of interactive development in action. Note that although Idris 2 isn't finished yet, a great deal of these examples (such as zip) work in Idris 1.3.2 (the current release). 2. Idris lets you specify your program gradually. When problems arise, you can refine your types and Idris will guide you through all of the refactoring you need to do to enforce your new invariants. 3. Idris does not force all of your functions to be total, only the ones you want to use in types. Idris checks the totality of all your functions and can produce compilation errors based on totality annotations attached to your functions. In practice, It is not very hard to make every function in your program total, apart from the main loop. 4. Idris has modules and gives you powerful tools (such as views) that allow you to define a stable API at the module boundary. This means you can mess around with any of the types of private functions to your heart's content, without any visible change to the outside world. This is entirely the opposite of 'non local' Java exceptions. 5. Idris has extremely powerful tools for working with state and writing concurrent programs which preserve invariants that cannot otherwise be checked easily with other tools. As for OO, well, that's a concept so nebulous as to be almost incoherent at this point. In practice, Idris's interfaces can dispatch on as many parameters as you want, unlike most OO languages which only do single dispatch. [1] https://www.idris-lang.org https://www.idris-lang.org [2] https://www.youtube.com/watch?v=DRq2NgeFcO0 https://www.youtube.com/watch?v=DRq2NgeFcO0
permeakra 7y ago
1. Problems with type inference is a problem introduced with polymorphism with implicit type variables and isn't exclusive to dependent types, 'f = show . read' shouldn't compile because of type ambiguity. What is so specific about dependent types in this regard?

by 9q9 7y ago

hope-striker 7y ago

1. Bidirectional typing can be easily generalized to dependent types. You can't always infer the type, but an 80% solution is definitely good enough for inference. 2. Your types don't have to be full specifications, and you can refine them later, no? 3. Idris, at least, doesn't force you to make all your functions total, and functions are actually partial by default. 4. Again, in Idris, implementations are hidden by default across modules. Maybe there's a nice middle-ground between hiding everything and exposing everything, but I don't know what that would look like. 5. What are the competing approaches and how are they better at dealing with, for example, distributed computing? I'm not very familiar with dependent types, but none of these seem like fundamental restrictions.

9q9 7y ago
1. BIdirectional isn't magic. If I program MergeSort or Quicksort, and give it the signature forall T. Array[T] -> (T -> T -> Bool) -> Array[T] Bidirectional will not infer what's missing towards a full spec. 2. Yes, you can refine later, but if you want to refine later (and in practise you almost always have the full spec -- if it exists at all -- only at the end), then why pay the cost of dependent types from the start? Once you have the full spec, verify with Hoare logic. 3, 4: I'm not sufficiently familiar with Idris to comment. 5. Alternative approaches, in addition owhat "pron" mentioned includes program logic, e.g. TLA.
- hope-striker 7y ago
  1. Yes, but the situation regarding type inference is only a bit worse than the situation in non-dependently-typed languages. Of course the compiler can't magically figure out what theorems you want to prove.
  - 9q9 7y ago
    This is my point. Adding dependent types comes with costs that you will always have to pay, even if you don't use the power of dependent types. If you verify with e.g. program logic in the few real-world cases where formal verification is financially viable, then you only pay the price when you do the verification.

chongli 7y ago

Every single one of your claims is addressed by the programming language Idris [1], which has dependent types. This is not to say that Idris is the only dependently typed language which solves these issues, only that it exists as a counterexample to your claims. 1. Idris does not have type inference at the top level, but it does infer types within the body of functions. It can even disambiguate identically-named functions with different types, something Haskell cannot do. Moreover, Idris (and other dependently typed languages) can perform implementation inference, something which is much more powerful and useful to the programmer than type inference. It lets you work interactively with the Idris compiler whereby you specify a type and Idris creates a skeleton of the function for you, filled with holes that you replace with expressions. You can ask Idris what the type of a hole is and it will helpfully tell you the types of all other identifiers in scope. You can even ask Idris to attempt to fill in the hole for you, something it can usually do when there is only one possible expression with that type (occurs extremely often in practice). Watch Edwin Brady's demo of Idris 2 [2] to see this form of interactive development in action. Note that although Idris 2 isn't finished yet, a great deal of these examples (such as zip) work in Idris 1.3.2 (the current release). 2. Idris lets you specify your program gradually. When problems arise, you can refine your types and Idris will guide you through all of the refactoring you need to do to enforce your new invariants. 3. Idris does not force all of your functions to be total, only the ones you want to use in types. Idris checks the totality of all your functions and can produce compilation errors based on totality annotations attached to your functions. In practice, It is not very hard to make every function in your program total, apart from the main loop. 4. Idris has modules and gives you powerful tools (such as views) that allow you to define a stable API at the module boundary. This means you can mess around with any of the types of private functions to your heart's content, without any visible change to the outside world. This is entirely the opposite of 'non local' Java exceptions. 5. Idris has extremely powerful tools for working with state and writing concurrent programs which preserve invariants that cannot otherwise be checked easily with other tools. As for OO, well, that's a concept so nebulous as to be almost incoherent at this point. In practice, Idris's interfaces can dispatch on as many parameters as you want, unlike most OO languages which only do single dispatch. [1] https://www.idris-lang.org https://www.idris-lang.org [2] https://www.youtube.com/watch?v=DRq2NgeFcO0 https://www.youtube.com/watch?v=DRq2NgeFcO0

permeakra 7y ago

1. Problems with type inference is a problem introduced with polymorphism with implicit type variables and isn't exclusive to dependent types, 'f = show . read' shouldn't compile because of type ambiguity. What is so specific about dependent types in this regard?