On 01/02/2013 10:09 AM, Matthias Felleisen wrote:
I remain worried that R programmers will want to use math and array and matrix
and friends and will experience performance problems when you have invested so
much work in doing it right the first time. But we will see.
They'll experience performance problems only for `math/array' and
`math/matrix'. Most everything else isn't higher-order.
3. ... I can't speak for anyone else, but when I get something ... to pass the
type checker, my code is usually correct.
I have heard this sentence often, in exactly this form. I have never believed
it...
I don't believe it, either, because it's obviously wrong. That's why the
array library has hundreds of test cases.
The "like `array-axis-reduce'" part is missing from that sentence,
probably because I wasn't very clear about what it means. Having had
time to mull it over, I've decided I meant "combinators". When I get a
combinator to pass the type checker, its implementation is usually correct.
The type of `unsafe-array-axis-reduce' is
(All (A B) ((Array A) Index (Index (Index -> A) -> B) -> (Array B)))
(Haskell, in Racket. It's so beautiful. *sniff*)
Like most combinators, it's not obvious from the type what it means. But
the type puts severe constraints on what can be done with the arguments.
Usually, when I "fill in" the code around a type like this, there are
only two options that pass the type checker, which also plausibly
implement what I want. For this, I had a test case in mind:
(unsafe-array-axis-reduce arr 0 build-list)
which reduced the two options to the correct one.
On the other hand, I've written monads in untyped Racket before. It...
really kind of sucks without having about 5x more test cases than code.
If you don't have them - and they can be hard to come up with, so it's
easy to leave them out - getting it right is awful. It's really easy to
have something you think works until you use some return/bind combo you
didn't think of before, which blows up.
I will freely acknowledge that type systems such as ML's, Haskell's, and ours
eliminate typo-level mistakes immediately. I am deeply skeptical about the
elimination of semantic bugs. That's not what these type systems are about.
I wonder if I could sum up by claiming that, with combinators, there's a
great amount of overlap between typos and semantic errors.
The simplest example I can think of is the type (All (A) (A -> A)),
which has only one correct implementation. Everything else is a typo.
Interesting. My extremely limited experience -- and Shriram's -- suggests an
eternal struggle with the numerical tower for 'beginners' like myself.
This is my experience as well.
One place this bit me pretty early was getting TR to optimize loops over
indexes *without using casts or assertions*. It's a puzzle, but it's
solvable with a couple of templates. Here's one to loop over [0..n-1]:
ensure n : Index ...
(let: loop ([i : Nonnegative-Fixnum 0] args ...)
(cond [(i . fx< . n) compute ...
(loop (fx+ i 1) args ...)]
[else answer ...]))
The optimizer changes `fx<' into `unsafe-fx<' and `fx+' into
`unsafe-fx+'. Also, (i . fx< . n) proves i : Index within "compute ...".
Here's a template to loop over [n-1..0]:
ensure n : Index ...
(let: loop ([i : Index n] args ...)
(cond [(i . fx= . 0) answer ...]
[else (let ([i (fx- i 1)])
compute ...
(loop i args ...))]))
The optimizer changes `fx=' and `fx-' to their unsafe counterparts.
Also, (i . fx= . 0) proves i : Positive-Index in the `else' branch, so i
: Index in "compute ...".
This should also work:
(let: loop ([i : Index n] args ...)
(cond [(i . fx> . 0) (let ([i (fx- i 1)])
compute ...
(loop i))]
[else answer ...]))
Unfortunately, (i . fx> . 0) doesn't prove i : Positive-Index, even
though it could.
This brings me to what I think is the major issue for us n00bs: the
types force you to understand the numeric tower really well if you want
to use types more precise than `Number'. Before you reach that level of
understanding, though, and Typed Racket spits errors at you, it's hard
to tell whether it has a legitimate complaint - especially when you
don't know whether you should expect, say, (i . fx> . 0) to prove i :
Positive-Index.
It would be really handy if TR could give counterexamples in these
cases. "This is how you can end up with an exact zero by multiplying an
exact rational and a flonum: (* 0 1.0)."
After you do understand the numeric tower well, you start looking for
ways to prove to TR that your code won't explode at runtime. It's not
always possible - again because, sometimes, the types aren't as precise
as they could be. But sometimes because it's just hard.
One fine example is `sqrt'. Its types are sensible:
> (sqrt (ann 5 Real))
- : Number
2.23606797749979
> (sqrt (ann 5 Nonnegative-Real))
- : Real [generalized from Nonnegative-Real]
2.23606797749979
But it's often really hard to prove that something is nonnegative
without an explicit cast, assertion, or test, and thus stay within the
reals in expressions with roots.
Neil ⊥
_________________________
Racket Developers list:
http://lists.racket-lang.org/dev
