6 ms·

Types Considered Harmful

83 points by joelburget 16y ago

crux_ 16y ago
The project he's working on, http://www.seas.upenn.edu/~harmony/ http://www.seas.upenn.edu/~harmony/, is one I've been half-paying-attention to for a while. In particular something like this will (I think) be a perfect substrate for refactoring parsers, semantic diff tools, and other neat stuff...
- joe_the_user 16y ago
  Yes, it's exciting problem. I think it's good he's articulated it. Yet in ways, this paper seems like a confession that he's reached something of a brick wall with the problem. If you look at the bidirectional link, http://lambda-the-ultimate.org/node/1526 http://lambda-the-ultimate.org/node/1526, he goes over a series of partial solutions before discussing his (very general) approach. I suspect that a workable system might be better through putting together all the classes of partial-but-well-behaved solutions rather than attempting a fully general solution. Another thing that interests me is bidirectional code that operates on itself.
  - crux_ 16y ago
    > Yet in ways, this paper seems like a confession that he's reached something of a brick wall with the problem. If "the problem" is that of providing accurate, fully static types for this type of transform, then of course yes. ;) I think the end result is improved (easier to learn and more flexible) for consciously relaxing that goal, however. (Edit to muse: I think 'relaxing' is a far more intelligent & interesting approach to overly-ambitious goals, as opposed to 'abandoning'.)
pgbovine 16y ago
semi off-topic: Prof. Pierce's research group created the Unison bi-directional file synchronizer and open-sourced it. It's a really useful tool that I use literally every single day to keep my files synchronized. Think of it as a predecessor to dropbox, without the UI polish ;) http://www.cis.upenn.edu/~bcpierce/unison/ http://www.cis.upenn.edu/~bcpierce/unison/
- alexgartrell 16y ago
  Additional interesting fact, unison is written in ocaml. Very cool to see interesting systemsy software written in a functional programming language. I'm very excited to peruse it later.
  - JoachimSchipper 16y ago
    Unison also hasn't been updated at all since the original authors stopped working on it, as far as I can tell. It's only one data point, but it does suggest a downside of using ocaml for open source software...
    - Zev 16y ago
      Projects not receiving much love after the original authors give it up isn't unique to projects written in ocaml.
      - agazso 16y ago
        But the probability of discontinuing a project is higher when the language is a less popular one.
stralep 16y ago
Do we want languages where a PhD is required to understand the library documentation? two PhDs for Haskell This presentation is so lighthearted... I realy like it.
- joe_the_user 16y ago
  Yes but the honesty is great. A lot of academic research doesn't acknowledge that the reason a working programmer wants a tool that is really simple is because I am constantly working with the threat of my project becoming overwhelmingly complex. A really simple, clear tool lets me keep a little more distance from that final, looming complexity.
- voxcogitatio 16y ago
  The "You need a PHD to understand Haskell" slur is so bloody ridiculous. I certainly didn't have a problem with it, and I haven't even finished my degree yet! On a more general note, I find the idea that a programming language can be "too smart" troubling. Is the solution to have dumber programming languages then?
  - jedbrown 16y ago
    There is a very big difference between "too smart" and "too complicated". I think Haskell is dangerously close to the former category while C++ is firmly in the second. I appreciate "smart" for many tasks, but sometimes the operational semantics become important (e.g. it's performance-sensitive) and then you have to understand the stack at a pretty deep level and it can be awfully confusing why a tiny source-level change makes a big performance or space difference. Sometimes I pretty much know what assembly I want and it's much easier to make a C compiler produce it than to get GHC to produce it.
    - merijnv 16y ago
      I agree that it is hard to get GHC produce the assembly you want, but I think this is unfair to "blame" GHC for this. In my eyes Haskell is mostly a high-level language and if you worry about the assembler produced I think we have left high-level language territory and it might easier to just write C and use the FFI.
joelburget 16y ago
The author, Benjamin Pierce, also wrote the book Types and Programming Languages, among others. His website: http://www.cis.upenn.edu/~bcpierce/ http://www.cis.upenn.edu/~bcpierce/
jules 16y ago
What's a good introduction to contracts? I'd like to know how a basic contract system works and which extensions are there? What's the relation between contracts and assert?
- limmeau 16y ago
  Provided that to you, a "good introduction" is something with a lambda-calculus extension and a reduction semantics, the 2002 paper by Findler and Felleisen[1] is a good read. 1. http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.11.4081&rep=rep1&type=pdf http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.11....
  - jules 16y ago
    Thanks, that is exactly what I meant :) I also found this one quite interesting: http://www.cs.brown.edu/~arjun/public/poly-contracts.pdf http://www.cs.brown.edu/~arjun/public/poly-contracts.pdf
