8 ms·

Seven deadly sins of talking about “types” (2014)

98 points by porker 7y ago

GnarfGnarf 7y ago
I've written a lot of C++, and a fair bit of Python. Dynamic typing is seductive at first, but you eventually realize that you would much prefer errors be caught at compile time, rather than run time. I want a language where I can: cInches in1, in2, in3; cCm cm1; in1 = in2 + in3; // OK in1 = cm1; // compilation error: cannot mix units in1 = in2 * in3; // compilation error: square inches are not inches in1 = 2.0 * in2; // OK float f1 = in1 / in2; // OK cCm foo(cInches in) { return cCm(in * 2.54); } foo(cm1); // compilation error Naturally this is accomplished with special classes (not shown here), it is not an inherent property of the language.
- jraph 7y ago
  It would be great to have dimensional analysis in typing systems of programming languages.
  - momentoftop 7y ago
    F# has had typed units of measure for over a decade, with Hindley-Milner style type-inference, so you can do stuff like let foo x y = (x:int<m>) * y + 10<m/s>;; And it infers that y has type <1/s>. You can add whatever dimensional types you want.
- kristiandupont 7y ago
  I am not sure if your "I want a language where I can" is followed by an implicit ", and C++ is that language" or ", I wish it existed". I am guessing the former as your example is possible with C++ but it doesn't seem like a great example as you are using units of measure for your types. There are languages that support those and obviously, in such a case, assigning centimeters or inches to a distance-typed variable is both ok. The type error would be in mixing distance and, say, weight.
  - GnarfGnarf 7y ago
    I meant C++. I'm using this currently in C++ production code. Has saved me tons of debugging. What I meant was that if I'm going to look at a new language, I would expect it to support this type of functionality. I suppose I can enhance the classes and overload the operators to automatically convert from cm to inches when doing mixed arithmetic. But this will quickly become insanely complicated when considering all possible permutations of arithmetic operators.
- jasim 7y ago
  F# has "Units of Measure" that does this. https://docs.microsoft.com/en-us/dotnet/fsharp/language-reference/units-of-measure https://docs.microsoft.com/en-us/dotnet/fsharp/language-refe...
- clarry 7y ago
  Why do you want these compilation errors? Both are measures of length. I can add an inch and a centimeter, and the result is a well defined length that we can express in inches, centimeters, light years, or any other measure of length. Likewise for areas or ratios of lengths. I would generally prefer it if the language just gave me the correct result, which I can then print out in the user's preferred unit.
  - GnarfGnarf 7y ago
    Adding inches and raw centimetres is like adding apples and oranges, which they taught us not to do in grade school. What you are thinking of is: in1 = cm1.toInches(); If someone passes cm to a function that expects inches, much error and grief will result.
    - clarry 7y ago
      No, I'm not thinking of dec1 = hex1.toDecimal(); because num1 = 0xff00 + 64; works just as well and so does functionThatExpectsNumber(0b1101); as does p1 = mat1 * vec1; Lengths are just as absolute as integers, but we have different ways to input and represent them. A sufficiently advanced language understands the equivalences and does just the right thing. Adding apples and oranges does not happen. Generally your function should not expect inches, it should expect some length and I can input it in any unit of length I want. Sure there are cases where you're constrained and need to account for the limited range and precision of your underlying storage format, but that should not be the default for any modern high level general purpose programming language. We don't need to concern ourselves with grade school stuff, the computer can do it for us. Adding apples to oranges is concern at a lower level than the abstraction we should be working with by default. Doing arithmetic by hand on pen and paper is pretty low level. Adding apples to oranges is also a concern when you don't have proper types by which the system can deduce that orange is actually just 2.54*apple.
      - GnarfGnarf 7y ago
        You're missing the point. I make an app that prints charts. It includes a function that subtracts user-specified margins from the paper width, to calculate available space. Some of my customers are in the U.S (inches), others are not (cm). If I call printPage(0.75, 0.75); you really think it's going to be all the same whether "0.75" represents inches or centimetres?
