Re:A project with a single 11,000-line code file
by exdsq on Sunday April 03, 2022 @07:33PM
(#30901853)
It's nice to have invariants - I believe I've seen them in Rackets contracts but I'm a little away from that stuff in my Lisp journey :)
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
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...
I've been implementing it for a couple years now, though not seriously till the past couple months. There are some interesting (and overlooked) ideas in Bel.
Bel is sort of the limit case of generality. For example, you might expect the "type" above to be a separate kind of object, the way that types are separate kinds of things in TypeScript.
But in fact, it's simply a function that receives the argument and can throw an error. So for example, you can do something like:
I just wish he'd solved keyword arguments as thoroughly as every other kind of argument. There are hints that it was always in the back of his mind. Though it's true he never needed them, so that's probably why he never made them.