4 ms·

It wouldn't surprise me at all if static typing was capable of offering useful help. If it can't today, I wouldn't be surprised to see us make progress over the

It wouldn't surprise me at all if static typing was capable of offering useful help. If it can't today, I wouldn't be surprised to see us make progress over the next few years. I think interesting conversations could be had about why this problem is harder to model using type systems than other problems are. Where I get confused is when this is used as an argument against using static typing in general. By analogy: “Hammering nails is probably one of the most basic things you can do as a carpenter. If lathes aren't capable of offering useful help, then something is very odd.” I don't mean to mock, but it doesn't seem odd to me at all that not all tools are good for all purposes. What seems odd to me is trying to argue against the use of a tool that has proven itself in many different situations by pointing out that there exist situations it isn't useful in. Sure, that's true, but so what?

metaphorm 11y ago
but a programming language isn't a hammer or a lathe. its a workshop that is used to produce hammers and lathes and every other tool you will need. the criteria for judging the workshop is rather different than the criteria for judging the lathe.
- Solarsail 11y ago
  PL's as tools is a half-accurate analogy. If you're going to stretch it that far, shouldn't you use something more accurate? Or better, not use an analogy for something that detailed? Say, PL's are materials. They are something that useful things "tools" are fashioned out of. The properties of a material affect the entire thing built out of it, in modest but pervasive ways. Some programs are built in more than one language, this could be seen as an object built with different materials for different parts. Now, whether mainstream languages are analogous to different iron alloys, wood, concrete or plastic is a different discussion. (And maybe another exercise in taking an analogy too far...) Not sure where I saw this analogy first, since I can't find it on LtU...
- deleted 11y ago
  [deleted]
tome 11y ago
> I think interesting conversations could be had about why this problem is harder to model using type systems than other problems are. We can summarize this in ten seconds: More equations hold between combinations of units than combinations of types constructed using type constructors. For example, m kg m^-1 = kg, but no such relationship exists between (A, (B, A -> R)) and B. Proving these sorts of equivalences adds complexity to type systems.

metaphorm 11y ago

but a programming language isn't a hammer or a lathe. its a workshop that is used to produce hammers and lathes and every other tool you will need. the criteria for judging the workshop is rather different than the criteria for judging the lathe.

Solarsail 11y ago
PL's as tools is a half-accurate analogy. If you're going to stretch it that far, shouldn't you use something more accurate? Or better, not use an analogy for something that detailed? Say, PL's are materials. They are something that useful things "tools" are fashioned out of. The properties of a material affect the entire thing built out of it, in modest but pervasive ways. Some programs are built in more than one language, this could be seen as an object built with different materials for different parts. Now, whether mainstream languages are analogous to different iron alloys, wood, concrete or plastic is a different discussion. (And maybe another exercise in taking an analogy too far...) Not sure where I saw this analogy first, since I can't find it on LtU...
deleted 11y ago
[deleted]

tome 11y ago

> I think interesting conversations could be had about why this problem is harder to model using type systems than other problems are. We can summarize this in ten seconds: More equations hold between combinations of units than combinations of types constructed using type constructors. For example, m kg m^-1 = kg, but no such relationship exists between (A, (B, A -> R)) and B. Proving these sorts of equivalences adds complexity to type systems.