- auxym 7y ago
  I believe you can do this with distinct type aliases in Nim: https://nim-by-example.github.io/types/distinct/ https://nim-by-example.github.io/types/distinct/
whateveracct 7y ago
> Presenting type-level programming as a good thing > Fetishizing Curry-Howard These seem a bit causal :) When you do closer and closer to dependently-typed programming (which necessitates more type-level programming because dependent types aren't present in any production language yet), Curry-Howard actually can be a nice way to ground yourself when you get confused or stuck programming at the type level.
_bxg1 7y ago
Good points. However, I disagree with this: > But please, stop pretending that type-level programming is a desirable thing. It's a kludge, and hopefully a temporary one. Personally, I want to write all my specifications in more-or-less the same language I use to write ordinary code. It's the tool's job to prove correctness or, if it must, tell me that it failed. I don't see explicit type-programming as (always) a kludge; oftentimes it's the primary vocabulary for expressing certain ideas. I.e. type annotations are not (always) just typechecker-hints, but can be explicit documentation of intent. > We need to be able to step up the strength of our specifications without switching language all the time. We need to integrate typed and untyped code This has been a revelation during my time spent with TypeScript. The fact that I can just add a comment that disables an unhelpful type error on a given line is a game-changer. Or that I can assert to the system "no really, this value that has a union type is actually just this particular subset of that union" (cast) and retain meaningful checks after that point. Having a type system that's flexible has made it enormously more useful. It allows you to deal with those cases where what you want to do can't be type-checked, within the context of (and playing nicely with) a broader system that is type-checked.
- mike_hock 7y ago
  It is sensible to include this in TypeScript, because it needs to interface with potentially large swathes of plain JavaScript, which is akin to unsafe code in Rust. TypeString type assertions are like C++ reinterpret_cast. If you're wrong about what you think it is, that's as good as undefined behavior in C++, virtually anything can happen.
  - ChrisSD 7y ago
    I'm only nitpicking because this is one of the things the article complains about but I think you're conflating two types of saftey. All Javascript (TypeScript included) is "safe" in the sense of C++/Rust. Using the wrong TypeScript type in TypeScript can result in programming errors but not unsafety or undefined behaviour in C++/Rust terms.
- atoav 7y ago
  As somebody who moved from untyped to typed (Python to Rust) I think the two biggest arguments for typed systems are: - they encourage you to keep you code data oriented, which is usually (at least in my experience) a food thing - certain classes of mistakes can be checked for before you even run the code itself
js8 7y ago
The problem is, just like with "function", the usage word of the word "type" is a bit less formal in programming than mathematics. As far as I can tell, we use "types" in programming for 4 things: 1. Modelling the domain (e.g. type Temperature) 2. Limiting the range of values (e.g. enum) 3. Decision about how to store the data (e.g. ArrayList) 4. Specification of dispatch on values (e.g. file as an interface) The formal type theory deals with 1 and perhaps a bit of 2. The original usage of types in programming (in old assemblers, Cobol, etc.) was 3. Dynamic programming languages primarily use the term in the 4th meaning.
- nbevans 7y ago
  Your #2 is wrong (sorry). Enums in most mainstream languages don't "limit"; they merely specify known values. Unknown values are still possible. For a type-safe enum, see discriminated union.
  - thethirdone 7y ago
    Can you give some examples other than C, C++, and C# where this is true? Most languages either don't have them as definable types, are C based and therefore map them to integers, or actually limit values. AFAIK, python, java, rust, ocaml, haskell, and swift all have enums that actually limit values.
    - t-writescode 7y ago
      You can do bitwise operations in Java https://stackoverflow.com/questions/6282619/is-there-a-way-to-bitwise-or-enums-in-java https://stackoverflow.com/questions/6282619/is-there-a-way-t...
choeger 7y ago
The author is right with every. Single. Point. But I think their criticism comes from an ivory tower where people in general agree that efficient programming needs strong and sound tools. Unfortunately, in practice it seems to be all about "velocity". When you see a huge codebase in python grown over several years and try to refactor it, reason about it, or just enhance it, you will inevitably come to the conclusion that the omission of static type checking is a grave error from a system-design perspective. And when you work with the developers of such a code base you will understand that static type checking is first and foremost a means of communication between the language implementation and the developers. Without this tool it is like taking away a common spoken language between the developers and having to translate everything into some form of pidgin.
- jmull 7y ago
  If you have a system where the developers often aren’t sure what it does, how to organize the code, aren’t designing for maintainability, etc., static type checking really isn’t going to help you pick up the pieces afterward. I like static type checking for what it does, but it solves some little problems, not big ones. (And can cause their own little problems.)
  - cobbzilla 7y ago
    Disagree. Off the top of my head: Inability to do automatic, reliable refactoring is a big problem. Inability to detect a wide range of errors before hitting them at runtime, big problem. There are many more.
    - naasking 7y ago
      In other words, it will help you not break things. Tests are existential proofs of something broken, but types establish a universal proof that something is not broken in specific ways. Tests simply can't replace the properties guaranteed by types.
      - jnwatson 7y ago
waffletower 7y ago
This blog post ought to circulate annually.
cjfd 7y ago
Mostly good points but also some quibles. "Personally, I want to write all my specifications in more-or-less the same language I use to write ordinary code." If we take 'specifications' one level further and actually want our algorithms to be proven correct, as in, by a proof assistant it is quite unclear that this possible or desirable. Maybe the best way to program is to have specifications in a language as close to mathematics as possible and executable code in a language much closer to the machine. It is not clear to me that both of these things should be the same language. "Equivocating around type-safety" The author seems to want 'type-safety' to mean that it is made sure that an integer in memory is not accessed as if it were a float. While this is clearly a desirable feature that also dynamically typed languages provide by checking and/or converting at run time I really don't think this is the meaning of 'type-safety' in common parlance. If I attempt to use a variable as if it were of a different type I generally get a runtime error in a dynamic language, e.g., because I am accessing a field that does not exist. 'type-safety' is the property that the language prevents this runtime error from happening because this is checked at compile/lint time.
- DougBTX 7y ago
  > I really don't think this is the meaning of 'type-safety' in common parlance. The bulk of the article is a call for more accurate use of terminology, so in a sense you’re noting the same thing: people using “type safe” when they mean “compile-time type-checked”, as a specific misuse of terminology. The Wikipedia page spells out the difference clearly: https://en.m.wikipedia.org/wiki/Type_safety https://en.m.wikipedia.org/wiki/Type_safety Types are safe if they are checked, and the checking can be done statically at compile time or dynamically at run time. Perhaps we’re just so used to working with type-safe languages that it is taken for granted (it would be quite unusual in eg Web Dev to use a language that is not type-safe) that the terminology is repurposed to be useful in conversations that we might have more often, eg, whether to rely more on static vs dynamic type checks.
- pizlonator 7y ago
  > The author seems to want 'type-safety' to mean that it is made sure that an integer in memory is not accessed as if it were a float. While this is clearly a desirable feature that also dynamically typed languages provide by checking and/or converting at run time I really don't think this is the meaning of 'type-safety' in common parlance. The author is wonderfully clear on this point. Under what he calls “Saraswat type safety” (not the best name), a dynamically typed language is type safe. So is a language like B that just has a word type (sort of... B may or may not have had UB depending on your perspective and UB may or may not preclude type safety... again depending on perspective). There is a modern new-age use of the term “type safety” that means something less precise than this, namely your idea that it somehow precludes dynamic type checks. What nonsense. If a language checks array bounds dynamically, does that mean it’s not type safe? Give me a break.
Tomte 7y ago
It makes me smile that blosxom is still in use.
dmbieleu 7y ago
cool
dmbieleu 7y ago
ÉLISABETH I LIKE HER SO MUCH
andybak 7y ago
> In a typed language, only polymorphism which can be proved correct is admissible. In an untyped language, arbitrarily complex polymorphism is expressible. [Hickey's tranducers give an] example of how patterns of polymorphism which humans find comprehensible can easily become extremely hard to capture precisely in a logic. Usually they are captured only overapproximately, which, in turn, yields an inexpressive proof system. The end result is that some manifestly correct code does not type-check. There is something here close to a feeling that I've got that I struggle to experess. My two day to day languages are Python and C#. My C# code is usally longer and more complex than my Python code. At least part of this isn't down to the problem domain, syntax or features available in one but not the other. However I struggle to put into words exactly why or what is the cause of this (or even to really quantify the difference as I'm doing very different things in each language). The pendulum has swung massively towards pro-static-typing but I remember the last cycle and I would like to hear from more people who were around for the last time we all started to decide static typing had huge drawbacks and the cost of dynamic typing was a price worth paying.
- Smaug123 7y ago
  Well, C# is a pretty verbose language and it really pushes you towards object orientation (which is itself a verbose paradigm). It's not surprising that your code is longer in C#. I'd say a more fair comparison with Python would be F#, which is roughly as terse as Python.
- IshKebab 7y ago
  Python is a much more compact and densely expressive language than C#. I don't think comparing the length of code is particularly helpful. How many runtime type errors do you get in your C# code?
based2 7y ago
+ Avoid vagueness of 'type' as attribute.
arkanciscan 7y ago
It's funny to me that someone can write so intelligently about types on a blog that looks like such garbage on mobile.
lewisjoe 7y ago
I like how the author acknowledges the problem with the very word "type" - https://www.cs.tufts.edu/~nr/cs257/archive/stephen-kell/in-search-of-types.pdf https://www.cs.tufts.edu/~nr/cs257/archive/stephen-kell/in-s... The word "Type" is such an overloaded term, just like how "Workflow" is an overloaded term in the tech industry[1]. For example, when people say "X is strongly typed language" means something much different than when people say "In Haskell, function have types" [2] or "Idris has dependent types". They aren't completely unrelated, but they mean two very different set of things depending on the context. [1] https://news.ycombinator.com/item?id=21544453 https://news.ycombinator.com/item?id=21544453 [2] http://learnyouahaskell.com/types-and-typeclasses http://learnyouahaskell.com/types-and-typeclasses

98 points by porker 7y ago

I've written a lot of C++, and a fair bit of Python. Dynamic typing is seductive at first, but you eventually realize that you would much prefer errors be caught at compile time, rather than run time. I want a language where I can: cInches in1, in2, in3; cCm cm1; in1 = in2 + in3; // OK in1 = cm1; // compilation error: cannot mix units in1 = in2 * in3; // compilation error: square inches are not inches in1 = 2.0 * in2; // OK float f1 = in1 / in2; // OK cCm foo(cInches in) { return cCm(in * 2.54); } foo(cm1); // compilation error Naturally this is accomplished with special classes (not shown here), it is not an inherent property of the language.

jraph 7y ago
It would be great to have dimensional analysis in typing systems of programming languages.
- momentoftop 7y ago
  F# has had typed units of measure for over a decade, with Hindley-Milner style type-inference, so you can do stuff like let foo x y = (x:int<m>) * y + 10<m/s>;; And it infers that y has type <1/s>. You can add whatever dimensional types you want.
kristiandupont 7y ago
I am not sure if your "I want a language where I can" is followed by an implicit ", and C++ is that language" or ", I wish it existed". I am guessing the former as your example is possible with C++ but it doesn't seem like a great example as you are using units of measure for your types. There are languages that support those and obviously, in such a case, assigning centimeters or inches to a distance-typed variable is both ok. The type error would be in mixing distance and, say, weight.
- GnarfGnarf 7y ago
  I meant C++. I'm using this currently in C++ production code. Has saved me tons of debugging. What I meant was that if I'm going to look at a new language, I would expect it to support this type of functionality. I suppose I can enhance the classes and overload the operators to automatically convert from cm to inches when doing mixed arithmetic. But this will quickly become insanely complicated when considering all possible permutations of arithmetic operators.
jasim 7y ago
F# has "Units of Measure" that does this. https://docs.microsoft.com/en-us/dotnet/fsharp/language-reference/units-of-measure https://docs.microsoft.com/en-us/dotnet/fsharp/language-refe...
clarry 7y ago
Why do you want these compilation errors? Both are measures of length. I can add an inch and a centimeter, and the result is a well defined length that we can express in inches, centimeters, light years, or any other measure of length. Likewise for areas or ratios of lengths. I would generally prefer it if the language just gave me the correct result, which I can then print out in the user's preferred unit.
- GnarfGnarf 7y ago
  Adding inches and raw centimetres is like adding apples and oranges, which they taught us not to do in grade school. What you are thinking of is: in1 = cm1.toInches(); If someone passes cm to a function that expects inches, much error and grief will result.
  - clarry 7y ago
    No, I'm not thinking of dec1 = hex1.toDecimal(); because num1 = 0xff00 + 64; works just as well and so does functionThatExpectsNumber(0b1101); as does p1 = mat1 * vec1; Lengths are just as absolute as integers, but we have different ways to input and represent them. A sufficiently advanced language understands the equivalences and does just the right thing. Adding apples and oranges does not happen. Generally your function should not expect inches, it should expect some length and I can input it in any unit of length I want. Sure there are cases where you're constrained and need to account for the limited range and precision of your underlying storage format, but that should not be the default for any modern high level general purpose programming language. We don't need to concern ourselves with grade school stuff, the computer can do it for us. Adding apples to oranges is concern at a lower level than the abstraction we should be working with by default. Doing arithmetic by hand on pen and paper is pretty low level. Adding apples to oranges is also a concern when you don't have proper types by which the system can deduce that orange is actually just 2.54*apple.
    - GnarfGnarf 7y ago
      You're missing the point. I make an app that prints charts. It includes a function that subtracts user-specified margins from the paper width, to calculate available space. Some of my customers are in the U.S (inches), others are not (cm). If I call printPage(0.75, 0.75); you really think it's going to be all the same whether "0.75" represents inches or centimetres?
auxym 7y ago
I believe you can do this with distinct type aliases in Nim: https://nim-by-example.github.io/types/distinct/ https://nim-by-example.github.io/types/distinct/

whateveracct 7y ago

> Presenting type-level programming as a good thing > Fetishizing Curry-Howard These seem a bit causal :) When you do closer and closer to dependently-typed programming (which necessitates more type-level programming because dependent types aren't present in any production language yet), Curry-Howard actually can be a nice way to ground yourself when you get confused or stuck programming at the type level.

_bxg1 7y ago

Good points. However, I disagree with this: > But please, stop pretending that type-level programming is a desirable thing. It's a kludge, and hopefully a temporary one. Personally, I want to write all my specifications in more-or-less the same language I use to write ordinary code. It's the tool's job to prove correctness or, if it must, tell me that it failed. I don't see explicit type-programming as (always) a kludge; oftentimes it's the primary vocabulary for expressing certain ideas. I.e. type annotations are not (always) just typechecker-hints, but can be explicit documentation of intent. > We need to be able to step up the strength of our specifications without switching language all the time. We need to integrate typed and untyped code This has been a revelation during my time spent with TypeScript. The fact that I can just add a comment that disables an unhelpful type error on a given line is a game-changer. Or that I can assert to the system "no really, this value that has a union type is actually just this particular subset of that union" (cast) and retain meaningful checks after that point. Having a type system that's flexible has made it enormously more useful. It allows you to deal with those cases where what you want to do can't be type-checked, within the context of (and playing nicely with) a broader system that is type-checked.

mike_hock 7y ago
It is sensible to include this in TypeScript, because it needs to interface with potentially large swathes of plain JavaScript, which is akin to unsafe code in Rust. TypeString type assertions are like C++ reinterpret_cast. If you're wrong about what you think it is, that's as good as undefined behavior in C++, virtually anything can happen.
- ChrisSD 7y ago
  I'm only nitpicking because this is one of the things the article complains about but I think you're conflating two types of saftey. All Javascript (TypeScript included) is "safe" in the sense of C++/Rust. Using the wrong TypeScript type in TypeScript can result in programming errors but not unsafety or undefined behaviour in C++/Rust terms.
atoav 7y ago
As somebody who moved from untyped to typed (Python to Rust) I think the two biggest arguments for typed systems are: - they encourage you to keep you code data oriented, which is usually (at least in my experience) a food thing - certain classes of mistakes can be checked for before you even run the code itself

js8 7y ago

The problem is, just like with "function", the usage word of the word "type" is a bit less formal in programming than mathematics. As far as I can tell, we use "types" in programming for 4 things: 1. Modelling the domain (e.g. type Temperature) 2. Limiting the range of values (e.g. enum) 3. Decision about how to store the data (e.g. ArrayList) 4. Specification of dispatch on values (e.g. file as an interface) The formal type theory deals with 1 and perhaps a bit of 2. The original usage of types in programming (in old assemblers, Cobol, etc.) was 3. Dynamic programming languages primarily use the term in the 4th meaning.

nbevans 7y ago
Your #2 is wrong (sorry). Enums in most mainstream languages don't "limit"; they merely specify known values. Unknown values are still possible. For a type-safe enum, see discriminated union.
- thethirdone 7y ago
  Can you give some examples other than C, C++, and C# where this is true? Most languages either don't have them as definable types, are C based and therefore map them to integers, or actually limit values. AFAIK, python, java, rust, ocaml, haskell, and swift all have enums that actually limit values.
  - t-writescode 7y ago
    You can do bitwise operations in Java https://stackoverflow.com/questions/6282619/is-there-a-way-to-bitwise-or-enums-in-java https://stackoverflow.com/questions/6282619/is-there-a-way-t...

choeger 7y ago

The author is right with every. Single. Point. But I think their criticism comes from an ivory tower where people in general agree that efficient programming needs strong and sound tools. Unfortunately, in practice it seems to be all about "velocity". When you see a huge codebase in python grown over several years and try to refactor it, reason about it, or just enhance it, you will inevitably come to the conclusion that the omission of static type checking is a grave error from a system-design perspective. And when you work with the developers of such a code base you will understand that static type checking is first and foremost a means of communication between the language implementation and the developers. Without this tool it is like taking away a common spoken language between the developers and having to translate everything into some form of pidgin.

jmull 7y ago
If you have a system where the developers often aren’t sure what it does, how to organize the code, aren’t designing for maintainability, etc., static type checking really isn’t going to help you pick up the pieces afterward. I like static type checking for what it does, but it solves some little problems, not big ones. (And can cause their own little problems.)
- cobbzilla 7y ago
  Disagree. Off the top of my head: Inability to do automatic, reliable refactoring is a big problem. Inability to detect a wide range of errors before hitting them at runtime, big problem. There are many more.
  - naasking 7y ago
    In other words, it will help you not break things. Tests are existential proofs of something broken, but types establish a universal proof that something is not broken in specific ways. Tests simply can't replace the properties guaranteed by types.
    - jnwatson 7y ago

waffletower 7y ago

This blog post ought to circulate annually.

cjfd 7y ago

Mostly good points but also some quibles. "Personally, I want to write all my specifications in more-or-less the same language I use to write ordinary code." If we take 'specifications' one level further and actually want our algorithms to be proven correct, as in, by a proof assistant it is quite unclear that this possible or desirable. Maybe the best way to program is to have specifications in a language as close to mathematics as possible and executable code in a language much closer to the machine. It is not clear to me that both of these things should be the same language. "Equivocating around type-safety" The author seems to want 'type-safety' to mean that it is made sure that an integer in memory is not accessed as if it were a float. While this is clearly a desirable feature that also dynamically typed languages provide by checking and/or converting at run time I really don't think this is the meaning of 'type-safety' in common parlance. If I attempt to use a variable as if it were of a different type I generally get a runtime error in a dynamic language, e.g., because I am accessing a field that does not exist. 'type-safety' is the property that the language prevents this runtime error from happening because this is checked at compile/lint time.

DougBTX 7y ago
> I really don't think this is the meaning of 'type-safety' in common parlance. The bulk of the article is a call for more accurate use of terminology, so in a sense you’re noting the same thing: people using “type safe” when they mean “compile-time type-checked”, as a specific misuse of terminology. The Wikipedia page spells out the difference clearly: https://en.m.wikipedia.org/wiki/Type_safety https://en.m.wikipedia.org/wiki/Type_safety Types are safe if they are checked, and the checking can be done statically at compile time or dynamically at run time. Perhaps we’re just so used to working with type-safe languages that it is taken for granted (it would be quite unusual in eg Web Dev to use a language that is not type-safe) that the terminology is repurposed to be useful in conversations that we might have more often, eg, whether to rely more on static vs dynamic type checks.
pizlonator 7y ago
> The author seems to want 'type-safety' to mean that it is made sure that an integer in memory is not accessed as if it were a float. While this is clearly a desirable feature that also dynamically typed languages provide by checking and/or converting at run time I really don't think this is the meaning of 'type-safety' in common parlance. The author is wonderfully clear on this point. Under what he calls “Saraswat type safety” (not the best name), a dynamically typed language is type safe. So is a language like B that just has a word type (sort of... B may or may not have had UB depending on your perspective and UB may or may not preclude type safety... again depending on perspective). There is a modern new-age use of the term “type safety” that means something less precise than this, namely your idea that it somehow precludes dynamic type checks. What nonsense. If a language checks array bounds dynamically, does that mean it’s not type safe? Give me a break.

Tomte 7y ago

It makes me smile that blosxom is still in use.

dmbieleu 7y ago

cool

dmbieleu 7y ago

ÉLISABETH I LIKE HER SO MUCH

andybak 7y ago

> In a typed language, only polymorphism which can be proved correct is admissible. In an untyped language, arbitrarily complex polymorphism is expressible. [Hickey's tranducers give an] example of how patterns of polymorphism which humans find comprehensible can easily become extremely hard to capture precisely in a logic. Usually they are captured only overapproximately, which, in turn, yields an inexpressive proof system. The end result is that some manifestly correct code does not type-check. There is something here close to a feeling that I've got that I struggle to experess. My two day to day languages are Python and C#. My C# code is usally longer and more complex than my Python code. At least part of this isn't down to the problem domain, syntax or features available in one but not the other. However I struggle to put into words exactly why or what is the cause of this (or even to really quantify the difference as I'm doing very different things in each language). The pendulum has swung massively towards pro-static-typing but I remember the last cycle and I would like to hear from more people who were around for the last time we all started to decide static typing had huge drawbacks and the cost of dynamic typing was a price worth paying.

Smaug123 7y ago
Well, C# is a pretty verbose language and it really pushes you towards object orientation (which is itself a verbose paradigm). It's not surprising that your code is longer in C#. I'd say a more fair comparison with Python would be F#, which is roughly as terse as Python.
IshKebab 7y ago
Python is a much more compact and densely expressive language than C#. I don't think comparing the length of code is particularly helpful. How many runtime type errors do you get in your C# code?

based2 7y ago

+ Avoid vagueness of 'type' as attribute.

arkanciscan 7y ago

It's funny to me that someone can write so intelligently about types on a blog that looks like such garbage on mobile.

lewisjoe 7y ago

I like how the author acknowledges the problem with the very word "type" - https://www.cs.tufts.edu/~nr/cs257/archive/stephen-kell/in-search-of-types.pdf https://www.cs.tufts.edu/~nr/cs257/archive/stephen-kell/in-s... The word "Type" is such an overloaded term, just like how "Workflow" is an overloaded term in the tech industry[1]. For example, when people say "X is strongly typed language" means something much different than when people say "In Haskell, function have types" [2] or "Idris has dependent types". They aren't completely unrelated, but they mean two very different set of things depending on the context. [1] https://news.ycombinator.com/item?id=21544453 https://news.ycombinator.com/item?id=21544453 [2] http://learnyouahaskell.com/types-and-typeclasses http://learnyouahaskell.com/types-and-typeclasses