4 ms·
That doesn't really allow for type checking which is a major purpose of types. It's more of just some nice sugar for runtime assertions
by CornCobs 5y ago
That doesn't really allow for type checking which is a major purpose of types. It's more of just some nice sugar for runtime assertions
- klibertp 5y agoWell, you can interpret the predicate function body as a set of constraints on the type. Of course, such predicate function would need to be restricted to what your type system can handle. Typed Racket does this, by allowing you to implement type refinements[1]. As long as the predicate only uses operations listed there, it can be used for type checking. Idris also lets you write functions that operate on types and that are used for type checking. [1] https://docs.racket-lang.org/ts-reference/Experimental_Features.html#%28form._%28%28lib._typed-racket%2Fbase-env%2Fbase-types-extra..rkt%29._.Refine%29%29 https://docs.racket-lang.org/ts-reference/Experimental_Featu...