8 ms·

Reified Generics: The Search for the Cure

86 points by wstrange 8y ago

_hardwaregeek 8y ago
I'm nowhere near qualified enough to critique this article in a meaningful manner, but I've been thinking recently that types and compile time functions go hand in hand. Type systems are essentially an attempt to embed a logic that can prove various invariants about the code. What varies across type system to type system is A. what you can express and B. how much you can check. The issue is, most programming language designers decide these two things for you. That's why stuff like reification vs type erasure bites designers; the decision is irreversible. But what if it wasn't? And this seems to be what this article is proposing. That if you can write compile time functions that deal with types as a construct, you can leave decisions like type erasure and reification to the programmer. Granted, that essentially forces programmers to act as language designers. And I doubt most programmers want to learn stuff like type rules or how to prove soundness. However it does have some really cool implications. Like right now, Ruby has this whole debate over adding types. And sure, Ruby could just add normal static typing with some annotations and it'd work. But it kind of doesn't make sense for such a dynamic language to use such a static construct. What'd make more sense (to me) is some sort of metaprogramming on code that allows for checking invariants. Like being able to load a class, then run it through a checker at runtime. I've been reading a book on dependent types (The Little Typer) and the whole idea of types having types with a meta-type of sorts (universes in dependent types, meta classes in Ruby) seems very applicable to Ruby.
- reificator 8y ago
  Your next step on this journey is to learn a LISP.
  - _hardwaregeek 8y ago
    Actually the source for this thought process was going to Racket School and seeing them explain Turnstile and typechecking via syntax-parse and compile time functions :D. It's a fascinating idea but I'm skeptical of the whole "every library is a language" philosophy of Racket scaling. Bugs like infinite compile times are fine when you're writing all the code, but it breaks down when you have libraries.
    - TheDong 8y ago
      As opposed to the current state of the art in more "normal" languages where bugs result in infinite loops / deadlocks at runtime. I've imported many a library which deadlocked, crashed, or infinite looped. In reality it's not that big a deal; it happens and you figure out the bug.
- danharaj 8y ago
  The main issue is that designing a good type system is a dark art. The more powerful a type system, the easier it is to manipulate terms but the harder it is to reason about types. That's the fundamental tradeoff. Being able to specify your own type language is like having an untyped language governing your term language. There are promising directions though. In 20 years they might even have matured.
  - YorkshireSeason 8y ago
    That's the fundamental tradeoff. I'd like to refine this to: the fundamental tradeoff is between expressivity of the typing system and computational complexity of type-inference. Hindley-Milner's polymorphic typing system "has hit a sweetspot" (B. Pierce) between expressivity, type-inference. Almost every extension to Hindley-Milner makes full type inference undecidable.
    - danharaj 8y ago
      Type inference is just one part of it. That's taking a term and asking "what type could this have?" Another thing you can do is turn it around and ask "what terms have this type?". That question also gets complicated easily. And that's principled type systems. If you put ad hoc garbage into the types it might be inferrable and whatnot but still be ridiculous to reason about.
      - YorkshireSeason 8y ago
        what terms have this type? This is a very interesting question, but one that is rarely asked by compilers or by programmers, or indeed by theoreticians. I conjecture that the complexity of both questions is related, although I admit that I'd be hard-pressed even to define properly what the complexity of "what type could this have?" might be.
        danharaj 8y ago
        Oh, it's more common a question than you suggest. If I am writing a block of code and I come to some hole in context, for example `foo (bar _) baz`, and I know what type of thing has to go in that hole, then the very next thing I ask is "What term do I need there?". This is a big question for theoreticians working on new languages. The problem is called canonicity in that context. Here is an example of such a proof of "What terms have this type [in this context]?": https://arxiv.org/abs/1607.04156 https://arxiv.org/abs/1607.04156 And finally, compilers will ask this question if they're nice to you :) Here is GHC recently gaining the ability to ask this: https://phabricator.haskell.org/D3361 https://phabricator.haskell.org/D3361 The questions are related by proofs of cut elimination / normalization, which is the compatibility between a term and its context. Complex types describe more complex interactions between terms and contexts. Higher rank polymorphism has undecidable inference because a higher rank type can be used in very complex contexts.
- naasking 8y ago
  > I've been thinking recently that types and compile time functions go hand in hand. Type checking is a stage: http://lambda-the-ultimate.org/node/2575 http://lambda-the-ultimate.org/node/2575 Type systems as macros: http://lambda-the-ultimate.org/node/5426 http://lambda-the-ultimate.org/node/5426
