2 ms·
> a type should be capable of reflecting any arbitrary rules a programmer knows about the bounds of a value That's a programming language. In other words, now
by carapace 2y ago
> a type should be capable of reflecting any arbitrary rules a programmer knows about the bounds of a value
That's a programming language. In other words, now your type system needs a type system.
- mrkeen 2y agoSure. If you're Haskell, you call them kinds. In Idris, they're just types.
- carapace 2y agoYes but that misses the point. The pragmatic (not to say economic) motivation for type systems in the first place is to eliminate bugs in software. If you make them more complicated it makes it harder (more expensive, cost is always brought up as a barrier to correctness) to use them.