|
|
|
|
|
|
by rntz
3734 days ago
|
|
|
Decidability actually is optional; some folks experimenting with dependent type systems are bullish on giving up decidability (allowing type checking to fail to terminate in some cases). Typechecking is already 2^(2^PROGSIZE) for, say, ML. That could easily - in theory - lead to impracticably long compilation times. Yet in practice, it doesn't. So why not go whole hog? |
|
|