- jules 8y ago
  Dependently typed languages do use the same evaluation mechanism for the type level and value level. In Java you have List<Int> and that's different than foo(bar), but in dependently typed languages Int is just a value of type Type, and List is a function that takes a Type and returns a Type. The difference is that this evaluation takes place at compile time. For run-time checking there is the work on higher order contracts. That's a systematic way to create wrappers around functions that check the input and output values against a contract. For example, the contract A -> B applied to a function f wraps f with a check on the input and output. The A and B itself can be primitive contracts such as Int which just checks if a value is an int, or function contracts, so that you can have (Int -> Int) -> Int. The neat thing about contracts is that they can tell you whose fault it is if something goes wrong. If you wrap f with the contract (Int -> Int) -> Int, and you call f(g) with some function g, then the contract will ensure that f can only pass Int to g, and if it passes something else the contract will tell you that's f's fault. On the other hand, if g returns something that's not an Int, then the contract can tell you that's g's fault. In general for some value v wrapped with a contract C evaluated in a context E(v wrapped with C), the contract can tell you if it's v's fault if something goes wrong, or E's fault. This is very helpful if v is a module and E is code that uses the module: the contracts can tell you if the module is at fault or whether the user of the module is at fault.
Groxx 8y ago
So I totally buy the argument that you can reify your own generics with a system like this. It's nice, I like it. ...but I don't see how this feeds into the compiler without a "shadow type system"[1]. If you have to specify the types everywhere, or don't have compile-time checks, it's not really generics. It's just an Object-container that has validation funcs executed at runtime, which can already be done relatively easily in basically every language. Did I miss something? [1]: or compile-time code generation, but that isn't mentioned. and that strikes me more as a macro system than a type system (though I don't know if that's a real distinction, if your macros are sufficiently powerful™)
- chriswarbo 8y ago
  > If you have to specify the types everywhere, or don't have compile-time checks, it's not really generics. Specify which types everywhere? If you mean specifying the concrete types (e.g. `Integer` and `List[Integer]`, then I'd agree. If you mean type variables (e.g. `T` and `List[T]`) then I disagree: that's a perfectly valid way to do generics, and having to annotate stuff is just a deficiency of inference (no worse than, say, Java). The key is that we're allowed to use the argument names and function/method names in our types, thanks to the 2 given rules. We don't need to lift those functions up to the type level, since we're only checking that the inputs and outputs line up. To me, this seems to be a form of dependent types. Note that "dependent types" only refers to the ability of having types refer to values, e.g. dependent function types like `(n : Int) -> Foo n` or dependent pairs like `(n : Int, Bar n)`. Most dependently typed languages also treat types as first-class language constructs, allow the type-checker to run arbitrary code (which usually implies that computations are pure and everything terminates/coterminates). Those latter aspects don't seem to apply here: it's just about using value-level names in our types. I think this works quite nicely, from a theoretical point of view; but I wonder what would happen in more complicated situations. When type checking is purely syntactic, we can easily get stuck with mismatched things like "should have type 'T', got type 'Pair[T, U].first()'". That's where we need type-level computation, to reduce things down to normal forms so that the syntactic checks (are more likely to) work.
  - Groxx 8y ago
zmmmmm 8y ago
This sounds very academic. Meantime in the real world, people in Java-land are constantly killing themselves trying to invent workarounds for type erasure induced problems. The latest example I know of being Micronaut [1] which touts itself in some sense as being a whole platform for re-reification. [1] https://objectcomputing.com/news/2018/10/08/micronaut-10-rc2 https://objectcomputing.com/news/2018/10/08/micronaut-10-rc2
- AstralStorm 8y ago
  This is because the decision to type erase was very weird for a strong static typed language... You inject weak typing (unexpected conversations) into a strong type system by doing that.
  - stewbrew 8y ago
    "Weird" is a strong word. Once the compiler has proven the codes satisfies certain type constraints you usually don't need the type information anymore ... except when you do of course.
    - deleted 8y ago
      [deleted]
- chriswarbo 8y ago
  > This sounds very academic. Meantime in the real world, people in Java-land are constantly killing themselves trying to invent workarounds for type erasure induced problems. Are you a manager at Sun by any chance? ;) See the "tangent; tl;dr" section in the article: "Sun management deluded themselves that Java was the ultimate programming language (though yours truly did try to hint, ever so gently, that further progress in PL was at least conceivable)." The author has spent a lot of effort trying to improve Java specifically, via language design committees, etc. AFAIK he was one of the lead designers of Java's reflection system. Looking through his past posts it's clear that Java was getting increasingly hampered by the consequences of past decisions, and the committees weren't aiming for the same direction Bracha would like to see, so he gave up that uphill battle in favour of working with newer languages which are either free from legacy baggage (e.g. Dart) or can serve as a demonstration that these ideas can actually be implemented and work (e.g. Newspeak). Whilst the latter is largely academic, it's basically a proof-of-principle for the former. For example, from https://gbracha.blogspot.com/2009/05/original-sin.html https://gbracha.blogspot.com/2009/05/original-sin.html (linked in the article as "There is no justification for primitive types in an object oriented language"): "I do not favor any of these features, but we will take them as a given." "I am not suggesting that this discussion should be reopened. This is just a mental exercise." "One of the many reasons I left Sun was because it was increasingly impossible to make meaningful progress on the language, or anything else for that matter."
