6 ms·

Yes, type erasure is neat and a bit of thinking will make it obvious why proving static properties does not require run time checks if the transformations you p

Yes, type erasure is neat and a bit of thinking will make it obvious why proving static properties does not require run time checks if the transformations you perform on your program preserve those static properties. I disagree with the author's claim though that types are everywhere. Types in fact are extra structure that is hoisted onto programs. At the end of the day the machine knows nothing about the types and will shuttle bytes back and forth all day long. Furthermore, types restrict the universe of computation and there are examples of programs that are not well-typed but don't go wrong when evaluated.

mtdewcmu 12y ago
I wonder if type erasure is profound, or if it only sounds profound after being hypnotized by type theory.
- dkarapetyan 12y ago
  Don't get me wrong I think type theory is really cool. In fact any kind of theory that makes me a better programmer is cool. That's one of the reasons TypeScript right now is one of my favorite languages. It is the perfect balance between the prototyping power of dynamic languages and the awesome static guarantees of statically typed languages. The best part is that the type system does not get in the way when I'm prototyping and actually starts to help out when I have the design fleshed out. I just wish more languages supported that kind of type system because sometimes I really miss the static checks when writing stuff in Ruby and Python.
  - mtdewcmu 12y ago
    What I think is cool is getting computers to do things that are interesting. Types don't do anything. I find them hard to get excited about.
    - the_af 12y ago
      What do you mean "types don't do anything"? Are you seriously going to argue that? I don't know many people in the programming or CS fields who believe that. What some people believe is that there are type systems too onerous for the benefits they bring (which is, of course, debatable). Following your line of thought, one could say that the textual representation of your program "doesn't do anything" either, and neither does the syntax or the IDE/editor you use. So none of it matters. But of course it wouldn't be true -- all those things are useful tools that help you write software that does cool things. edit: thought of an even better example: tests. Tests "don't do anything". They are not directly related to the cool stuff we want to do with our computers. But who is going to argue that we shouldn't write any tests?
      - Dylan16807 12y ago
        I find it hard to get excited about normal testing.
        the_af 12y ago
        You'll notice I only addressed the faulty assertion that "types don't do anything". I've purposefully left the excitement part out, because that's subjective. Some people are excited about testing methodologies, some about programming languages, some about their IDEs, etc. What you can bet is that absolutely no-one is excited about mission-critical software failing because of a bug that could have been caught by testing... or type checking.
      - mtdewcmu 12y ago
        I guess I wasn't clear. You could say that a line of code does something if it generates instructions for the cpu. `x = y` would generate at least one instruction (probably some kind of mov on an intel system), which would instruct the cpu to do something, e.g. change the value in a register. If you scanned through a program looking for syntactic forms that represent types as such, you could find clear examples of such syntax in most programs; some programs would have more and some less, probably determined to a large extent by programming language. It would be things like variable declarations, class declarations, etc. -- essentially declarative scaffolding, which wraps and adds meaning and context to code that does things; the type code itself, though, generates no cpu instructions, because its purpose isn't to represent action, it's orthogonal to action. You could argue that type code causes actions to be performed, such as when types need to be casted, which may trigger some kind of transformation on the underlying data. But, even though the type helps trigger action (the data transformation), the type is not that action. I don't know if what I've written will make sense or sound like empty nonsense... but the article itself makes the point that you will generally not find types in machine code; at most you can find indirect evidence that they were there. You may say, "what difference does that make? Why make the distinction?" Well, machine instructions are what make the computer do observable things. Any code you have to write that doesn't produce instructions needs to be justified somehow. There are lots of ways of justifying such extra code. But it's orthogonal to actually doing things -- pretty much by definition. Edit -- to respond more directly: >>What some people believe is that there are type systems too onerous for the benefits they bring (which is, of course, debatable). I think that's a real risk. People tend to get attached to ideas about programming languages in quasi-religious fashion; I think it's healthy to stay in touch with an objective cost/benefit perspective, though. The user doesn't see the code, he/she only sees the results. And the experience of the user is what you should focus on as a programmer -- right? >>Following your line of thought, one could say that the textual representation of your program "doesn't do anything" either, and neither does the syntax or the IDE/editor you use. So none of it matters. But of course it wouldn't be true -- all those things are useful tools that help you write software that does cool things. I'm not sure I follow the distinction you're making, between the textual representation of the code and -- what? Clearly the text has to be written before the computer will do anything -- so it must be important. >>edit: thought of an even better example: tests. Tests "don't do anything". They are not directly related to the cool stuff we want to do with our computers. But who is going to argue that we shouldn't write any tests? I said types don't do anything, and that they don't excite me. I didn't say we should get rid of all types. Tests don't do anything, either (at least, they don't do what the program should do). Tests also don't excite me. That doesn't mean that testing is pointless. Testing can be costly and tedious -- but you have to weigh that against the risk of bugs getting through.