- Nick_C 16y ago
  If you want introductory, see Bertrand Myer and the Eiffel programming language. http://www.eiffel.com/developers/design_by_contract.html http://www.eiffel.com/developers/design_by_contract.html http://en.wikipedia.org/wiki/Design_by_contract http://en.wikipedia.org/wiki/Design_by_contract http://en.wikipedia.org/wiki/Eiffel_(programming_language) http://en.wikipedia.org/wiki/Eiffel_(programming_language)
voxcogitatio 16y ago
Benjamin Pierce considered troll.
lawnchair_larry 16y ago
Obligatory: "Considered Harmful" Essays Considered Harmful http://meyerweb.com/eric/comment/chech.html http://meyerweb.com/eric/comment/chech.html
6ren 16y ago
With respect to very precise type systems, and coupling between program structure and types, one of the reason mathematics is so powerful is its flexibility I actually have trouble with mathematics, because it is so flexible. For example, equality of sets A and B is typically shown by saying that every element of A is in B, and every element in B is in A. Why on earth do they do that? Why not just say they're the same??! One advantage is it gives you the flexibility to demonstrate the first limb using one technique, and the second limb with a completely unrelated approach. I saw one example of showing equivalence of language defined by a class of grammars, and a language defined by constraints over sequences. You could even use a constructive and a non-constructive proof for each half. It's a way of subdividing that is decoupled.

83 points by joelburget 16y ago

crux_ 16y ago

The project he's working on, http://www.seas.upenn.edu/~harmony/ http://www.seas.upenn.edu/~harmony/, is one I've been half-paying-attention to for a while. In particular something like this will (I think) be a perfect substrate for refactoring parsers, semantic diff tools, and other neat stuff...

joe_the_user 16y ago
Yes, it's exciting problem. I think it's good he's articulated it. Yet in ways, this paper seems like a confession that he's reached something of a brick wall with the problem. If you look at the bidirectional link, http://lambda-the-ultimate.org/node/1526 http://lambda-the-ultimate.org/node/1526, he goes over a series of partial solutions before discussing his (very general) approach. I suspect that a workable system might be better through putting together all the classes of partial-but-well-behaved solutions rather than attempting a fully general solution. Another thing that interests me is bidirectional code that operates on itself.
- crux_ 16y ago
  > Yet in ways, this paper seems like a confession that he's reached something of a brick wall with the problem. If "the problem" is that of providing accurate, fully static types for this type of transform, then of course yes. ;) I think the end result is improved (easier to learn and more flexible) for consciously relaxing that goal, however. (Edit to muse: I think 'relaxing' is a far more intelligent & interesting approach to overly-ambitious goals, as opposed to 'abandoning'.)

pgbovine 16y ago

semi off-topic: Prof. Pierce's research group created the Unison bi-directional file synchronizer and open-sourced it. It's a really useful tool that I use literally every single day to keep my files synchronized. Think of it as a predecessor to dropbox, without the UI polish ;) http://www.cis.upenn.edu/~bcpierce/unison/ http://www.cis.upenn.edu/~bcpierce/unison/

