TAL / Nuprl Differences
TAL concerned with safety
- Partial rather than total function spaces
TAL needs a tractible type system
- Decidable, linear in practice
TAL uses type erasure interpretation
- TAL forall means Nuprl intersection
TAL has impredicative polymorphism and general recursive types