- dsuth 12y ago
  I couldn't decide whether this was an incredibly deep post that I'm missing, or just a very obvious by-product of compilation.
  - mtdewcmu 12y ago
    One man's obvious is another man's deep.
    - dsuth 12y ago
      ... It's happening again!!
TheLoneWolfling 12y ago
Case in point: try to do the fast inverse square root hack with a (truly) strongly typed language.
- phaedrus 12y ago
  If the language supports union, then simply give your working variable the type of "union { float, long }". This directly expresses the idea that you're working with a piece of memory that is used for two purposes.
  - TheLoneWolfling 12y ago
    If the language supports untagged unions, it isn't strongly typed. With very few exceptions.
    - tomp 12y ago
      Untagged unions between two non-pointer types with the same representation (same number of bits) are perfectly safe, they are just ordinary bit-casts.
- gsg 12y ago
  What's the difficulty, exactly? You need some mundane float->bits and bits->float operations, which are commonly although not universally provided in strongly typed environments. The rest is integer ops.
  - TheLoneWolfling 12y ago
    Sure, if you can convert float -> bits -> float you can make code that does the same thing, but efficient code? Good luck.
    - jwise0 12y ago
      That's not a terribly difficult proposition in a strongly-typed language -- in fact, it is even more performant than if you were to do it with tagged unions! The function "floatFromBits : float -> bits" has no execution overhead, and simply adds a type annotation to the semantic meaning of the identity. At execution time, there are no instructions emitted for it... So, thanks for the well wishes, but in this case I don't think they're needed: any reasonable compiler should be able to do this without great difficulty.
takeoutweight 12y ago
Types give you the power of abstraction -- they allow you to define new concepts that "don't to go wrong" and allow you to speak of things other than just bytes-shuttled-on-a-turing-tape. Rigorously justifying the ignorance of the underlying bytes (i.e. being parametric over representation) is an advantage, not a downside. But maybe I am misunderstanding your comment? Perhaps you were just equivocating over what "really there" means? If that's the case, is multiplication not "really there" because it can be implemented in terms of bit shifting and addition? We don't imagine multiplication as somehow putting these restrictions on what we can do with our bit shift operators -- the multiplication is the "real" thing we care about and the binary operations are incidental. In any case, see the famous parable that opens Reynolds' "Types, Abstraction, and Parametric Polymorphism" for a colourful example of ignoring the underlying data representation: http://www.cse.chalmers.se/edu/year/2010/course/DAT140_Types/Reynolds_typesabpara.pdf http://www.cse.chalmers.se/edu/year/2010/course/DAT140_Types...
- dkarapetyan 12y ago
  If you're doing mathematics then multiplication is the thing you care about and not its representation in any given number/notation system but if you're actually implementing multiplication then you definitely care about the actual bits and bytes. What structure you impose on top of the implementation to make it easier is all nice and well but don't fool yourself into thinking that types are the end of it. In fact to truly impose some kind of type structure so you could reason about what was going on at the hardware level you'd need more than just the integer type or the floating point type because those types don't let you reason about overflow/underflow at such a high level. Any correct implementation would need to worry about those restrictions and consequently would have to represent those restrictions in the type system.
  - pinealservo 12y ago
    It's entirely possible to do so; there are even typed assembly languages and "bitdata" types and typed memory regions. Types in general can be far more expressive than most people know. Very expressive types are not necessarily easy to work with, though.
