|
|
|
|
|
by lifthrasiir
1801 days ago
|
|
As others have mentioned (only partially though, hence this summary), there are several ways (with varying trade-offs) to achieve this. Multi-stage programming languages have, well, multiple stages of compilation and you can manipulate types as a first-class value in higher stages. This is a natural extension to the type-level evaluation, as the only thing changes is that the type-level evaluation uses the same fragment of language as the value-level evaluation. Of course we would then have a type of types, a type of types of types and so on; some languages do not distinguish them and a single meta-type is used as catch-all. This model is powerful but you wouldn't get stronger guarantees for lower stages; in particular this model is not a substitute for generic types which typically guarantee that every instance of a generic type is instantiable. (By the way it is a common misconception that being able to use something like `function f<T>() { return T.size; }` is a first-class type; the type parameter T and the lowered value T is a different thing in different stages.) Dependently typed languages extend the type system itself to handle mixed types and values. This can be much more huge undertaking than multi-staged programming and harder to reconcile with the type inference and other goodies typically available for strong (enough) type systems, but correctly done they can provide a very strong guarantee that was only possible with static analyses to the limited extent. Note that dependent typing is historically associated with proof assistants but still possible without them; its usefulness and usability would be limited though. (You might have guessed but this is why I don't think dependent typing at the current stage is not the future.) Conventional metaprogramming methods like macros or code generation are huge wrenches always available for throwing. (Multi-stage programming is also a kind of metaprogramming, but not included in the colloquial "metaprogramming".) They would be significantly limited in scope and/or inconvenient to use, but depending on the scope they might be still appropriate. |
|