skybrian 8y ago
It's not directly related, but this reminds me a bit of Zig's treatment of compile-time parameters [1], which seems somewhat more natural than generic parameters in most languages. Zig doesn't go all the way, though. Instead, a type parameter could be any combination of a compile-time and runtime parameter, depending how it's used. I do wonder how that affects calling conventions, though? If have separate linking then we probably need to avoid changing the calling convention if a function is modified so that a parameter is used in a different way. [1] https://andrewkelley.me/post/zig-programming-language-blurs-line-compile-time-run-time.html#compile-time-parameters https://andrewkelley.me/post/zig-programming-language-blurs-...
whateveracct 8y ago
Haskell has shown that you can have erased generics and have reified generics opt-in (i.e. Typeable and Generic). Works perfectly. And the vast majority of generic Haskell code does not have either of those constraints, which makes you think how important reified generics as-default really is.
- masklinn 8y ago
  > Haskell has shown that you can have erased generics and have reified generics opt-in (i.e. Typeable and Generic). Works perfectly. Haskell has little to no RTTI, which makes erased generic a non-issue. Java/C#/Dart have a lot of RTTI, which makes erased generics problematic. Without RTTI/reflection capabilities, generics reification become a performance tradeoff, with it they become a logic/correctness issue.
  - int_19h 8y ago
    It's not just RTTI. There are some idioms in OOP languages that legitimately ought to apply to generics, but don't if you erase. For a fairly common example, a class implementing several specializations of the same generic interface. Suppose we have Convertible<T> for something that can make a T out of itself - it would be perfectly reasonable for an object to be both Convertible<int> and Convertible<string>, but you can't do that in Java. And this doesn't require RTTI checks at call site at all - it might be that the caller is itself generic, and is just trying to accept something that's Convertible<U> for its own U.
    - bunderbunder 8y ago
      It also happens with method overloading. In Java, you can't have a class that has both of these methods at the same time: Integer sum(List<Integer> values) { ... } float sum(List<Float> values) { ... } because, as far as Java is concerned, both of these methods have exactly the same argument list. You also have no way in the language to express things like "Map<String, Option<Integer>>.class", which has some ergonomic implementations. (e.g., see: http://gafter.blogspot.com/2006/12/super-type-tokens.html http://gafter.blogspot.com/2006/12/super-type-tokens.html) The gotcha here, though, is that Haskell doesn't have these problems, or the one with implementing multiple specializations of the same generic type, even though it erases types much more completely than Java does. I'm not much of an expert on language design, but that leaves me thinking that there's probably a lot of stuff we lay at the feet of Java's type erasure that is actually more properly attributable to having a type system that is broken in some fundamental way. Or maybe it's the way that type erasure interacts with dynamic dispatch in an object-oriented language? Since the dynamic dispatch means that there are decisions about datatypes that a language like Haskell or ML can sort out at compile time, but that an OO language like Java must delay until run-time?
nicktelford 8y ago
I haven't seen anyone mention it yet, so I'll just point out that the kind of userland reification described in this article is also possible in Scala using implicits: class List[T](implicit tag: ClassTag[T]) { def elementType: Class[_] = tag.runtimeClass } You can do something similar for your own types in Java, albeit with less help from the compiler: public class List<T> { private final Class<T> t; public List(final Class<T> t) { this.t = t; } public Class<T> elementType() { return this.t; } } The problem is that you rarely own the definition of all the types you want/need to reify.

