20 ms·

Haskell's Type Classes: We Can Do Better

97 points by andars 11y ago

dkarapetyan 11y ago
Has anyone here shipped anything production worthy with dependently typed languages? I'm serious. There are like 10 PhDs in France working on a certified compiler toolchain for C and that's it. Meanwhile Go and JavaScript are taking over the world and they're anything but dependently typed. Maybe there's a reason for that? Maybe the reason is that after a certain point the validation overhead of advanced type systems is just not worth it. Yes, I know the article isn't about dependent types per se but many of the features he wants get pretty close to dependent types since that is pretty much the state of the art when it comes to advanced type systems with lawful abstractions and whatnot.
- Ixiaus 11y ago
  I'm shipping massive amounts of code written in Haskell - production worthy for a real product - and the benefits of using Haskell over any other mainstream imperative language have been fairly significant.
  - Drup 11y ago
    Haskell is not a real dependently type language. It may tries to quack like one, but compared to Idris/Agda, it's doing a very bad job at it. I'm pretty sure Parent didn't included Haskell.
    - wyager 11y ago
      Haskell has decent experimental support for dependent types. I've been using the CLaSH Haskell to hardware conversion system, which makes heavy use of type level arithmetic, with pretty good results.
      - Drup 11y ago
        Type level arithmetic is sugar for clever GADTs, not full blown dependent types. Try to do things in Agda/Idris and come back to haskell, the expressiveness is not nearly comparable.
        wyager 11y ago
        Are Nats in agda and idris not also just GADT based peano numbers?
        Drup 11y ago
        The toyish version showed in tutorials, yes. The real stuff, no, it's just .. integers. And anyway, my point was that you can do much much more than type level arithmetic.
    - Ixiaus 11y ago
      His comparison sounded much more like "research languages vs. mainstream imperative languages" and Haskell definitely came from research land, just as Idris and Agda are. Plus someone is seriously working on dependent types in Haskell - so no, I think it's fitting.
- jjaredsimpson 11y ago
  The value proposition I've always read is related to gains in expressiveness and correctness. Programming is eventually going to become like Advanced Chess (human+computer team) and entire classes of mistakes will cease to exist. I don't think I can be convinced that correct-by-construction methods are wrongheaded. I am convinced that humans aren't very good at wrangling precise and complex and large ideas without failure.
- Drup 11y ago
  Does selling CompCert to Airbus count as begin "production worthy" ? I would (not) be amused when people try to put javascript in plane navigation systems. Do not forget that most dependently type languages (and Coq the first) are proof languages. The goal is not (only) to write programs, but to prove things and a rather large number of theorem have been proven that way. Dependently types languages for programming (as opposed to proving) are very much cutting edge research. Is it so surprising that they are not used in the wild ? Edit: woops, missed the "here" in parent's comment. No, I don't work on compcert. :)
  - theseoafs 11y ago
    > Dependently types languages for programming (as opposed to proving) are very much cutting edge research. Is it so surprising that they are not used in the wild ? How long will this be the case? Seems like they've been "cutting edge research" for a few decades, and the Curry-Howard correspondence itself is like 80 years old. Surely if there were a real demand for these kinds of programming languages, we would have seen some industry penetration at some point, right?
    - tunesmith 11y ago
      There's been plenty of industry penetration for languages with more advanced type systems. Not sure why there's the arbitrary line being drawn here of dependent type systems. Some of this is about the penetration of certain ideas. Like, we had to wait for multiple cores on commodity hardware before functional programming started to cross over from the academic community to the professional web programmer. That shift helps your average programmer to think a bit more mathematically, and then it's basically about whether the programmer starts to appreciate types - and to me that seems to be less about purity of argument than the professional atmosphere the programmer is in. Are you prototyping and moving fast and breaking stuff, or are you caring more about longevity and correctness. And then once you start getting more into static typing and functional programming, a lot of these other ideas start to become more attractive and intriguing. It's like a lot of ideas that circulate around for a long time before they really take hold; you're waiting for a certain critical mass of system inputs and momentum, and then things can start to change really fast.
- mmarx 11y ago
  The formally-verified Odd Order Theorem[0] using Coq was quite an acomplishment (though probably not what you had in mind). [0] https://hal.inria.fr/hal-00816699/file/main.pdf https://hal.inria.fr/hal-00816699/file/main.pdf
- incepted 11y ago
  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).
