7 ms·

Why didn't refinement types find their way into mainstream languages yet? It seems like it would have a tremendous impact on how programs are written and tested

Why didn't refinement types find their way into mainstream languages yet? It seems like it would have a tremendous impact on how programs are written and tested.

pjmlp 9y ago
Because major organizations only want replaceable developers, as cogs in the enterprise machine. Better quality of software is irrelevant unless they get fined, like it happens on medicine or aeronautics industry.
- ainar-g 9y ago
  If anything, I would say refinement types make developers more replaceable. If Developer-1 documents all assumptions in the code using refinements, then, when they are replaced with Developer-2, the new developer can be productive more quickly.
  - pjmlp 9y ago
    I agree with you, but most managers don't. They only care about cost centers, Excel reports and who delivers at lower cost per seat.
- kakarot 9y ago
  Those "major organizations", with the exception of Google and Apple, aren't spearheading language design. Their point of view has no impact on the evolution of language paradigms, and if you told them they could save money on QA and increase the reliability of their product for virtually no overhead with new paradigms, I don't see why many people would reject the idea.
  - pjmlp 9y ago
    Google, as in Go? "Type system tyranny", page 8 - https://talks.golang.org/2009/go_talk-20091030.pdf https://talks.golang.org/2009/go_talk-20091030.pdf "Programmers working at Google are early in their careers and are most familiar with procedural languages, particularly from the C family. The need to get programmers productive quickly in a new language means that the language cannot be too radical." https://talks.golang.org/2012/splash.article https://talks.golang.org/2012/splash.article
    - fauigerzigerk 9y ago
      This is a convenient explanation and you will find a lot of evidence for it, but I think it's superficial. The real question is, why can they afford to take this approach without being outperformed by companies that use better languages and better developers? For those of us who enjoy exploring more powerful/innovative languages, there is a convenient explanation and a not so convenient explanation. The convenient one is that the success of these "Blub companies" is largely determined by factors unrelated to software development. The inconvenient one is that all these interesting and powerful language features do not significantly improve software development outcomes. I think it is remarkable that some of the companies that are on the Blub side when it comes to software development are among the most cutting edge, research oriented companies in other regards, such as AI. Also, companies like Google can not only choose among the best candidates, they also have a lot of influence on what people learn before they even apply for a job there. So I simply don't buy the familiarity excuse, at least not for the entire workforce. I also don't buy the large existing codebase excuse as that would apply equally to new Blub languages and new PL research based languages. There is simply very little faith in any positive impact of PL research innovations on software development outcomes. And this lack of faith cannot be explained away by claiming that all those lacking faith are simply incompetent. The likes of Google and Microsoft can and do hire competent PL researchers, just as they hire competent AI researchers. And they do have a massive incentive to improve software development quality and productivity. I think the truth is that PL researchers simply haven't made the case for the effectiveness of their work. In part because it's extremely difficult to make that case empirically. All the empirical studies I have seen suffer from huge and mostly unfixable counfounders. But I think another reason is that PL researchers seem to largely ignore cognitive science and sociology. I haven't seen much discussion about the impact of particular PL features on developers' state of mind in any realistic context. Nor have I seen much debate about programming languages as group communication tools or about the different roles in which people interact with code as part of a software development process. All of that is apparently considered out of scope. And that, I think, is the reason why it is so easy for many practitioners to dismiss PL research out of hand. Even where PL research is being picked up decades later it appears more fashion driven than evidence based.
      - 9y ago
  - davidgrenier 9y ago
    I may misunderstand your statement, you seem to be saying Google and Apple ARE spearheading language design? If so, you must be very confused with what they are doing with Go and Swift and Dart if you still consider that a thing.
    - kakarot 9y ago
      I should have expanded a bit more. They are spearheading the design of a language or a few languages, and thus have skin in the game. I didn't mean to imply that they are spearheading language design in general.
- mcguire 9y ago
  To an extent. My feeling is that developers themselves, in general, don't want to learn anything more complicated than they can pick up from a three-month bootcamp and certainly don't want to take on the responsibility for their errors.
badsectoracula 9y ago
Doesn't Ada have something like this?
- pjmlp 9y ago
  Kind of, you can achieve something similar with SPARK.