kvb 12y ago
This is an execution-centric view; I think that types really are everywhere when it comes to how typical programmers think about their code (even in dynamically typed languages).

mtdewcmu 12y ago

I wonder if type erasure is profound, or if it only sounds profound after being hypnotized by type theory.

dkarapetyan 12y ago
Don't get me wrong I think type theory is really cool. In fact any kind of theory that makes me a better programmer is cool. That's one of the reasons TypeScript right now is one of my favorite languages. It is the perfect balance between the prototyping power of dynamic languages and the awesome static guarantees of statically typed languages. The best part is that the type system does not get in the way when I'm prototyping and actually starts to help out when I have the design fleshed out. I just wish more languages supported that kind of type system because sometimes I really miss the static checks when writing stuff in Ruby and Python.
- mtdewcmu 12y ago
  What I think is cool is getting computers to do things that are interesting. Types don't do anything. I find them hard to get excited about.
  - the_af 12y ago
    What do you mean "types don't do anything"? Are you seriously going to argue that? I don't know many people in the programming or CS fields who believe that. What some people believe is that there are type systems too onerous for the benefits they bring (which is, of course, debatable). Following your line of thought, one could say that the textual representation of your program "doesn't do anything" either, and neither does the syntax or the IDE/editor you use. So none of it matters. But of course it wouldn't be true -- all those things are useful tools that help you write software that does cool things. edit: thought of an even better example: tests. Tests "don't do anything". They are not directly related to the cool stuff we want to do with our computers. But who is going to argue that we shouldn't write any tests?
    - Dylan16807 12y ago
      I find it hard to get excited about normal testing.
      - the_af 12y ago
        You'll notice I only addressed the faulty assertion that "types don't do anything". I've purposefully left the excitement part out, because that's subjective. Some people are excited about testing methodologies, some about programming languages, some about their IDEs, etc. What you can bet is that absolutely no-one is excited about mission-critical software failing because of a bug that could have been caught by testing... or type checking.
    - mtdewcmu 12y ago
      I guess I wasn't clear. You could say that a line of code does something if it generates instructions for the cpu. `x = y` would generate at least one instruction (probably some kind of mov on an intel system), which would instruct the cpu to do something, e.g. change the value in a register. If you scanned through a program looking for syntactic forms that represent types as such, you could find clear examples of such syntax in most programs; some programs would have more and some less, probably determined to a large extent by programming language. It would be things like variable declarations, class declarations, etc. -- essentially declarative scaffolding, which wraps and adds meaning and context to code that does things; the type code itself, though, generates no cpu instructions, because its purpose isn't to represent action, it's orthogonal to action. You could argue that type code causes actions to be performed, such as when types need to be casted, which may trigger some kind of transformation on the underlying data. But, even though the type helps trigger action (the data transformation), the type is not that action. I don't know if what I've written will make sense or sound like empty nonsense... but the article itself makes the point that you will generally not find types in machine code; at most you can find indirect evidence that they were there. You may say, "what difference does that make? Why make the distinction?" Well, machine instructions are what make the computer do observable things. Any code you have to write that doesn't produce instructions needs to be justified somehow. There are lots of ways of justifying such extra code. But it's orthogonal to actually doing things -- pretty much by definition. Edit -- to respond more directly: >>What some people believe is that there are type systems too onerous for the benefits they bring (which is, of course, debatable). I think that's a real risk. People tend to get attached to ideas about programming languages in quasi-religious fashion; I think it's healthy to stay in touch with an objective cost/benefit perspective, though. The user doesn't see the code, he/she only sees the results. And the experience of the user is what you should focus on as a programmer -- right? >>Following your line of thought, one could say that the textual representation of your program "doesn't do anything" either, and neither does the syntax or the IDE/editor you use. So none of it matters. But of course it wouldn't be true -- all those things are useful tools that help you write software that does cool things. I'm not sure I follow the distinction you're making, between the textual representation of the code and -- what? Clearly the text has to be written before the computer will do anything -- so it must be important. >>edit: thought of an even better example: tests. Tests "don't do anything". They are not directly related to the cool stuff we want to do with our computers. But who is going to argue that we shouldn't write any tests? I said types don't do anything, and that they don't excite me. I didn't say we should get rid of all types. Tests don't do anything, either (at least, they don't do what the program should do). Tests also don't excite me. That doesn't mean that testing is pointless. Testing can be costly and tedious -- but you have to weigh that against the risk of bugs getting through.