- mafribe 11y ago
  after a certain point the validation overhead of advanced type systems is just not worth it. But what makes you think you need dependent types to do full specification and verification of a program? Instead you could use program logic. Write the program in any language you like and later, when it the program is finished verifiy that it meets its specification using program logic. This separates programming from verification completely. In my opinion this is the future of certified programming. Dependent types are too heavyweight to support any conventional programming process. Another advantage is that unlike Curry-Howard based verification, program logic does not have to be constructive, instead you can use classical reasoning with excluded middle. This tends to yield shorter proofs. See Microsoft's Daphny [1] or CFML [2] for prototype tool chains implementing program logic based verification. Facebook's infer tool [3], while not allowing full verification, is also based on program logic. [1] http://research.microsoft.com/en-us/projects/dafny http://research.microsoft.com/en-us/projects/dafny [2] http://www.chargueraud.org/softs/cfml http://www.chargueraud.org/softs/cfml [3] https://github.com/facebook/infer https://github.com/facebook/infer
  - darzu 11y ago
    > This separates programming from verification completely. This is simply not the case. Significant verification projects always plan for verification and do verification in tandem. This is definitely true for all Dafny projects to date as well. Verification is just so much harder than unverified programming that you generally want to do everything you can while programming to make verification easier. This may become less true as proof automation improves but it will always be a tension. > But what makes you think you need dependent types to do full specification [...] ? Also, keep in mind that Dafny and similar tools can only express first order logic; this can significantly restricts the expressiveness of your specification language and intermediate lemmas. > program logic does not have to be constructive, instead you can use classical reasoning with excluded middle. This is a silly point. First off proof assistants like Coq aren't inconsistent with the law of the excluded middle (only NuPRL is I believe) so you can always assume it as an axiom if you'd like. Most projects don't do this because constructivism is a benefit not a burden in verification: it allows you to make distinctions that aren't possible in classical logic. I agree that Dafny and similar projects are very exciting though; Dafny's tight integration with Z3 provides an awesome level of automation that will keep getting better and better.
- darzu 11y ago
  True certified programming has a lot of overhead but there are definitely areas where it'll be worth it: medical devices, car systems, mars rovers, aviation, etc. The University of Washington is actively working on verifying radiation therapy machine software and early results are already used in production for example. I think the reason certified programming hasn't been more widely adopted yet is because the tooling is terrible at the moment and we still have some important bits of theory to work out (e.g. homotopy type theory & other equality issues). It'll get there. Projects like Lean & Dafny at MSR, Adam Chlipala's work at MIT, and the large amount of theory work being done at CMU, Cornell, UPenn, Inria and other places are very promising. My bet is that the tooling & theory will continue to improve and eventually the overhead will become low enough that a significant portion (~10-20%) of software will be certified. I recommend reading Adam Chlipala's vision statement for inspiration on what certified programming could enable: http://adam.chlipala.net/summary.html http://adam.chlipala.net/summary.html
- jules 11y ago
  The reason is twofold. One, research into dependent types is still ongoing. Two, type system researchers promote provably correct programming as the advantage of dependent types. IMO the far more important advantage of dependent types is expressiveness and simplicity: they generalize a vast swath of different type system features and extensions to a handful of simple constructs. Well, arguably just a single construct: it generalizes the usual function type A -> B to the dependent function type x:A -> B(x). This subsumes a lot of things like generics, existential types, GADTs, higher kinded types, rank-n polymorphism, etc. You can even use it to do record types, polymorphic variants, modules, refinement types, etc. The dependent function type is a universal lego block for types. Even more striking, it unifies the type level with the value level. Instead of having a language of types and a language of expressions there is just one language. The type List<T> takes a type T and gives you the type of lists with elements of type T. In dependently typed languages this is just a function List(T) that takes a type and returns a type. Instead of having F<T> at the type level and f(x) at the value level, there's only one kind of function that does both. I have no doubt that we will eventually be programming in a dependently typed language, the only question is when.
  - mafribe 11y ago
    I have no doubt that we will eventually be programming in a dependently typed language, the only question is when. For the reasons I give in another posting in this thread (inability to extend dependent types beyond pure functions, and forcing the full cost of verification on early states of software productions when specifications are unstable), I predict the opposite: dependently typed verification will give way to program logic, the only question is when.
    - jules 11y ago
      Why would dependent types not extend beyond pure functions? Idris has both dependent types and non pure functions, is that not satisfactory? The fact that you can write software that provably satisfies a strict specification in dependently typed languages doesn't mean that you must. It is perfectly possible to program in them like you would in a normal language. That's what I was trying to get at: dependent types are also more expressive, not just more constraining. Now that I know about dependent types I regularly run into situations where I think "gosh, if I had dependent types I wouldn't have had to put in these type casts or handle these error cases that I know for sure cannot happen". So even if you ultimately want to reason about your programs using an external program logic (which I predict we do not, but we'll see), then for expressiveness you still want your language to have dependent types for the reason I mentioned above: > Two, type system researchers promote provably correct programming as the advantage of dependent types. IMO the far more important advantage of dependent types is expressiveness and simplicity: they generalize a vast swath of different type system features and extensions to a handful of simple constructs. Furthermore, if you want it's possible to use a program logic style of verification in a dependent type system. You can write your program as normal and later prove lemmas about functions in the program. For instance instead of saying reverse : Vec n a -> Vec n a or reverse : (xs : List a) -> {ys : List a | length xs == length ys} you can do reverse : List a -> List a and a lemma reverse_preserves_length : forall xs. length (reverse xs) == length xs It's just not the only option you have. What's this forall you say? A dependent function type of course!
- lmm 11y ago
  I've been doing Scala for 5+ years, real-world production code. From here it feels like the popularity of types is going up and up (and within Scala they're becoming more popular e.g. look at doobie). Haskell and OCaml look to be getting more popular, not less. Javascript is a special case because of the browser. Go is mostly displacing Python and Ruby. There's certainly no exodus of ex-Haskell programmers fleeing for less typed languages.
