cur
cur copied to clipboard
Lack of documentation
Cur currently lacks any human readable documentation.
The number one thing I need right now is how elim works. I haven't been able to write any recursive functions so far because I just get a type error and I have no idea what's wrong.
How's this http://pkg-build.racket-lang.org/doc/cur@cur/Curnel_Forms.html#(form._((lib._cur/main..rkt)._elim))
Helps but it doesn't describe what how the types for the clauses of the elim form are generated. Are all of the inductive cases at the end or are they after the argument they're associated with (for instance)?
Also that's just a really simple example. Like when I have a (List A)
do I use (elim List ...)
or (elim (List A) ...
?
kk, will work on the documentation
By the way, just pushed changes to elim
so the interface just changed. There's slightly more complicated examples in documentation for cur/stdlib/sugar
. With these changes, you can also ask for the type of an eliminator (at compile time) via something like:
(begin-for-syntax
(displayln (type-infer/syn #'(lambda (A : Type) (elim (List A) Type)))))
Update: Documentation exists, but has never been proof read, and is missing all but the simplest examples.
Typos from Dan:
-
[x] but each tactic{drop s} insults the user, and works only some of the time.{remove future tense from writing, if at all possible. Future and past tense are mostly for historical writers and novelists; not for technical writing.)
-
[ ] "Only" "Remember, you get only one time to make a first impression."
The sentence demonstrates the proper placement of "only" (See "Bugs in Writing, 2nd ed.) (pg 23) and a reminder that what it says is true, so double and triple check things that go public.
"Only" is an adverb and may only modify (not kiss or dance with) the meaning of the word that follows it, which may be either an a verb, an adjective, or maybe another adverb (No example comes to mind.)
-
[x] "These features in includes compile-time functions for type-checking," closed by #42
Other bugs
- [x] Docs claim we don't do positivity checking; we do, now.