86 points by wstrange 8y ago

I'm nowhere near qualified enough to critique this article in a meaningful manner, but I've been thinking recently that types and compile time functions go hand in hand. Type systems are essentially an attempt to embed a logic that can prove various invariants about the code. What varies across type system to type system is A. what you can express and B. how much you can check. The issue is, most programming language designers decide these two things for you. That's why stuff like reification vs type erasure bites designers; the decision is irreversible. But what if it wasn't? And this seems to be what this article is proposing. That if you can write compile time functions that deal with types as a construct, you can leave decisions like type erasure and reification to the programmer. Granted, that essentially forces programmers to act as language designers. And I doubt most programmers want to learn stuff like type rules or how to prove soundness. However it does have some really cool implications. Like right now, Ruby has this whole debate over adding types. And sure, Ruby could just add normal static typing with some annotations and it'd work. But it kind of doesn't make sense for such a dynamic language to use such a static construct. What'd make more sense (to me) is some sort of metaprogramming on code that allows for checking invariants. Like being able to load a class, then run it through a checker at runtime. I've been reading a book on dependent types (The Little Typer) and the whole idea of types having types with a meta-type of sorts (universes in dependent types, meta classes in Ruby) seems very applicable to Ruby.

reificator 8y ago
Your next step on this journey is to learn a LISP.
- _hardwaregeek 8y ago
  Actually the source for this thought process was going to Racket School and seeing them explain Turnstile and typechecking via syntax-parse and compile time functions :D. It's a fascinating idea but I'm skeptical of the whole "every library is a language" philosophy of Racket scaling. Bugs like infinite compile times are fine when you're writing all the code, but it breaks down when you have libraries.
  - TheDong 8y ago
    As opposed to the current state of the art in more "normal" languages where bugs result in infinite loops / deadlocks at runtime. I've imported many a library which deadlocked, crashed, or infinite looped. In reality it's not that big a deal; it happens and you figure out the bug.
danharaj 8y ago
The main issue is that designing a good type system is a dark art. The more powerful a type system, the easier it is to manipulate terms but the harder it is to reason about types. That's the fundamental tradeoff. Being able to specify your own type language is like having an untyped language governing your term language. There are promising directions though. In 20 years they might even have matured.
- YorkshireSeason 8y ago
  That's the fundamental tradeoff. I'd like to refine this to: the fundamental tradeoff is between expressivity of the typing system and computational complexity of type-inference. Hindley-Milner's polymorphic typing system "has hit a sweetspot" (B. Pierce) between expressivity, type-inference. Almost every extension to Hindley-Milner makes full type inference undecidable.
  - danharaj 8y ago
    Type inference is just one part of it. That's taking a term and asking "what type could this have?" Another thing you can do is turn it around and ask "what terms have this type?". That question also gets complicated easily. And that's principled type systems. If you put ad hoc garbage into the types it might be inferrable and whatnot but still be ridiculous to reason about.
    - YorkshireSeason 8y ago
      what terms have this type? This is a very interesting question, but one that is rarely asked by compilers or by programmers, or indeed by theoreticians. I conjecture that the complexity of both questions is related, although I admit that I'd be hard-pressed even to define properly what the complexity of "what type could this have?" might be.
      - danharaj 8y ago
        Oh, it's more common a question than you suggest. If I am writing a block of code and I come to some hole in context, for example `foo (bar _) baz`, and I know what type of thing has to go in that hole, then the very next thing I ask is "What term do I need there?". This is a big question for theoreticians working on new languages. The problem is called canonicity in that context. Here is an example of such a proof of "What terms have this type [in this context]?": https://arxiv.org/abs/1607.04156 https://arxiv.org/abs/1607.04156 And finally, compilers will ask this question if they're nice to you :) Here is GHC recently gaining the ability to ask this: https://phabricator.haskell.org/D3361 https://phabricator.haskell.org/D3361 The questions are related by proofs of cut elimination / normalization, which is the compatibility between a term and its context. Complex types describe more complex interactions between terms and contexts. Higher rank polymorphism has undecidable inference because a higher rank type can be used in very complex contexts.
