Re:A project with a single 11,000-line code file
by CornCobs on Monday April 04, 2022 @12:37AM
(#30903342)
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
[ Parent
| on HN ]
Re:A project with a single 11,000-line code file
by klibertp on Monday April 04, 2022 @08:50AM
(#30906010)
Well, 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_Featu...