3 ms·

A type is an expression. The type of an expression is the result of evaluating the type expression, in this case, "list a". In other words, the type constructo

A type is an expression. The type of an expression is the result of evaluating the type expression, in this case, "list a". In other words, the type constructor invocation that gives the expression its type is itself an expression. In that context, I'm wondering how type expressions differ from "stages"--does the type expression language need to be sufficiently complex (e.g., Turing complete)?

naasking 9y ago
> A type is an expression. A type is not an expression. We wouldn't have two words designating the same concept. Even in dependently typed languages where types and expressions are intermingled, they are still distinct concepts. Now, you can sort of talk about expressions in the "type language", but these are not expressions of the "value language". Even so, an unqualified statement like "a type is an expression" is simply incorrect because "expression" always refers to the value language, so that phrase conveys the completely wrong intention. Finally, as for how to relate staging to concepts you might be more familiar with, I suggest the paper, Closing the Stage: From Staged Code to Typed Closures [1]. [1] http://lambda-the-ultimate.org/node/2575 http://lambda-the-ultimate.org/node/2575
- weberc2 9y ago
  Types (or "type expressions") are expressions whose type is type. In other words, types are higher order expressions. It's a poor definition or discipline that doesn't capture this basic concept.
  - naasking 9y ago
    > Types (or "type expressions") are expressions whose type is type. This is only true in dependently typed languages. And even then, soundness requires stratifying types into universes or something similar. > In other words, types are higher order expressions. This isn't the meaning of higher order as it applies to programming languages or the standard isomorphism to logic.

naasking 9y ago

> A type is an expression. A type is not an expression. We wouldn't have two words designating the same concept. Even in dependently typed languages where types and expressions are intermingled, they are still distinct concepts. Now, you can sort of talk about expressions in the "type language", but these are not expressions of the "value language". Even so, an unqualified statement like "a type is an expression" is simply incorrect because "expression" always refers to the value language, so that phrase conveys the completely wrong intention. Finally, as for how to relate staging to concepts you might be more familiar with, I suggest the paper, Closing the Stage: From Staged Code to Typed Closures [1]. [1] http://lambda-the-ultimate.org/node/2575 http://lambda-the-ultimate.org/node/2575

weberc2 9y ago
Types (or "type expressions") are expressions whose type is type. In other words, types are higher order expressions. It's a poor definition or discipline that doesn't capture this basic concept.
- naasking 9y ago
  > Types (or "type expressions") are expressions whose type is type. This is only true in dependently typed languages. And even then, soundness requires stratifying types into universes or something similar. > In other words, types are higher order expressions. This isn't the meaning of higher order as it applies to programming languages or the standard isomorphism to logic.