4 ms·
A good type system can affect the compiled code through valuable static analysis, though. Recognising when optimisations are possible via type restrictions or t
by ivanbakel 8y ago
A good type system can affect the compiled code through valuable static analysis, though. Recognising when optimisations are possible via type restrictions or techniques like monomorphising is an important part of modern typed compilers.
- AstralStorm 8y agoI'd prefer stronger methods like logic proofs and constraint or contract specifications. Compilers could use those even better to optimize and check the meaning of the program. Types are very limited logic constraints after all. While at it, you could ditch some of the old language. Ultimately, everything is just some place in memory, cache and/or CPU register.
- icebraining 8y agoDependent types can encode constraints and require proofs.
- AstralStorm 8y agoYes they do. In a supremely roundabout way typically making for ugly fat proofs for anything high order. Sometimes, rarely, they make proofs cleaner and more direct than high order logic. Plus there is the potential undecidability if you want to use automated type deduction. Hard to spot where the types have to be so to speak reified with bad error messages.