wyager 11y ago
I think the article mixes up "type" and "newtype". "newtype Email = String" doesn't make sense.
- gizmo686 11y ago
  "type" wouldn't work in this context, as it is literally just an alias, so the compiler cannot use to determine what instance to use. In contrast, newtype actually creates a new type, that acts as a wrapper around the old type. I believe what the author meant to say was "newtype Email = Email String".
eru 11y ago
There's some template Haskell magic that generates QuickCheck properties for the typeclass laws for your instances for you. That's taking care of some of the article's worries.
- nicolast 11y ago
  No need for TH, actually. Write a function which takes a `proxy a` and returns e.g. a Tasty `TestTree`: `testMyClassLaws :: proxy a -> TestTree`. Then in your test module, add something like `testGroup "MyClassLaws for MyType" $ testMyClassLaws (Proxy :: Proxy MyType)` somewhere in your list of tests.
jules 11y ago
The requirement to be globally unambiguous is the #1 wart of type classes. Rather than enforcing it with the compiler it would be better to make that restriction unnecessary. It should be possible to define a type class instance local to a module. Locally unambiguous yes, globally unambiguous no.
- Kutta 11y ago
  That's not good. We can put an instance into a runtime box, pass it to another module, and now there are potentially two different instances to choose from in the other module. We'd have to ban moving around instances in runtime data if we are to preserve class coherence, which is unsatisfactory.
  - jules 11y ago
    > and now there are potentially two different instances to choose from in the other module [...] to preserve class coherence I know the standard arguments for class coherence (Set etc.), but I haven't found any of them convincing. Relying on two values coming from two different places to be the same indicates that the design of the code is wrong. It's like writing a function f x y but you must only ever call it with identical arguments x=y. The right thing to do then is to give f only one argument to begin with.
    - Kutta 11y ago
      I consider coherence seriously mainly because Edward Kmett supports it, and he has immense experience regarding the relative merits of coherent vs. incoherent classes in practical development. One core Kmett argument that I subscribe to is that 95% percent of the time there is no newtype noise needed, and in that case coherence is very nice, since one doesn't have to think about class hierarchies (which can get very complex, with many alternate instance derivations) as far as the code typechecks. But aside of that, I'm not all that convinced of the importance of coherence in a dependent setting either! My intuition is that types should encode all the properties that we'd like to be able to use in instances. In other words, even if we don't get coherence, we can use types to constrain the implementation of instances as much as we like. Highly ambiguous instance resolution (like a bunch of Monoid Int instances lying around) is a bit of a pain though, and there could be some "using instance" feature/syntax that locally throws out all instances except one. Additionally, as of now there are no large production code bases that use Coq style type classes in a proper dependent language. There are very few sizable applications in dependent languages to begin with. So we don't know a lot about the practical caveats of that design, while there is a lot of experience and know-how about Haskell-style classes, which is one reason why we should at least consider salvaging coherence in future languages. Generally, I think that type classes are a rather ugly and haphazard construction compared to the succinct elegance of the type theories of core languages; still, eventually type classes worm their way into languages (Agda, Coq) because people really like them and like to use them, so a language designer should consider them. I wish there was an elegant/general formal treatment that captures the essential features, in any case.
