Name: Anonymous 2009-07-30 2:50
The debate of whether to use dynamic or static typing has long since been dismissed by the usual sentiment of adaptive context. General wisdom holds that for large, complex systems, a static type system is beneficial towards giving structure, whilst a dynamic type system allows the flexibility needed for quickly evolving projects and specialized uses, such as reflection and metaprogramming. Of course, there are instances of cross-over use, but I'm speaking in general terms here.
What if, however, there were "hybrid" systems that allow for the advantages of both on demand? Indeed, the recent adventures on the JVM and CLR, and C++'s new standard all adopt somewhat of this idea. But simply "mixing" the two, I feel, is heavy handed and prone to abuse. Given enough effort, a modicum of dynamic power can corrupt the most strict of static systems.
Researchers have long known that advances in type theory mainly stem from the tension between power and safety. Surely there is a system that can afford both? Having thought upon this matter a bit, and done some light reading, I came upon this:
http://www.cs.chalmers.se/~jwr/pure/
A Pure Type System, it seems, combines both type safety and UNLIMITED POWER. Terms must still be constrained by their type, but those types are themselves terms, and so can represent any arbitrary specification. With an infinite tower of terms, even the most extravagant dynamic ideas are statically checked for consistency.
So, /prog/, discuss.
What if, however, there were "hybrid" systems that allow for the advantages of both on demand? Indeed, the recent adventures on the JVM and CLR, and C++'s new standard all adopt somewhat of this idea. But simply "mixing" the two, I feel, is heavy handed and prone to abuse. Given enough effort, a modicum of dynamic power can corrupt the most strict of static systems.
Researchers have long known that advances in type theory mainly stem from the tension between power and safety. Surely there is a system that can afford both? Having thought upon this matter a bit, and done some light reading, I came upon this:
http://www.cs.chalmers.se/~jwr/pure/
A Pure Type System, it seems, combines both type safety and UNLIMITED POWER. Terms must still be constrained by their type, but those types are themselves terms, and so can represent any arbitrary specification. With an infinite tower of terms, even the most extravagant dynamic ideas are statically checked for consistency.
So, /prog/, discuss.