- tom_mellior 9y ago
  AFAIK Ada's "refinement types" are essentially ranged integer types, i.e., you can define type Int is range 0 .. 100; and it will be impossible to store any number outside that range in a variable of this type. But you can't define more general properties than this.
  - mcguire 9y ago
    In general Ada, those are only checked at runtime, IIRC.
    - junke 9y ago
      Types are checked by names, even you have the same underlying range of values. But some checks can only be done at runtime.
  - badsectoracula 9y ago
    Pascal also has this, but i remember some Ada-related post from a few months ago here that had code along the lines of (imaginary syntax, i don't remember the exact code): type Int is range 0 .. 100 check(v) if (v = 10) or (v = 50) then error; end; That would allow all values of v between 0 and 100, except 10 and 50. Note that everything after (and including) "check" is something i came up (and is more Pascal-ish), not what i am talking about. I also remember that this could be used with objects so that you could have something like (this one is Object Pascal-ish, i do not know Ada): type Foo = object Enabled : Boolean; Magnitude : 0..1000; check if (Enabled and (Magnitude=0)) or (not Enabled and (Magnitude > 0)) then error; end; procedure Bar; end; The code in check would be called whenever the object changes externally, so "Bar" can change Enabled and Magnitude with the check being invoked only at the exit of Bar to ensure object consistency and not whenever Bar does the assignment (so it can do a Enabled:=False; Magnitude:=0; and not fail at the first assignment), but assigning those values directly from outside the object would trigger it (so having a var f: Foo; and then writing f.Enabled:=True; would trigger the error). Or at least that is what i remember understanding. Maybe i remember some other Pascal-styled language, but the only other such language i know of is Oberon and that goes against the "put everything imaginable, plus extra more" mentality of Ada seems to have :-P.
johncolanduoni 9y ago
I find it even more frustrating that some mainstream languages accept all the complexity of dependent typing while restricting the benefits by hiding it deep within an ad-hoc construction (C++ and Scala are both guilty of this).
- hellohn123 9y ago
  Genuinely curious; can you elaborate which benefits the C++ implementation is missing out on?
- Peaker 9y ago
  C++ and Scala don't really have dependent typing, but rather a single feature that is typical of dependent typing. That is: type-level values of any type.
  - taejo 9y ago
    Doesn't C++ only have type-level integers (as template parameters)? Are you referring to something else?
    - Peaker 9y ago
      I haven't used C++ in years. That may be true. In that case, it may be even more puzzling to claim that C++ has dependent types.
  - johncolanduoni 9y ago
    Both Scala and C++ have a set of type-system features that when combined allow you create functions whose return type can depend on the value of the passed argument. For a good step by step of how to do this in Scala see here[1], and a (unfortunately less in depth) C++ example is here[2]. [1]: http://gigiigig.github.io/tlp-step-by-step/dependent-types.html http://gigiigig.github.io/tlp-step-by-step/dependent-types.h... [2]: https://www.reddit.com/r/cpp/comments/2tilfw/dependent_typing_in_c/ https://www.reddit.com/r/cpp/comments/2tilfw/dependent_typin...
tom_mellior 9y ago
Statically checking refinements still only works so-so, that is, what do you do when the SMT solver times out? Writing manual proofs (or proof fragments) is great for special-purpose languages used by highly trained people, but it's not quite ready for the mainstream yet. Checking refinements at run time is considered "too expensive" by many people.
- saosebastiao 9y ago
  I use the Refined library for scala and it works incredibly well (a few bumps here or there, and some occasional boilerplate for library interop). On my app server, it basically becomes my validation layer for all request data, after which I only worry about object ownership/authorization. The big win with refined types is from compiler level support though. With relatively simple checking occurring mostly at IO boundaries, you can eliminate or make obsolete massive portions of testing, type checking, manual optimization, etc., and enable massive amounts of automated optimization. In other words, the "too expensive" refinement checking at runtime becomes a net performance and engineering benefit over the whole product lifecycle.
- floatboth 9y ago
  Runtime refinements are actually useful for places where you'd have checks anyway. E.g. in Haskell, this library http://nikita-volkov.github.io/refined/ http://nikita-volkov.github.io/refined/ — can be integrated with JSON: https://github.com/myfreeweb/magicbane/blob/7c417504590fc40ecd37a61e3c3a80640eb4d8dd/library/Magicbane/Validation.hs https://github.com/myfreeweb/magicbane/blob/7c417504590fc40e... — and you get input validation specified right in the types of your data structures.

Why didn't refinement types find their way into mainstream languages yet? It seems like it would have a tremendous impact on how programs are written and tested.

pjmlp 9y ago

Because major organizations only want replaceable developers, as cogs in the enterprise machine. Better quality of software is irrelevant unless they get fined, like it happens on medicine or aeronautics industry.

ainar-g 9y ago
If anything, I would say refinement types make developers more replaceable. If Developer-1 documents all assumptions in the code using refinements, then, when they are replaced with Developer-2, the new developer can be productive more quickly.
- pjmlp 9y ago
  I agree with you, but most managers don't. They only care about cost centers, Excel reports and who delivers at lower cost per seat.
kakarot 9y ago
Those "major organizations", with the exception of Google and Apple, aren't spearheading language design. Their point of view has no impact on the evolution of language paradigms, and if you told them they could save money on QA and increase the reliability of their product for virtually no overhead with new paradigms, I don't see why many people would reject the idea.
- pjmlp 9y ago
  Google, as in Go? "Type system tyranny", page 8 - https://talks.golang.org/2009/go_talk-20091030.pdf https://talks.golang.org/2009/go_talk-20091030.pdf "Programmers working at Google are early in their careers and are most familiar with procedural languages, particularly from the C family. The need to get programmers productive quickly in a new language means that the language cannot be too radical." https://talks.golang.org/2012/splash.article https://talks.golang.org/2012/splash.article
  - fauigerzigerk 9y ago
    This is a convenient explanation and you will find a lot of evidence for it, but I think it's superficial. The real question is, why can they afford to take this approach without being outperformed by companies that use better languages and better developers? For those of us who enjoy exploring more powerful/innovative languages, there is a convenient explanation and a not so convenient explanation. The convenient one is that the success of these "Blub companies" is largely determined by factors unrelated to software development. The inconvenient one is that all these interesting and powerful language features do not significantly improve software development outcomes. I think it is remarkable that some of the companies that are on the Blub side when it comes to software development are among the most cutting edge, research oriented companies in other regards, such as AI. Also, companies like Google can not only choose among the best candidates, they also have a lot of influence on what people learn before they even apply for a job there. So I simply don't buy the familiarity excuse, at least not for the entire workforce. I also don't buy the large existing codebase excuse as that would apply equally to new Blub languages and new PL research based languages. There is simply very little faith in any positive impact of PL research innovations on software development outcomes. And this lack of faith cannot be explained away by claiming that all those lacking faith are simply incompetent. The likes of Google and Microsoft can and do hire competent PL researchers, just as they hire competent AI researchers. And they do have a massive incentive to improve software development quality and productivity. I think the truth is that PL researchers simply haven't made the case for the effectiveness of their work. In part because it's extremely difficult to make that case empirically. All the empirical studies I have seen suffer from huge and mostly unfixable counfounders. But I think another reason is that PL researchers seem to largely ignore cognitive science and sociology. I haven't seen much discussion about the impact of particular PL features on developers' state of mind in any realistic context. Nor have I seen much debate about programming languages as group communication tools or about the different roles in which people interact with code as part of a software development process. All of that is apparently considered out of scope. And that, I think, is the reason why it is so easy for many practitioners to dismiss PL research out of hand. Even where PL research is being picked up decades later it appears more fashion driven than evidence based.
    - 9y ago
- davidgrenier 9y ago
  I may misunderstand your statement, you seem to be saying Google and Apple ARE spearheading language design? If so, you must be very confused with what they are doing with Go and Swift and Dart if you still consider that a thing.
  - kakarot 9y ago
    I should have expanded a bit more. They are spearheading the design of a language or a few languages, and thus have skin in the game. I didn't mean to imply that they are spearheading language design in general.
mcguire 9y ago
To an extent. My feeling is that developers themselves, in general, don't want to learn anything more complicated than they can pick up from a three-month bootcamp and certainly don't want to take on the responsibility for their errors.

badsectoracula 9y ago

Doesn't Ada have something like this?

pjmlp 9y ago
Kind of, you can achieve something similar with SPARK.
tom_mellior 9y ago
AFAIK Ada's "refinement types" are essentially ranged integer types, i.e., you can define type Int is range 0 .. 100; and it will be impossible to store any number outside that range in a variable of this type. But you can't define more general properties than this.
- mcguire 9y ago
  In general Ada, those are only checked at runtime, IIRC.
  - junke 9y ago
    Types are checked by names, even you have the same underlying range of values. But some checks can only be done at runtime.
- badsectoracula 9y ago
  Pascal also has this, but i remember some Ada-related post from a few months ago here that had code along the lines of (imaginary syntax, i don't remember the exact code): type Int is range 0 .. 100 check(v) if (v = 10) or (v = 50) then error; end; That would allow all values of v between 0 and 100, except 10 and 50. Note that everything after (and including) "check" is something i came up (and is more Pascal-ish), not what i am talking about. I also remember that this could be used with objects so that you could have something like (this one is Object Pascal-ish, i do not know Ada): type Foo = object Enabled : Boolean; Magnitude : 0..1000; check if (Enabled and (Magnitude=0)) or (not Enabled and (Magnitude > 0)) then error; end; procedure Bar; end; The code in check would be called whenever the object changes externally, so "Bar" can change Enabled and Magnitude with the check being invoked only at the exit of Bar to ensure object consistency and not whenever Bar does the assignment (so it can do a Enabled:=False; Magnitude:=0; and not fail at the first assignment), but assigning those values directly from outside the object would trigger it (so having a var f: Foo; and then writing f.Enabled:=True; would trigger the error). Or at least that is what i remember understanding. Maybe i remember some other Pascal-styled language, but the only other such language i know of is Oberon and that goes against the "put everything imaginable, plus extra more" mentality of Ada seems to have :-P.

johncolanduoni 9y ago

I find it even more frustrating that some mainstream languages accept all the complexity of dependent typing while restricting the benefits by hiding it deep within an ad-hoc construction (C++ and Scala are both guilty of this).

hellohn123 9y ago
Genuinely curious; can you elaborate which benefits the C++ implementation is missing out on?
Peaker 9y ago
C++ and Scala don't really have dependent typing, but rather a single feature that is typical of dependent typing. That is: type-level values of any type.
- taejo 9y ago
  Doesn't C++ only have type-level integers (as template parameters)? Are you referring to something else?
  - Peaker 9y ago
    I haven't used C++ in years. That may be true. In that case, it may be even more puzzling to claim that C++ has dependent types.
- johncolanduoni 9y ago
  Both Scala and C++ have a set of type-system features that when combined allow you create functions whose return type can depend on the value of the passed argument. For a good step by step of how to do this in Scala see here[1], and a (unfortunately less in depth) C++ example is here[2]. [1]: http://gigiigig.github.io/tlp-step-by-step/dependent-types.html http://gigiigig.github.io/tlp-step-by-step/dependent-types.h... [2]: https://www.reddit.com/r/cpp/comments/2tilfw/dependent_typing_in_c/ https://www.reddit.com/r/cpp/comments/2tilfw/dependent_typin...

tom_mellior 9y ago

Statically checking refinements still only works so-so, that is, what do you do when the SMT solver times out? Writing manual proofs (or proof fragments) is great for special-purpose languages used by highly trained people, but it's not quite ready for the mainstream yet. Checking refinements at run time is considered "too expensive" by many people.

saosebastiao 9y ago
I use the Refined library for scala and it works incredibly well (a few bumps here or there, and some occasional boilerplate for library interop). On my app server, it basically becomes my validation layer for all request data, after which I only worry about object ownership/authorization. The big win with refined types is from compiler level support though. With relatively simple checking occurring mostly at IO boundaries, you can eliminate or make obsolete massive portions of testing, type checking, manual optimization, etc., and enable massive amounts of automated optimization. In other words, the "too expensive" refinement checking at runtime becomes a net performance and engineering benefit over the whole product lifecycle.
floatboth 9y ago
Runtime refinements are actually useful for places where you'd have checks anyway. E.g. in Haskell, this library http://nikita-volkov.github.io/refined/ http://nikita-volkov.github.io/refined/ — can be integrated with JSON: https://github.com/myfreeweb/magicbane/blob/7c417504590fc40ecd37a61e3c3a80640eb4d8dd/library/Magicbane/Validation.hs https://github.com/myfreeweb/magicbane/blob/7c417504590fc40e... — and you get input validation specified right in the types of your data structures.