joseraul 11y ago
Note the weakness of the Java solution. Since its interfaces offer no support for virtual contructors (hence the design pattern), you have to instanciate a factory before you can get an empty value.
- kushti 11y ago
  Possible now with Java 8 default methods.
joostdevries 11y ago
John de Goes mentions at the start of his article how Scala implements type classes without an extra language construct. But he doesn't show what his example would look like in Scala. So I wrote that out for my own amusement. You can find the gist here. https://gist.github.com/joost-de-vries/949fbea6345fec1ac4ef https://gist.github.com/joost-de-vries/949fbea6345fec1ac4ef
dwenzek 11y ago
An alternative approach is under development [1] for OCaml : modular implicits [2]. This is a mix of ideas from SML/OCaml modules, Scala implicits and Haskell type classes. More than one alternative module implementation may be provided for a module signature, and the actual implementation to be used is chosen on the implicit modules available in the current context. This results into an error if the implicit module cannot be chosen without ambiguity. [1] https://github.com/ocamllabs/ocaml-modular-implicits https://github.com/ocamllabs/ocaml-modular-implicits [2] http://www.lpw25.net/ml2014.pdf http://www.lpw25.net/ml2014.pdf
- Kutta 11y ago
  (very similar systems are already implemented in Agda and Coq)
Kutta 11y ago
This post engages in plenty of armchair speculation, and is overall horribly vague, or just nonsense ("addOneTwo works on any type that’s provably isomorphic to Integer"). It's more like a plea for all things that seem intuitively nice and good, mashed together without any deep consideration for whether they can be realized consistently. Type classes are still an open research topic, especially when combined with dependent types. From the top of my head: Class coherence is the property that any two instances of the same types are equal. It's a strong guarantee that boosts the robustness and usability of type classes significantly. Scala doesn't have it, instead it has a arcane set of rules that determine the resolution of implicits in the face of ambiguity, and it's a huge pain for more complicated use cases. Named instances are incompatible with coherence. We could just put one named instance into a runtime object, and voila, it's indistinguishable from any other instance. We could remedy this by indexing the type of an instance with a label, which isn't better than choosing instances with newtype wrappers. Similarly, local instances and explicit instance application imply incoherence. Also, laws for classes are an already existing feature in Idris, Agda and Coq. The problem is that laws for anything are by far best realized via dependent types, and dependent types have a nontrivial interaction with classes that is an open problem. With dependent types, checking whether two instance heads are different could be just undecidable, depending on what constructs one allows there. It's a possibility to neuter the language fragment that goes into instance heads, so that propositional equality becomes decidable over it - in a way Haskell already does this, by disallowing type families in instances. But in a dependent language it could be rather awkward that a fair amount of useful types cannot be made instances. Alternatively, one could require proofs from the programmer in each instance that the instance head is propositionally different from all other instance heads in scope. But this would also require much thought, and I haven't given it yet. Also, if our classes are actually coherent, we would like to have an internal proof of this property (as opposed to in current Haskell where we just sort of know that this is the case), but I have no idea how to do this best. Maybe the instance resolution procedure could be modeled internally in a strong enough language, and coherence could be given as a theorem, and there could be some syntactic sugar for code with classes. Or we could have both coherent and incoherent classes, each explicitly marked as such. Or we could have coherent classes by proving that a certain class is necessarily coherent, independently from any instance resolution procedure. There are many such classes, but not nearly all that we frequently use, and some classes are coherent but we can't prove it in currently implemented type theories because the proof relies on parametricity (Functor is such a class).
jonsterling 11y ago
There are a number of good points here, but I am surprised by the fact that John wants a global coherence check, since in our conversations he has always insisted on the primacy of local reasoning.
pcwalton 11y ago
It's interesting to contrast this with the attitude in the D community (or at least Andrei and Walter), which has also come to the conclusion that typeclasses are a bad idea–but because they're too strongly typed rather than not strongly typed enough, and the solution is to throw them out in favor of dynamic "typing" at the type level through ad-hoc templates. My two cents is that this is just like every other static vs. dynamic typing debate, and it's a deep tradeoff. I've been pretty pleased with typeclasses as an easy-to-use sweet spot between complexity/mental overhead and safety. But I'm certainly willing to believe we can do better, of course.

