3 ms·

OK, so I'm probably just confused here, but: It's not particularly surprising that structures have the same tag, but sum types (aka variants) do. (As you note.)

OK, so I'm probably just confused here, but: It's not particularly surprising that structures have the same tag, but sum types (aka variants) do. (As you note.) That's certainly runtime-information about the types of values, but I suppose our disagreement may be about the exact meaning of RTTI. After looking at the Wikipedia entry, I see that my intuition doesn't align with the C++ 'definition' of RTTI, either so thanks for correcting that misconception. It actually looks more like Haskell's Typeable in that it (can apply)/(applies) to any type even primitive types. Of course Typeable is opt-in and stored separately from the values, so... I'm still not sure I understand your objection, but maybe I just haven't read your OP closely enough and/or thought about it long enough.

colanderman 9y ago
The information in a variant has nothing to do with the type. I can declare: type foo = Bar of int | Baz of int And the two variant cases remain distinguishable, despite both having fields of the same type, and both being members of the same type. No information, runtime or otherwise, about the type, is involved. Therefore it is not by any definition RTTI. Pattern-matching is performed solely based on the explicit tag names. Consider that OCaml variants are in effect no different from the standard C pattern of enum + union. And I think we can agree that C has no RTTI whatsoever. Now if I could write: type foo = int | string Then pattern-matching that would require RTTI. But OCaml doesn't support such things.
- lomnakkus 9y ago
  You're just reiterating what we agree on. (I think I stated as much, but maybe not.) EDIT: Just in case: We do agree that certain programs in dependently typed languages would require such reification of type information, yes? That is, we're talking about a run-time decision about choosing a type (or another type), yes?
  - colanderman 9y ago
    I'm talking about run-time introspection into the type of a value. That is, the ability to ask the question, "is this arbitrary value an integer or a string?" That is what the OP needs for his example (clone an object of unknown type). That is something you need RTTI for, and something that I claim is better served by explicit variant tags. I don't know what you mean by "run-time decision about choosing a type (or another type)". Can you give an example of some code that does this? I also don't know what you mean by dependently typed languages requiring RTTI. Dependent type systems, like HM and other type systems, only constrain programs, they do not enable any behavior. Any program valid in an arbitrary dependently-typed language is still valid if the typing system is removed, rendering the language untyped (and thus devoid of any RTTI). (Specifically, DT adds to HM the ability to write expressions whose type or validity depends on other values. It does not grant ability to introspect those types; that is out of the scope of a type system.) Example: Coq is dependently typed, but has absolutely no notion of RTTI.
    - jcelerier 9y ago
      > Dependent type systems, like HM and other type systems, only constrain programs, they do not enable any behavior. The question arises when you have languages that compile to native code: you want your constraints to still be valid when you load new types in your program at run-time. eg obj = dlopen("libfoo.so") factory = /* insert some cast here */ dlsym(obj, "some_factory_function") a_value = factory.create_value() some_constrained_function(a_value)
      - colanderman 9y ago
        What part of that example requires RTTI? Clearly the type of `factory` (and thus the type of values it produces, even if they vary with input values) is known at compile time, thanks to the cast. And confirming that the dynamically loaded code adheres to that type is a loader problem (which can be solved with metadata), not a language/runtime problem (which would require RTTI and the overhead of checking it). The point of a static type system, either HM or a DT system, is to ensure that the types are either known at compile time, or derivable from some other runtime value (e.g. input to a function). This is for two reasons: safety, and the ability to elide RTTI. (Note that a type system forbids you from doing anything with a value with a dependent type until it finds its way into a conditional branch which simplifies its type to a non-dependent one.)

colanderman 9y ago

The information in a variant has nothing to do with the type. I can declare: type foo = Bar of int | Baz of int And the two variant cases remain distinguishable, despite both having fields of the same type, and both being members of the same type. No information, runtime or otherwise, about the type, is involved. Therefore it is not by any definition RTTI. Pattern-matching is performed solely based on the explicit tag names. Consider that OCaml variants are in effect no different from the standard C pattern of enum + union. And I think we can agree that C has no RTTI whatsoever. Now if I could write: type foo = int | string Then pattern-matching that would require RTTI. But OCaml doesn't support such things.

lomnakkus 9y ago
You're just reiterating what we agree on. (I think I stated as much, but maybe not.) EDIT: Just in case: We do agree that certain programs in dependently typed languages would require such reification of type information, yes? That is, we're talking about a run-time decision about choosing a type (or another type), yes?
- colanderman 9y ago
  I'm talking about run-time introspection into the type of a value. That is, the ability to ask the question, "is this arbitrary value an integer or a string?" That is what the OP needs for his example (clone an object of unknown type). That is something you need RTTI for, and something that I claim is better served by explicit variant tags. I don't know what you mean by "run-time decision about choosing a type (or another type)". Can you give an example of some code that does this? I also don't know what you mean by dependently typed languages requiring RTTI. Dependent type systems, like HM and other type systems, only constrain programs, they do not enable any behavior. Any program valid in an arbitrary dependently-typed language is still valid if the typing system is removed, rendering the language untyped (and thus devoid of any RTTI). (Specifically, DT adds to HM the ability to write expressions whose type or validity depends on other values. It does not grant ability to introspect those types; that is out of the scope of a type system.) Example: Coq is dependently typed, but has absolutely no notion of RTTI.
  - jcelerier 9y ago
    > Dependent type systems, like HM and other type systems, only constrain programs, they do not enable any behavior. The question arises when you have languages that compile to native code: you want your constraints to still be valid when you load new types in your program at run-time. eg obj = dlopen("libfoo.so") factory = /* insert some cast here */ dlsym(obj, "some_factory_function") a_value = factory.create_value() some_constrained_function(a_value)
    - colanderman 9y ago
      What part of that example requires RTTI? Clearly the type of `factory` (and thus the type of values it produces, even if they vary with input values) is known at compile time, thanks to the cast. And confirming that the dynamically loaded code adheres to that type is a loader problem (which can be solved with metadata), not a language/runtime problem (which would require RTTI and the overhead of checking it). The point of a static type system, either HM or a DT system, is to ensure that the types are either known at compile time, or derivable from some other runtime value (e.g. input to a function). This is for two reasons: safety, and the ability to elide RTTI. (Note that a type system forbids you from doing anything with a value with a dependent type until it finds its way into a conditional branch which simplifies its type to a non-dependent one.)