4 ms·
A System F type system can't be replaced by a dependent type system without affecting existing code. There is no way to turn the libraries in Haskell into libra
by firethief 9y ago
A System F type system can't be replaced by a dependent type system without affecting existing code. There is no way to turn the libraries in Haskell into libraries in dependently-typed Haskell without "porting them to a new language" and all the work that entails.
- taktoa 9y agoThis is 100% false. The Calculus of Constructions is a superset of System F. You may be thinking of the fact that if you want your type system to be sound when interpreted as a logic, then termination must be guaranteed (which would break backwards compatibility). Dependent types and totality are often found together, but are in actuality orthogonal features.