97 points by andars 11y ago

Has anyone here shipped anything production worthy with dependently typed languages? I'm serious. There are like 10 PhDs in France working on a certified compiler toolchain for C and that's it. Meanwhile Go and JavaScript are taking over the world and they're anything but dependently typed. Maybe there's a reason for that? Maybe the reason is that after a certain point the validation overhead of advanced type systems is just not worth it. Yes, I know the article isn't about dependent types per se but many of the features he wants get pretty close to dependent types since that is pretty much the state of the art when it comes to advanced type systems with lawful abstractions and whatnot.

Ixiaus 11y ago
I'm shipping massive amounts of code written in Haskell - production worthy for a real product - and the benefits of using Haskell over any other mainstream imperative language have been fairly significant.
- Drup 11y ago
  Haskell is not a real dependently type language. It may tries to quack like one, but compared to Idris/Agda, it's doing a very bad job at it. I'm pretty sure Parent didn't included Haskell.
  - wyager 11y ago
    Haskell has decent experimental support for dependent types. I've been using the CLaSH Haskell to hardware conversion system, which makes heavy use of type level arithmetic, with pretty good results.
    - Drup 11y ago
      Type level arithmetic is sugar for clever GADTs, not full blown dependent types. Try to do things in Agda/Idris and come back to haskell, the expressiveness is not nearly comparable.
      - wyager 11y ago
        Are Nats in agda and idris not also just GADT based peano numbers?
        Drup 11y ago
        The toyish version showed in tutorials, yes. The real stuff, no, it's just .. integers. And anyway, my point was that you can do much much more than type level arithmetic.
  - Ixiaus 11y ago
    His comparison sounded much more like "research languages vs. mainstream imperative languages" and Haskell definitely came from research land, just as Idris and Agda are. Plus someone is seriously working on dependent types in Haskell - so no, I think it's fitting.
jjaredsimpson 11y ago
The value proposition I've always read is related to gains in expressiveness and correctness. Programming is eventually going to become like Advanced Chess (human+computer team) and entire classes of mistakes will cease to exist. I don't think I can be convinced that correct-by-construction methods are wrongheaded. I am convinced that humans aren't very good at wrangling precise and complex and large ideas without failure.
Drup 11y ago
Does selling CompCert to Airbus count as begin "production worthy" ? I would (not) be amused when people try to put javascript in plane navigation systems. Do not forget that most dependently type languages (and Coq the first) are proof languages. The goal is not (only) to write programs, but to prove things and a rather large number of theorem have been proven that way. Dependently types languages for programming (as opposed to proving) are very much cutting edge research. Is it so surprising that they are not used in the wild ? Edit: woops, missed the "here" in parent's comment. No, I don't work on compcert. :)
- theseoafs 11y ago
  > Dependently types languages for programming (as opposed to proving) are very much cutting edge research. Is it so surprising that they are not used in the wild ? How long will this be the case? Seems like they've been "cutting edge research" for a few decades, and the Curry-Howard correspondence itself is like 80 years old. Surely if there were a real demand for these kinds of programming languages, we would have seen some industry penetration at some point, right?
  - tunesmith 11y ago
    There's been plenty of industry penetration for languages with more advanced type systems. Not sure why there's the arbitrary line being drawn here of dependent type systems. Some of this is about the penetration of certain ideas. Like, we had to wait for multiple cores on commodity hardware before functional programming started to cross over from the academic community to the professional web programmer. That shift helps your average programmer to think a bit more mathematically, and then it's basically about whether the programmer starts to appreciate types - and to me that seems to be less about purity of argument than the professional atmosphere the programmer is in. Are you prototyping and moving fast and breaking stuff, or are you caring more about longevity and correctness. And then once you start getting more into static typing and functional programming, a lot of these other ideas start to become more attractive and intriguing. It's like a lot of ideas that circulate around for a long time before they really take hold; you're waiting for a certain critical mass of system inputs and momentum, and then things can start to change really fast.