naasking 8y ago
> I've been thinking recently that types and compile time functions go hand in hand. Type checking is a stage: http://lambda-the-ultimate.org/node/2575 http://lambda-the-ultimate.org/node/2575 Type systems as macros: http://lambda-the-ultimate.org/node/5426 http://lambda-the-ultimate.org/node/5426
jules 8y ago
Dependently typed languages do use the same evaluation mechanism for the type level and value level. In Java you have List<Int> and that's different than foo(bar), but in dependently typed languages Int is just a value of type Type, and List is a function that takes a Type and returns a Type. The difference is that this evaluation takes place at compile time. For run-time checking there is the work on higher order contracts. That's a systematic way to create wrappers around functions that check the input and output values against a contract. For example, the contract A -> B applied to a function f wraps f with a check on the input and output. The A and B itself can be primitive contracts such as Int which just checks if a value is an int, or function contracts, so that you can have (Int -> Int) -> Int. The neat thing about contracts is that they can tell you whose fault it is if something goes wrong. If you wrap f with the contract (Int -> Int) -> Int, and you call f(g) with some function g, then the contract will ensure that f can only pass Int to g, and if it passes something else the contract will tell you that's f's fault. On the other hand, if g returns something that's not an Int, then the contract can tell you that's g's fault. In general for some value v wrapped with a contract C evaluated in a context E(v wrapped with C), the contract can tell you if it's v's fault if something goes wrong, or E's fault. This is very helpful if v is a module and E is code that uses the module: the contracts can tell you if the module is at fault or whether the user of the module is at fault.

Groxx 8y ago

So I totally buy the argument that you can reify your own generics with a system like this. It's nice, I like it. ...but I don't see how this feeds into the compiler without a "shadow type system"[1]. If you have to specify the types everywhere, or don't have compile-time checks, it's not really generics. It's just an Object-container that has validation funcs executed at runtime, which can already be done relatively easily in basically every language. Did I miss something? [1]: or compile-time code generation, but that isn't mentioned. and that strikes me more as a macro system than a type system (though I don't know if that's a real distinction, if your macros are sufficiently powerful™)

chriswarbo 8y ago
> If you have to specify the types everywhere, or don't have compile-time checks, it's not really generics. Specify which types everywhere? If you mean specifying the concrete types (e.g. `Integer` and `List[Integer]`, then I'd agree. If you mean type variables (e.g. `T` and `List[T]`) then I disagree: that's a perfectly valid way to do generics, and having to annotate stuff is just a deficiency of inference (no worse than, say, Java). The key is that we're allowed to use the argument names and function/method names in our types, thanks to the 2 given rules. We don't need to lift those functions up to the type level, since we're only checking that the inputs and outputs line up. To me, this seems to be a form of dependent types. Note that "dependent types" only refers to the ability of having types refer to values, e.g. dependent function types like `(n : Int) -> Foo n` or dependent pairs like `(n : Int, Bar n)`. Most dependently typed languages also treat types as first-class language constructs, allow the type-checker to run arbitrary code (which usually implies that computations are pure and everything terminates/coterminates). Those latter aspects don't seem to apply here: it's just about using value-level names in our types. I think this works quite nicely, from a theoretical point of view; but I wonder what would happen in more complicated situations. When type checking is purely syntactic, we can easily get stuck with mismatched things like "should have type 'T', got type 'Pair[T, U].first()'". That's where we need type-level computation, to reduce things down to normal forms so that the syntactic checks (are more likely to) work.
- Groxx 8y ago

zmmmmm 8y ago

This sounds very academic. Meantime in the real world, people in Java-land are constantly killing themselves trying to invent workarounds for type erasure induced problems. The latest example I know of being Micronaut [1] which touts itself in some sense as being a whole platform for re-reification. [1] https://objectcomputing.com/news/2018/10/08/micronaut-10-rc2 https://objectcomputing.com/news/2018/10/08/micronaut-10-rc2

AstralStorm 8y ago
This is because the decision to type erase was very weird for a strong static typed language... You inject weak typing (unexpected conversations) into a strong type system by doing that.
- stewbrew 8y ago
  "Weird" is a strong word. Once the compiler has proven the codes satisfies certain type constraints you usually don't need the type information anymore ... except when you do of course.
  - deleted 8y ago
    [deleted]
chriswarbo 8y ago
> This sounds very academic. Meantime in the real world, people in Java-land are constantly killing themselves trying to invent workarounds for type erasure induced problems. Are you a manager at Sun by any chance? ;) See the "tangent; tl;dr" section in the article: "Sun management deluded themselves that Java was the ultimate programming language (though yours truly did try to hint, ever so gently, that further progress in PL was at least conceivable)." The author has spent a lot of effort trying to improve Java specifically, via language design committees, etc. AFAIK he was one of the lead designers of Java's reflection system. Looking through his past posts it's clear that Java was getting increasingly hampered by the consequences of past decisions, and the committees weren't aiming for the same direction Bracha would like to see, so he gave up that uphill battle in favour of working with newer languages which are either free from legacy baggage (e.g. Dart) or can serve as a demonstration that these ideas can actually be implemented and work (e.g. Newspeak). Whilst the latter is largely academic, it's basically a proof-of-principle for the former. For example, from https://gbracha.blogspot.com/2009/05/original-sin.html https://gbracha.blogspot.com/2009/05/original-sin.html (linked in the article as "There is no justification for primitive types in an object oriented language"): "I do not favor any of these features, but we will take them as a given." "I am not suggesting that this discussion should be reopened. This is just a mental exercise." "One of the many reasons I left Sun was because it was increasingly impossible to make meaningful progress on the language, or anything else for that matter."

