Re: [racket-dev] TR: Five feature/limitation interactions conspire to drive mad
On 12/31/2012 02:56 PM, Vincent St-Amour wrote:
At Mon, 31 Dec 2012 13:27:50 -0700,
Neil Toronto wrote:
2. Don't generalize argument types in let loops.
This is a bad idea. Often, inferring the types of loops only works
because of type generalization.
Agreed. Since this one is only a problem because of the other
limitations you list, ideally we should fix the others and leave this
one alone. Do you agree?
Very yes.
3. Allow let: loops to have unannotated arguments and return values.
This would totally work. I could use [i : Nonnegative-Fixnum 0] instead
of [#{i : Nonnegative-Fixnum} 0], and still not have to annotate `acc'
or the loop's return value.
Trying this one right now.
Thanks again. :D
4. Extend the set of types TR can produce contracts for.
This probably only works for first-order function types. It would be
helpful, but may not even work for functions with `Array' or `Matrix'
arguments (they're higher-order).
I can look into making contract generation smarter. Could you send me
a list of types that caused you issues with contract generation?
Actual examples are attached as a standalone Typed Racket program, with
the function bodies stubbed out. I think they cover pretty much all the
uses of `require/untyped-contract' in the math library.
Neil ⊥
#lang typed/racket
(struct: (A) Array ())
(define-type Indexes (Vectorof Index))
(define-type In-Indexes (U Indexes (Vectorof Integer)))
;;
---
;; Changing argument types from In-Indexes to (Vectorof Integer)
;; Most uses of `require/untyped-contract' in `math/array' are for this.
(: make-array (All (A) (In-Indexes A - (Array A
(define (make-array ds v)
(error 'undefined))
;; The contract can be created, but is ambiguous and always fails. Exported to
untyped Racket using
;; this subtype:
#;(All (A) ((Vectorof Integer) A - (Array A)))
;;
---
;; array-map's type
;; There was no subtype of this under which I could export it to untyped code:
(: array-map (All (R A B T ...)
(case- ((- R) - (Array R))
((A - R) (Array A) - (Array R))
((A B T ... T - R) (Array A) (Array B) (Array T) ...
T - (Array R)
(define array-map
(case-lambda
[(f) (error 'undefined)]
[(f arr) (error 'undefined)]
[(f arr0 arr1) (error 'undefined)]
[(f arr0 arr1 . arrs) (error 'undefined)]))
;; I ended up making a separate, typed implementation for untyped code, with
the type
#;(All (R A) (case- ((- R) - (Array R))
((A - R) (Array A) - (Array R))
((A A A * - R) (Array A) (Array A) (Array A) * - (Array
R
;;
---
;; Matrix argument types
;; Almost all uses of `require/untyped-contract' in `math/matrix' are for this.
(: matrix-determinant (case- ((Array Real) - Real)
((Array Number) - Number)))
(define (matrix-determinant M)
(error 'undefined))
;; Exported using the subtype
#;((Array Number) - Number)
;;
---
;; First-order numeric functions
;; Almost all uses of `require/untyped-contract' in `math/number-theory' and
`math/special-functions'
;; are variations of the following:
(: factorial (case- (Zero - One)
(One - One)
(Integer - Positive-Integer)))
(define (factorial n)
(error 'undefined))
;; Exported using the subtype
#;(Integer - Positive-Integer)
_
Racket Developers list:
http://lists.racket-lang.org/dev
[racket-dev] TR: Five feature/limitation interactions conspire to drive mad
The subject sounds complainy, and so will the rest of this email. So I
will state up front that I love Typed Racket, and I'm only frustrated
because I want to love it more.
Also, I apologize for the length of this email, but I have to tell a
story. Otherwise, I'll get a bunch of Why don't you try this? replies,
which I'll have to answer, leading to an inseparable tangle of ideas.
How the features and limitations interact is not always obvious.
The features and limitations are:
1. The reader is set by the #lang line, but not submodule forms.
2. Implicit argument types in let loops are generalized from the types
of their initial values.
3. let: loops require every argument type and the return type to be
annotated.
4. TR can't produce contracts for single-arity `case-' types.
5. Using single-arity `case-' types makes annotating function bodies
in certain ways impossible.
So here's my user story.
** ONCE UPON A TIME **
I'm working on `math/matrix'. TR doesn't do generics, which is fine for
now, but it means a lot of the matrix library's functions have to have
single-arity types like this:
(: matrix-hermitian (case- ((Matrix Real) - (Matrix Real))
((Matrix Number) - (Matrix Number
It could be (Matrix Number) - (Matrix Number). But the real matrices
are closed under almost every matrix operation, so `math/matrix'
shouldn't make users worry needlessly about complex numbers.
Annotating expressions inside the bodies of functions with single-arity
`case-' types like that is often impossible, because there's no name
for polymorphic type arguments (in this case, either `Real' or
`Number'). To separate the issues from `math/matrix', consider this
function instead:
(: repeat+1 (case- (Index Real - (Listof Real))
(Index Number - (Listof Number
(define (repeat+1 n num)
(let loop ([i 0] [acc empty])
(cond [( i n) (loop (+ i 1) (cons (+ num 1) acc))]
[else acc])))
It should act like this:
(repeat+1 3 10)
- : (Listof Real)
'(11 11 11)
(repeat+1 0 11+4i)
- : (Listof Number)
'()
But it doesn't type:
Type Checker: Expected (Listof Real), but got (Listof Any) in: acc
Type Checker: Expected (Listof Number), but got (Listof Any) in: acc
The highlighted expression is the `acc' inside of [else acc]. The
causes: TR gives the expression `empty' the type (Listof Any) in both
passes through the function body (one for each case).
The level of inference TR does is generally fine, requiring few
annotations. The problem here is that *I can't annotate `empty'*. I
don't have a name for the type argument to `Listof'.
Here's one annotation-less solution:
(define (repeat+1 n num)
(cond [(= n 0) empty]
[else
(let loop ([i 1] [acc (list (+ num 1))])
(cond [( i n) (loop (+ i 1) (cons (+ num 1) acc))]
[else acc]))]))
TR helpfully generalizes the type of (list (+ num 1)) from (List Real)
to (Listof Real) in the first typechecking pass and from (List Number)
to (Listof Number) in the second typechecking pass, so `acc' has the
correct type in both passes.
I committed the off-by-one error [i 0] and the copy error [acc (list
num)] while deriving that solution. Not liking either kind of error, I
figure this is safer, and also cleverer:
(define (repeat+1 n num)
(let loop ([i 0] [acc (rest (list num))])
(cond [( i n) (loop (+ i 1) (cons (+ num 1) acc))]
[else acc])))
I'm trying to get a properly typed `empty' by taking the rest of a
one-element list.
I get two type errors like this, highlighting (cons (+ num 1) acc):
Type Checker: Polymorphic function cons could not be applied to
arguments:
Types: a (Listof a) - (Listof a)
a b - (Pairof a b)
Arguments: Real (Listof Nothing)
Expected result: (Listof Nothing)
Ah, I see what happened. TR generalized from the type of (rest (list
num)), which is (Listof Nothing) because (list num) has the type (List
Real) or (List Number). I need to force it to generalize differently.
One way to do that is to turn the base case into a call to a polymorphic
function like `empty-listof':
(define (repeat+1 n num)
(let loop ([i 0] [acc (empty-listof num)])
(cond [( i n) (loop (+ i 1) (cons (+ num 1) acc))]
[else acc])))
(: empty-listof (All (A) (A - (Listof A
(define (empty-listof x) (rest (list x)))
Basically, `empty-listof' gives me a way to name the type parameter to
`Listof' in that one expression.
Well, it's either this or the wordier version, and this abstracts a
little better. So I'll package it up. First, though, I want to make the
loop faster. It turns out that this:
[#{i : Nonnegative-Fixnum} 0]
is enough to turn `' and `+' into `unsafe-fx' and `unsafe-fx+', and I
still don't have to annotate `acc' or the loop's return value. Awesome.
Provide and commit.
Re: [racket-dev] TR: Five feature/limitation interactions conspire to drive mad
First, though, I want to make the loop faster. It turns out that this:
[#{i : Nonnegative-Fixnum} 0]
is enough to turn `' and `+' into `unsafe-fx' and `unsafe-fx+', and I
still don't have to annotate `acc' or the loop's return value. Awesome.
Provide and commit.
Posted about this annoyance long back pleading for a special Index
increment operator that TR would optimize. [#{i: Nonnegative-Fixnum} 0] is
a slick idea. Thanks for that one.
_
Racket Developers list:
http://lists.racket-lang.org/dev
Re: [racket-dev] TR: Five feature/limitation interactions conspire to drive mad
At Mon, 31 Dec 2012 13:27:50 -0700,
Neil Toronto wrote:
1. Allow submodules to extend the reader.
Would using `#lang typed/racket/no-check' instead of `#lang racket' for
the top-level module work? It extends the reader and provides TR's
annotated forms, but otherwise counts as an untyped language.
That's not a general solution, but it may solve your problem.
2. Don't generalize argument types in let loops.
This is a bad idea. Often, inferring the types of loops only works
because of type generalization.
Agreed. Since this one is only a problem because of the other
limitations you list, ideally we should fix the others and leave this
one alone. Do you agree?
3. Allow let: loops to have unannotated arguments and return values.
This would totally work. I could use [i : Nonnegative-Fixnum 0] instead
of [#{i : Nonnegative-Fixnum} 0], and still not have to annotate `acc'
or the loop's return value.
Trying this one right now.
I think all of TR's annotating forms should allow any annotation to be
left out.
I'll look into that next.
4. Extend the set of types TR can produce contracts for.
This probably only works for first-order function types. It would be
helpful, but may not even work for functions with `Array' or `Matrix'
arguments (they're higher-order).
I can look into making contract generation smarter. Could you send me
a list of types that caused you issues with contract generation?
There are two more general solutions to the first problem, that
single-arity `case-' types sometimes make annotating impossible:
5. Find some way to name the polymorphic arguments in `case-' types.
Yes. This. At least 25% of my time refactoring `math/matrix' has gone to
writing twisty, annotation-free function bodies.
I agree that this would be useful. Sam, do you think this is doable?
In general, we need a better story for scaling up programming with
intersection types.
Vincent
_
Racket Developers list:
http://lists.racket-lang.org/dev
Re: [racket-dev] TR: Five feature/limitation interactions conspire to drive mad
On Mon, Dec 31, 2012 at 3:27 PM, Neil Toronto neil.toro...@gmail.com wrote: 1. Allow submodules to extend the reader. This seems hard, because module forms are expanded after they've been read. One possibility is a #module reader macro. Seems like overkill. This, at least, has an easy solution -- use the `#reader` form with `typed-racket/typed-reader` collection, which provides `read` and `read-syntax`. Sam _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] TR: Five feature/limitation interactions conspire to drive mad
On Mon, Dec 31, 2012 at 4:56 PM, Vincent St-Amour stamo...@ccs.neu.edu wrote: In general, we need a better story for scaling up programming with intersection types. I agree with this. There are two more general solutions to the first problem, that single-arity `case-' types sometimes make annotating impossible: 5. Find some way to name the polymorphic arguments in `case-' types. Yes. This. At least 25% of my time refactoring `math/matrix' has gone to writing twisty, annotation-free function bodies. I agree that this would be useful. Sam, do you think this is doable? I'm not sure that an ad-hoc naming solution is the right thing. I really want to avoid adding more ad-hoc complexity to the Typed Racket type checker, and instead work on simplifying it into something that can be more precisely characterized, and thus be more sure that it's implemented correctly. Is there a generalization of this solution that we can give a clean story for? Sam _ Racket Developers list: http://lists.racket-lang.org/dev