mmarx 11y ago
The formally-verified Odd Order Theorem[0] using Coq was quite an acomplishment (though probably not what you had in mind). [0] https://hal.inria.fr/hal-00816699/file/main.pdf https://hal.inria.fr/hal-00816699/file/main.pdf
incepted 11y ago
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).
mafribe 11y ago
after a certain point the validation overhead of advanced type systems is just not worth it. But what makes you think you need dependent types to do full specification and verification of a program? Instead you could use program logic. Write the program in any language you like and later, when it the program is finished verifiy that it meets its specification using program logic. This separates programming from verification completely. In my opinion this is the future of certified programming. Dependent types are too heavyweight to support any conventional programming process. Another advantage is that unlike Curry-Howard based verification, program logic does not have to be constructive, instead you can use classical reasoning with excluded middle. This tends to yield shorter proofs. See Microsoft's Daphny [1] or CFML [2] for prototype tool chains implementing program logic based verification. Facebook's infer tool [3], while not allowing full verification, is also based on program logic. [1] http://research.microsoft.com/en-us/projects/dafny http://research.microsoft.com/en-us/projects/dafny [2] http://www.chargueraud.org/softs/cfml http://www.chargueraud.org/softs/cfml [3] https://github.com/facebook/infer https://github.com/facebook/infer
- darzu 11y ago
  > This separates programming from verification completely. This is simply not the case. Significant verification projects always plan for verification and do verification in tandem. This is definitely true for all Dafny projects to date as well. Verification is just so much harder than unverified programming that you generally want to do everything you can while programming to make verification easier. This may become less true as proof automation improves but it will always be a tension. > But what makes you think you need dependent types to do full specification [...] ? Also, keep in mind that Dafny and similar tools can only express first order logic; this can significantly restricts the expressiveness of your specification language and intermediate lemmas. > program logic does not have to be constructive, instead you can use classical reasoning with excluded middle. This is a silly point. First off proof assistants like Coq aren't inconsistent with the law of the excluded middle (only NuPRL is I believe) so you can always assume it as an axiom if you'd like. Most projects don't do this because constructivism is a benefit not a burden in verification: it allows you to make distinctions that aren't possible in classical logic. I agree that Dafny and similar projects are very exciting though; Dafny's tight integration with Z3 provides an awesome level of automation that will keep getting better and better.
darzu 11y ago
True certified programming has a lot of overhead but there are definitely areas where it'll be worth it: medical devices, car systems, mars rovers, aviation, etc. The University of Washington is actively working on verifying radiation therapy machine software and early results are already used in production for example. I think the reason certified programming hasn't been more widely adopted yet is because the tooling is terrible at the moment and we still have some important bits of theory to work out (e.g. homotopy type theory & other equality issues). It'll get there. Projects like Lean & Dafny at MSR, Adam Chlipala's work at MIT, and the large amount of theory work being done at CMU, Cornell, UPenn, Inria and other places are very promising. My bet is that the tooling & theory will continue to improve and eventually the overhead will become low enough that a significant portion (~10-20%) of software will be certified. I recommend reading Adam Chlipala's vision statement for inspiration on what certified programming could enable: http://adam.chlipala.net/summary.html http://adam.chlipala.net/summary.html
jules 11y ago
The reason is twofold. One, research into dependent types is still ongoing. Two, type system researchers promote provably correct programming as the advantage of dependent types. IMO the far more important advantage of dependent types is expressiveness and simplicity: they generalize a vast swath of different type system features and extensions to a handful of simple constructs. Well, arguably just a single construct: it generalizes the usual function type A -> B to the dependent function type x:A -> B(x). This subsumes a lot of things like generics, existential types, GADTs, higher kinded types, rank-n polymorphism, etc. You can even use it to do record types, polymorphic variants, modules, refinement types, etc. The dependent function type is a universal lego block for types. Even more striking, it unifies the type level with the value level. Instead of having a language of types and a language of expressions there is just one language. The type List<T> takes a type T and gives you the type of lists with elements of type T. In dependently typed languages this is just a function List(T) that takes a type and returns a type. Instead of having F<T> at the type level and f(x) at the value level, there's only one kind of function that does both. I have no doubt that we will eventually be programming in a dependently typed language, the only question is when.
- mafribe 11y ago
  I have no doubt that we will eventually be programming in a dependently typed language, the only question is when. For the reasons I give in another posting in this thread (inability to extend dependent types beyond pure functions, and forcing the full cost of verification on early states of software productions when specifications are unstable), I predict the opposite: dependently typed verification will give way to program logic, the only question is when.
  - jules 11y ago
    Why would dependent types not extend beyond pure functions? Idris has both dependent types and non pure functions, is that not satisfactory? The fact that you can write software that provably satisfies a strict specification in dependently typed languages doesn't mean that you must. It is perfectly possible to program in them like you would in a normal language. That's what I was trying to get at: dependent types are also more expressive, not just more constraining. Now that I know about dependent types I regularly run into situations where I think "gosh, if I had dependent types I wouldn't have had to put in these type casts or handle these error cases that I know for sure cannot happen". So even if you ultimately want to reason about your programs using an external program logic (which I predict we do not, but we'll see), then for expressiveness you still want your language to have dependent types for the reason I mentioned above: > Two, type system researchers promote provably correct programming as the advantage of dependent types. IMO the far more important advantage of dependent types is expressiveness and simplicity: they generalize a vast swath of different type system features and extensions to a handful of simple constructs. Furthermore, if you want it's possible to use a program logic style of verification in a dependent type system. You can write your program as normal and later prove lemmas about functions in the program. For instance instead of saying reverse : Vec n a -> Vec n a or reverse : (xs : List a) -> {ys : List a | length xs == length ys} you can do reverse : List a -> List a and a lemma reverse_preserves_length : forall xs. length (reverse xs) == length xs It's just not the only option you have. What's this forall you say? A dependent function type of course!
lmm 11y ago
I've been doing Scala for 5+ years, real-world production code. From here it feels like the popularity of types is going up and up (and within Scala they're becoming more popular e.g. look at doobie). Haskell and OCaml look to be getting more popular, not less. Javascript is a special case because of the browser. Go is mostly displacing Python and Ruby. There's certainly no exodus of ex-Haskell programmers fleeing for less typed languages.