alexgartrell 16y ago
Additional interesting fact, unison is written in ocaml. Very cool to see interesting systemsy software written in a functional programming language. I'm very excited to peruse it later.
- JoachimSchipper 16y ago
  Unison also hasn't been updated at all since the original authors stopped working on it, as far as I can tell. It's only one data point, but it does suggest a downside of using ocaml for open source software...
  - Zev 16y ago
    Projects not receiving much love after the original authors give it up isn't unique to projects written in ocaml.
    - agazso 16y ago
      But the probability of discontinuing a project is higher when the language is a less popular one.

stralep 16y ago

Do we want languages where a PhD is required to understand the library documentation? two PhDs for Haskell This presentation is so lighthearted... I realy like it.

joe_the_user 16y ago
Yes but the honesty is great. A lot of academic research doesn't acknowledge that the reason a working programmer wants a tool that is really simple is because I am constantly working with the threat of my project becoming overwhelmingly complex. A really simple, clear tool lets me keep a little more distance from that final, looming complexity.
voxcogitatio 16y ago
The "You need a PHD to understand Haskell" slur is so bloody ridiculous. I certainly didn't have a problem with it, and I haven't even finished my degree yet! On a more general note, I find the idea that a programming language can be "too smart" troubling. Is the solution to have dumber programming languages then?
- jedbrown 16y ago
  There is a very big difference between "too smart" and "too complicated". I think Haskell is dangerously close to the former category while C++ is firmly in the second. I appreciate "smart" for many tasks, but sometimes the operational semantics become important (e.g. it's performance-sensitive) and then you have to understand the stack at a pretty deep level and it can be awfully confusing why a tiny source-level change makes a big performance or space difference. Sometimes I pretty much know what assembly I want and it's much easier to make a C compiler produce it than to get GHC to produce it.
  - merijnv 16y ago
    I agree that it is hard to get GHC produce the assembly you want, but I think this is unfair to "blame" GHC for this. In my eyes Haskell is mostly a high-level language and if you worry about the assembler produced I think we have left high-level language territory and it might easier to just write C and use the FFI.

joelburget 16y ago

The author, Benjamin Pierce, also wrote the book Types and Programming Languages, among others. His website: http://www.cis.upenn.edu/~bcpierce/ http://www.cis.upenn.edu/~bcpierce/

jules 16y ago

What's a good introduction to contracts? I'd like to know how a basic contract system works and which extensions are there? What's the relation between contracts and assert?

limmeau 16y ago
Provided that to you, a "good introduction" is something with a lambda-calculus extension and a reduction semantics, the 2002 paper by Findler and Felleisen[1] is a good read. 1. http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.11.4081&rep=rep1&type=pdf http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.11....
- jules 16y ago
  Thanks, that is exactly what I meant :) I also found this one quite interesting: http://www.cs.brown.edu/~arjun/public/poly-contracts.pdf http://www.cs.brown.edu/~arjun/public/poly-contracts.pdf
Nick_C 16y ago
If you want introductory, see Bertrand Myer and the Eiffel programming language. http://www.eiffel.com/developers/design_by_contract.html http://www.eiffel.com/developers/design_by_contract.html http://en.wikipedia.org/wiki/Design_by_contract http://en.wikipedia.org/wiki/Design_by_contract http://en.wikipedia.org/wiki/Eiffel_(programming_language) http://en.wikipedia.org/wiki/Eiffel_(programming_language)

voxcogitatio 16y ago

Benjamin Pierce considered troll.

lawnchair_larry 16y ago

Obligatory: "Considered Harmful" Essays Considered Harmful http://meyerweb.com/eric/comment/chech.html http://meyerweb.com/eric/comment/chech.html

6ren 16y ago

With respect to very precise type systems, and coupling between program structure and types, one of the reason mathematics is so powerful is its flexibility I actually have trouble with mathematics, because it is so flexible. For example, equality of sets A and B is typically shown by saying that every element of A is in B, and every element in B is in A. Why on earth do they do that? Why not just say they're the same??! One advantage is it gives you the flexibility to demonstrate the first limb using one technique, and the second limb with a completely unrelated approach. I saw one example of showing equivalence of language defined by a class of grammars, and a language defined by constraints over sequences. You could even use a constructive and a non-constructive proof for each half. It's a way of subdividing that is decoupled.