3 ms·

You are I think making a comment about type parameters in object-oriented languages with subtyping? But why give up on static types so easily? How about a type

You are I think making a comment about type parameters in object-oriented languages with subtyping? But why give up on static types so easily? How about a type system without subtyping (e.g. Haskell, OCaml) or even better one with structural row typing (e.g. OCaml, Purescript, Elm)? Type systems are a form of machine-checked proof of correctness, at least for certain classes of errors. Sometimes proving things is laborious and a pain, but it is worth it if one cares about correctness (and often less effort than writing more unit tests).

Filligree 8y ago
Structural row typing I hadn't heard about. Elm is on my to-learn list, so I'll look it up separately, but... Coming from Haskell, what's the elevator pitch for it?
- willtim 8y ago
  IMHO, structural types are a better starting point. Nominal types can always be created by wrapping a structural type, but it is difficult to go the other way round. A language with row types can give a type to a query or have named function arguments. Extensible row types allow even more forms of composition, for example functions that require the presence of certain fields but will ignore others, very similar to subtyping.
  - ufo 8y ago
    structural vs nominal typing is orthogonal to row polymorphism vs subsumption rule.
    - deleted 8y ago
      [deleted]
    - willtim 8y ago
      Well not really as row polymorphism is a form of structural typing.
- always_good 8y ago
  The elevator pitch for Elm is that it helps you build UIs which is just never easy. And mostly prescribes its own architecture instead of having you picking between vanilla React, Redux, Mobx, etc. I never knew how amazing "if it compiles, it works" could be when building a UI.
- ufo 8y ago
  In a system with subtyping {x:int, y:int} is a subtype of {x:int}. You can have a function that receives {x:int} and you can pass a {x:int, y:int} to it. The subtype can be freely used whenever the supertype is expected. With row typing instead of subtyping you have "row variables". That function that would receive a {x:int} is typed as "forall p. {x:int; p}". You can pass the function a {x:int, y:int} because it unifies p with {y:int}. But you cannot freely convert a {x:int, y:int} to a {x:int}, it is all based around parametric polymorphism. This system with row variables works much better with hindley-milner type inference but it is a bit more restrictive. For example, you cannot use subtype polymorphism to have a heterogeneous list of objects. If you have a function that receieves a "forall p. [{x:int; p}]" you can have a list of {x:int} or a list of {x:int, y:int} but every element of the list must have the same type.
  - willtim 8y ago
    > you cannot use subtype polymorphism to have a heterogeneous list of objects You can by using an existential type parameter, which 'forgets' the types in much the same way as an upcast. [exists p. {x:int; p}]
ajross 8y ago
Not sure I get the point. The existence of a 1-argument function that takes type A to type B is semantically identical to a subtype/inheritance relationship. All the same problems pop up in basically the same ways. I genuinely thought that was what the article was talking about, but then my Haskell fu is very weak so maybe I've misunderstood the problem.
- willtim 8y ago
  I thought your comment was specifically about co/contraviance in type parameters with subtyping, because industry has explored the idea of making this unsound (e.g. the Google Dart team). But yes, co/contravariance pops up everywhere and so an unsound type system (or no type system at all) is not the answer. We had best all understand it!
  - ajross 8y ago
    > so an unsound type system (or no type system at all) is not the answer And my unpopular opinion is precisely that. "Sound" typesystems enforced at the expense of the kind of cognitive load we see here will hurt rather than help the expression of real world problems in code. Literally, casting a C function pointer through a void* is a better answer. I'm serious.
    - willtim 8y ago
      But the problem of correct program construction does not go away. There is certainly a middle ground somewhere, beyond which proofs become too expensive for most users. For the sorts of systems I work on, the sweet spot is close to Haskell 98, for others it may well be Python (no types at all).

Filligree 8y ago

Structural row typing I hadn't heard about. Elm is on my to-learn list, so I'll look it up separately, but... Coming from Haskell, what's the elevator pitch for it?

willtim 8y ago
IMHO, structural types are a better starting point. Nominal types can always be created by wrapping a structural type, but it is difficult to go the other way round. A language with row types can give a type to a query or have named function arguments. Extensible row types allow even more forms of composition, for example functions that require the presence of certain fields but will ignore others, very similar to subtyping.
- ufo 8y ago
  structural vs nominal typing is orthogonal to row polymorphism vs subsumption rule.
  - deleted 8y ago
    [deleted]
  - willtim 8y ago
    Well not really as row polymorphism is a form of structural typing.
always_good 8y ago
The elevator pitch for Elm is that it helps you build UIs which is just never easy. And mostly prescribes its own architecture instead of having you picking between vanilla React, Redux, Mobx, etc. I never knew how amazing "if it compiles, it works" could be when building a UI.
ufo 8y ago
In a system with subtyping {x:int, y:int} is a subtype of {x:int}. You can have a function that receives {x:int} and you can pass a {x:int, y:int} to it. The subtype can be freely used whenever the supertype is expected. With row typing instead of subtyping you have "row variables". That function that would receive a {x:int} is typed as "forall p. {x:int; p}". You can pass the function a {x:int, y:int} because it unifies p with {y:int}. But you cannot freely convert a {x:int, y:int} to a {x:int}, it is all based around parametric polymorphism. This system with row variables works much better with hindley-milner type inference but it is a bit more restrictive. For example, you cannot use subtype polymorphism to have a heterogeneous list of objects. If you have a function that receieves a "forall p. [{x:int; p}]" you can have a list of {x:int} or a list of {x:int, y:int} but every element of the list must have the same type.
- willtim 8y ago
  > you cannot use subtype polymorphism to have a heterogeneous list of objects You can by using an existential type parameter, which 'forgets' the types in much the same way as an upcast. [exists p. {x:int; p}]

ajross 8y ago

Not sure I get the point. The existence of a 1-argument function that takes type A to type B is semantically identical to a subtype/inheritance relationship. All the same problems pop up in basically the same ways. I genuinely thought that was what the article was talking about, but then my Haskell fu is very weak so maybe I've misunderstood the problem.

willtim 8y ago
I thought your comment was specifically about co/contraviance in type parameters with subtyping, because industry has explored the idea of making this unsound (e.g. the Google Dart team). But yes, co/contravariance pops up everywhere and so an unsound type system (or no type system at all) is not the answer. We had best all understand it!
- ajross 8y ago
  > so an unsound type system (or no type system at all) is not the answer And my unpopular opinion is precisely that. "Sound" typesystems enforced at the expense of the kind of cognitive load we see here will hurt rather than help the expression of real world problems in code. Literally, casting a C function pointer through a void* is a better answer. I'm serious.
  - willtim 8y ago
    But the problem of correct program construction does not go away. There is certainly a middle ground somewhere, beyond which proofs become too expensive for most users. For the sorts of systems I work on, the sweet spot is close to Haskell 98, for others it may well be Python (no types at all).