wyager 11y ago

I think the article mixes up "type" and "newtype". "newtype Email = String" doesn't make sense.

gizmo686 11y ago
"type" wouldn't work in this context, as it is literally just an alias, so the compiler cannot use to determine what instance to use. In contrast, newtype actually creates a new type, that acts as a wrapper around the old type. I believe what the author meant to say was "newtype Email = Email String".

eru 11y ago

There's some template Haskell magic that generates QuickCheck properties for the typeclass laws for your instances for you. That's taking care of some of the article's worries.

nicolast 11y ago
No need for TH, actually. Write a function which takes a `proxy a` and returns e.g. a Tasty `TestTree`: `testMyClassLaws :: proxy a -> TestTree`. Then in your test module, add something like `testGroup "MyClassLaws for MyType" $ testMyClassLaws (Proxy :: Proxy MyType)` somewhere in your list of tests.

jules 11y ago

The requirement to be globally unambiguous is the #1 wart of type classes. Rather than enforcing it with the compiler it would be better to make that restriction unnecessary. It should be possible to define a type class instance local to a module. Locally unambiguous yes, globally unambiguous no.

Kutta 11y ago
That's not good. We can put an instance into a runtime box, pass it to another module, and now there are potentially two different instances to choose from in the other module. We'd have to ban moving around instances in runtime data if we are to preserve class coherence, which is unsatisfactory.
- jules 11y ago
  > and now there are potentially two different instances to choose from in the other module [...] to preserve class coherence I know the standard arguments for class coherence (Set etc.), but I haven't found any of them convincing. Relying on two values coming from two different places to be the same indicates that the design of the code is wrong. It's like writing a function f x y but you must only ever call it with identical arguments x=y. The right thing to do then is to give f only one argument to begin with.
  - Kutta 11y ago
    I consider coherence seriously mainly because Edward Kmett supports it, and he has immense experience regarding the relative merits of coherent vs. incoherent classes in practical development. One core Kmett argument that I subscribe to is that 95% percent of the time there is no newtype noise needed, and in that case coherence is very nice, since one doesn't have to think about class hierarchies (which can get very complex, with many alternate instance derivations) as far as the code typechecks. But aside of that, I'm not all that convinced of the importance of coherence in a dependent setting either! My intuition is that types should encode all the properties that we'd like to be able to use in instances. In other words, even if we don't get coherence, we can use types to constrain the implementation of instances as much as we like. Highly ambiguous instance resolution (like a bunch of Monoid Int instances lying around) is a bit of a pain though, and there could be some "using instance" feature/syntax that locally throws out all instances except one. Additionally, as of now there are no large production code bases that use Coq style type classes in a proper dependent language. There are very few sizable applications in dependent languages to begin with. So we don't know a lot about the practical caveats of that design, while there is a lot of experience and know-how about Haskell-style classes, which is one reason why we should at least consider salvaging coherence in future languages. Generally, I think that type classes are a rather ugly and haphazard construction compared to the succinct elegance of the type theories of core languages; still, eventually type classes worm their way into languages (Agda, Coq) because people really like them and like to use them, so a language designer should consider them. I wish there was an elegant/general formal treatment that captures the essential features, in any case.