skybrian 8y ago

It's not directly related, but this reminds me a bit of Zig's treatment of compile-time parameters [1], which seems somewhat more natural than generic parameters in most languages. Zig doesn't go all the way, though. Instead, a type parameter could be any combination of a compile-time and runtime parameter, depending how it's used. I do wonder how that affects calling conventions, though? If have separate linking then we probably need to avoid changing the calling convention if a function is modified so that a parameter is used in a different way. [1] https://andrewkelley.me/post/zig-programming-language-blurs-line-compile-time-run-time.html#compile-time-parameters https://andrewkelley.me/post/zig-programming-language-blurs-...

whateveracct 8y ago

Haskell has shown that you can have erased generics and have reified generics opt-in (i.e. Typeable and Generic). Works perfectly. And the vast majority of generic Haskell code does not have either of those constraints, which makes you think how important reified generics as-default really is.

masklinn 8y ago
> Haskell has shown that you can have erased generics and have reified generics opt-in (i.e. Typeable and Generic). Works perfectly. Haskell has little to no RTTI, which makes erased generic a non-issue. Java/C#/Dart have a lot of RTTI, which makes erased generics problematic. Without RTTI/reflection capabilities, generics reification become a performance tradeoff, with it they become a logic/correctness issue.
- int_19h 8y ago
  It's not just RTTI. There are some idioms in OOP languages that legitimately ought to apply to generics, but don't if you erase. For a fairly common example, a class implementing several specializations of the same generic interface. Suppose we have Convertible<T> for something that can make a T out of itself - it would be perfectly reasonable for an object to be both Convertible<int> and Convertible<string>, but you can't do that in Java. And this doesn't require RTTI checks at call site at all - it might be that the caller is itself generic, and is just trying to accept something that's Convertible<U> for its own U.
  - bunderbunder 8y ago
    It also happens with method overloading. In Java, you can't have a class that has both of these methods at the same time: Integer sum(List<Integer> values) { ... } float sum(List<Float> values) { ... } because, as far as Java is concerned, both of these methods have exactly the same argument list. You also have no way in the language to express things like "Map<String, Option<Integer>>.class", which has some ergonomic implementations. (e.g., see: http://gafter.blogspot.com/2006/12/super-type-tokens.html http://gafter.blogspot.com/2006/12/super-type-tokens.html) The gotcha here, though, is that Haskell doesn't have these problems, or the one with implementing multiple specializations of the same generic type, even though it erases types much more completely than Java does. I'm not much of an expert on language design, but that leaves me thinking that there's probably a lot of stuff we lay at the feet of Java's type erasure that is actually more properly attributable to having a type system that is broken in some fundamental way. Or maybe it's the way that type erasure interacts with dynamic dispatch in an object-oriented language? Since the dynamic dispatch means that there are decisions about datatypes that a language like Haskell or ML can sort out at compile time, but that an OO language like Java must delay until run-time?

nicktelford 8y ago

I haven't seen anyone mention it yet, so I'll just point out that the kind of userland reification described in this article is also possible in Scala using implicits: class List[T](implicit tag: ClassTag[T]) { def elementType: Class[_] = tag.runtimeClass } You can do something similar for your own types in Java, albeit with less help from the compiler: public class List<T> { private final Class<T> t; public List(final Class<T> t) { this.t = t; } public Class<T> elementType() { return this.t; } } The problem is that you rarely own the definition of all the types you want/need to reify.