5 ms·

> Great! I believe, by that definition, your assertion that "good" typesystems don't reduce expressiveness is false, at least for common type systems such as Ha

> Great! I believe, by that definition, your assertion that "good" typesystems don't reduce expressiveness is false, at least for common type systems such as Haskell's, Java's, ML's, etc. Haskell is not very good at extensible runtime polymorphism (one of its weaknesses). Try OCaml's polymorphic variants.

codygman 10y ago
After quickly scanning https://realworldocaml.org/v1/en/html/variants.html https://realworldocaml.org/v1/en/html/variants.html, isn't the same thing accomplished by GADTs?
- rbehrends 10y ago
  The point of polymorphic variants is that the entire type doesn't have to be fully defined in one place; you can have partial definitions in a module and those definitions can even overlap. You can have (say) [ `Int of int | `String of string ] in one module and [ `String of string | `Char of char ] in another, and the typechecker will handle intersections and unions of these types.
rntz 10y ago
Okay, then I can pick another example: A dictionary where the type of the values depends on the key they're inserted under. (For example, a representation of the closure of a function in a typed language.) Of course, then I can go to a dependently typed language, but are you really going to tell me that only dependently typed languages count as "good" static type systems?
- rbehrends 10y ago
  I am not arguing completeness here; a type system is not a full-blown specification language and does not have to be. (I actually tend towards the point of view that trying to make them complete specification languages has limited practical value, but that's a different issue.) The point here is that the type system does not restrict me from implementing a data structure that adheres to this constraint, even if it does not enforce it for me.
  - deleted 10y ago
    [deleted]
- dllthomas 10y ago
  You can do this in GHC Haskell with existential quantification, or trade static checks for runtime with Data.Dynamic. (Again, not arguing against your thesis here.)

codygman 10y ago

After quickly scanning https://realworldocaml.org/v1/en/html/variants.html https://realworldocaml.org/v1/en/html/variants.html, isn't the same thing accomplished by GADTs?

rbehrends 10y ago
The point of polymorphic variants is that the entire type doesn't have to be fully defined in one place; you can have partial definitions in a module and those definitions can even overlap. You can have (say) [ `Int of int | `String of string ] in one module and [ `String of string | `Char of char ] in another, and the typechecker will handle intersections and unions of these types.

rntz 10y ago

Okay, then I can pick another example: A dictionary where the type of the values depends on the key they're inserted under. (For example, a representation of the closure of a function in a typed language.) Of course, then I can go to a dependently typed language, but are you really going to tell me that only dependently typed languages count as "good" static type systems?

rbehrends 10y ago
I am not arguing completeness here; a type system is not a full-blown specification language and does not have to be. (I actually tend towards the point of view that trying to make them complete specification languages has limited practical value, but that's a different issue.) The point here is that the type system does not restrict me from implementing a data structure that adheres to this constraint, even if it does not enforce it for me.
- deleted 10y ago
  [deleted]
dllthomas 10y ago
You can do this in GHC Haskell with existential quantification, or trade static checks for runtime with Data.Dynamic. (Again, not arguing against your thesis here.)