joseraul 11y ago

Note the weakness of the Java solution. Since its interfaces offer no support for virtual contructors (hence the design pattern), you have to instanciate a factory before you can get an empty value.

kushti 11y ago
Possible now with Java 8 default methods.

joostdevries 11y ago

John de Goes mentions at the start of his article how Scala implements type classes without an extra language construct. But he doesn't show what his example would look like in Scala. So I wrote that out for my own amusement. You can find the gist here. https://gist.github.com/joost-de-vries/949fbea6345fec1ac4ef https://gist.github.com/joost-de-vries/949fbea6345fec1ac4ef

dwenzek 11y ago

An alternative approach is under development [1] for OCaml : modular implicits [2]. This is a mix of ideas from SML/OCaml modules, Scala implicits and Haskell type classes. More than one alternative module implementation may be provided for a module signature, and the actual implementation to be used is chosen on the implicit modules available in the current context. This results into an error if the implicit module cannot be chosen without ambiguity. [1] https://github.com/ocamllabs/ocaml-modular-implicits https://github.com/ocamllabs/ocaml-modular-implicits [2] http://www.lpw25.net/ml2014.pdf http://www.lpw25.net/ml2014.pdf

Kutta 11y ago
(very similar systems are already implemented in Agda and Coq)

Kutta 11y ago

This post engages in plenty of armchair speculation, and is overall horribly vague, or just nonsense ("addOneTwo works on any type that’s provably isomorphic to Integer"). It's more like a plea for all things that seem intuitively nice and good, mashed together without any deep consideration for whether they can be realized consistently. Type classes are still an open research topic, especially when combined with dependent types. From the top of my head: Class coherence is the property that any two instances of the same types are equal. It's a strong guarantee that boosts the robustness and usability of type classes significantly. Scala doesn't have it, instead it has a arcane set of rules that determine the resolution of implicits in the face of ambiguity, and it's a huge pain for more complicated use cases. Named instances are incompatible with coherence. We could just put one named instance into a runtime object, and voila, it's indistinguishable from any other instance. We could remedy this by indexing the type of an instance with a label, which isn't better than choosing instances with newtype wrappers. Similarly, local instances and explicit instance application imply incoherence. Also, laws for classes are an already existing feature in Idris, Agda and Coq. The problem is that laws for anything are by far best realized via dependent types, and dependent types have a nontrivial interaction with classes that is an open problem. With dependent types, checking whether two instance heads are different could be just undecidable, depending on what constructs one allows there. It's a possibility to neuter the language fragment that goes into instance heads, so that propositional equality becomes decidable over it - in a way Haskell already does this, by disallowing type families in instances. But in a dependent language it could be rather awkward that a fair amount of useful types cannot be made instances. Alternatively, one could require proofs from the programmer in each instance that the instance head is propositionally different from all other instance heads in scope. But this would also require much thought, and I haven't given it yet. Also, if our classes are actually coherent, we would like to have an internal proof of this property (as opposed to in current Haskell where we just sort of know that this is the case), but I have no idea how to do this best. Maybe the instance resolution procedure could be modeled internally in a strong enough language, and coherence could be given as a theorem, and there could be some syntactic sugar for code with classes. Or we could have both coherent and incoherent classes, each explicitly marked as such. Or we could have coherent classes by proving that a certain class is necessarily coherent, independently from any instance resolution procedure. There are many such classes, but not nearly all that we frequently use, and some classes are coherent but we can't prove it in currently implemented type theories because the proof relies on parametricity (Functor is such a class).

jonsterling 11y ago

There are a number of good points here, but I am surprised by the fact that John wants a global coherence check, since in our conversations he has always insisted on the primacy of local reasoning.

pcwalton 11y ago

It's interesting to contrast this with the attitude in the D community (or at least Andrei and Walter), which has also come to the conclusion that typeclasses are a bad idea–but because they're too strongly typed rather than not strongly typed enough, and the solution is to throw them out in favor of dynamic "typing" at the type level through ad-hoc templates. My two cents is that this is just like every other static vs. dynamic typing debate, and it's a deep tradeoff. I've been pretty pleased with typeclasses as an easy-to-use sweet spot between complexity/mental overhead and safety. But I'm certainly willing to believe we can do better, of course.