News for hackers. Stuff that matters.

A comment on Types as Interfaces. Parent comment

Re:Types as Interfaces by carapace on Tuesday July 23, 2024 @04:09PM (#41050263)
> 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.

[ Parent | on HN ]
Re:Types as Interfaces by mrkeen on Tuesday July 23, 2024 @05:44PM (#41051277)
Sure. If you're Haskell, you call them kinds. In Idris, they're just types.
[ Parent | on HN ]
Re:Types as Interfaces by carapace on Wednesday July 24, 2024 @08:42AM (#41056460)
Yes 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.
[ Parent | on HN ]