4 ms·

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

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.)
    - jcelerier 9y ago
      > thanks to the cast. well, exactly: languages are able to do without the cast at all, just extracting type information from the runtime, which is much safer.
      - colanderman 9y ago
        You wrote the example, not me. I'm confused what your argument is. Are you saying that dynamic loaders should check the type of dynamically loaded code against the type expected by the code loading it? I agree that's a good idea, but it doesn't require language support for general RTTI, just a type-aware shared-object format and dynamic loader. (Heck, C++ symbol names already incorporate function argument type signatures, so this isn't a huge stretch.) Are you saying that a runtime shouldn't need to trust that dynamically-loaded code actually implements the interface it claims to? If so, that's an incredibly specific requirement that's really better served by sandboxing or an RPC-like interface (especially in C/C++).

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.)
  - jcelerier 9y ago
    > thanks to the cast. well, exactly: languages are able to do without the cast at all, just extracting type information from the runtime, which is much safer.
    - colanderman 9y ago
      You wrote the example, not me. I'm confused what your argument is. Are you saying that dynamic loaders should check the type of dynamically loaded code against the type expected by the code loading it? I agree that's a good idea, but it doesn't require language support for general RTTI, just a type-aware shared-object format and dynamic loader. (Heck, C++ symbol names already incorporate function argument type signatures, so this isn't a huge stretch.) Are you saying that a runtime shouldn't need to trust that dynamically-loaded code actually implements the interface it claims to? If so, that's an incredibly specific requirement that's really better served by sandboxing or an RPC-like interface (especially in C/C++).