dsuth 12y ago
I couldn't decide whether this was an incredibly deep post that I'm missing, or just a very obvious by-product of compilation.
- mtdewcmu 12y ago
  One man's obvious is another man's deep.
  - dsuth 12y ago
    ... It's happening again!!

TheLoneWolfling 12y ago

Case in point: try to do the fast inverse square root hack with a (truly) strongly typed language.

phaedrus 12y ago
If the language supports union, then simply give your working variable the type of "union { float, long }". This directly expresses the idea that you're working with a piece of memory that is used for two purposes.
- TheLoneWolfling 12y ago
  If the language supports untagged unions, it isn't strongly typed. With very few exceptions.
  - tomp 12y ago
    Untagged unions between two non-pointer types with the same representation (same number of bits) are perfectly safe, they are just ordinary bit-casts.
gsg 12y ago
What's the difficulty, exactly? You need some mundane float->bits and bits->float operations, which are commonly although not universally provided in strongly typed environments. The rest is integer ops.
- TheLoneWolfling 12y ago
  Sure, if you can convert float -> bits -> float you can make code that does the same thing, but efficient code? Good luck.
  - jwise0 12y ago
    That's not a terribly difficult proposition in a strongly-typed language -- in fact, it is even more performant than if you were to do it with tagged unions! The function "floatFromBits : float -> bits" has no execution overhead, and simply adds a type annotation to the semantic meaning of the identity. At execution time, there are no instructions emitted for it... So, thanks for the well wishes, but in this case I don't think they're needed: any reasonable compiler should be able to do this without great difficulty.

takeoutweight 12y ago

Types give you the power of abstraction -- they allow you to define new concepts that "don't to go wrong" and allow you to speak of things other than just bytes-shuttled-on-a-turing-tape. Rigorously justifying the ignorance of the underlying bytes (i.e. being parametric over representation) is an advantage, not a downside. But maybe I am misunderstanding your comment? Perhaps you were just equivocating over what "really there" means? If that's the case, is multiplication not "really there" because it can be implemented in terms of bit shifting and addition? We don't imagine multiplication as somehow putting these restrictions on what we can do with our bit shift operators -- the multiplication is the "real" thing we care about and the binary operations are incidental. In any case, see the famous parable that opens Reynolds' "Types, Abstraction, and Parametric Polymorphism" for a colourful example of ignoring the underlying data representation: http://www.cse.chalmers.se/edu/year/2010/course/DAT140_Types/Reynolds_typesabpara.pdf http://www.cse.chalmers.se/edu/year/2010/course/DAT140_Types...

dkarapetyan 12y ago
If you're doing mathematics then multiplication is the thing you care about and not its representation in any given number/notation system but if you're actually implementing multiplication then you definitely care about the actual bits and bytes. What structure you impose on top of the implementation to make it easier is all nice and well but don't fool yourself into thinking that types are the end of it. In fact to truly impose some kind of type structure so you could reason about what was going on at the hardware level you'd need more than just the integer type or the floating point type because those types don't let you reason about overflow/underflow at such a high level. Any correct implementation would need to worry about those restrictions and consequently would have to represent those restrictions in the type system.
- pinealservo 12y ago
  It's entirely possible to do so; there are even typed assembly languages and "bitdata" types and typed memory regions. Types in general can be far more expressive than most people know. Very expressive types are not necessarily easy to work with, though.

kvb 12y ago

This is an execution-centric view; I think that types really are everywhere when it comes to how typical programmers think about their code (even in dynamically typed languages).