[racket] Typed Racket reactions on developing polymorphic typed array library, and questions
Neil Toronto
by doing some 2D OpenGL game-type stuff in Racket. I decided that I
needed a nice array implementation, and later, that it should be in
Typed Racket so I could wring out as much performance as possible.
(I've read the array SRFIs. The arrays are untyped and underdeveloped,
and could probably never run at interactive speeds in my little demo.)
This email is feedback on using Typed Racket to develop a new library
(i.e. it isn't originally untyped code) that's about 3500 lines long,
and some questions.
I was inspired by Racket's sequences and the "for" macros that allow
looping over different kinds of sequence models using (almost) the same
syntax. I've made an analogous "array"/"arrayn" abstraction ("n" suffix
means multidimensional) to represent fixed-size data that is indexed by
natural numbers, is random-access, and is read-only or read/write.
Therefore, an array is a length (or shape for arrayn) and two
procedures: unsafe-ref and unsafe-set!. Vectors, flvectors, strings, and
bytes are "models" of arrays, and creating an array from one makes a
"view" of it.
Some macros with names starting with "forall" provide syntactic sugar
for mapping over arrays simultaneously. Here's an example of use:
(foralln/flvectorn:
([x : Float (<-flvectorn xs)]
[y : Float (<-flvectorn ys)])
(for/fold: : Float ([dm : Float 0.0]) ([pt : vec2 (in-list pts)])
(+ dm (delta-mass-from pt (vec2 x y))))))
Here, "flvectorn" is an N-dimensional flvector, and "<-flvectorn" is
special syntax like "in-list" (i.e. forall recognizes it as creating an
array backed by an flvectorn and inlines unsafe-flvectorn-ref accordingly).
Vincent will be happy to know that all the flonum and fixnum ops are
changed by TR's optimizer to be unsafe. (Except a certain add1 that TR
can't prove doesn't overflow; I can prove it, so I changed it myself.)
From my admittedly limited tests, I'd say that this particular forall
gets within spitting distance of equivalent C code. ("Spitting distance"
is a technical term meaning "within 3x to 5x time elapsed".) There's a
"foralln!:" that destructively updates arrays, which might get a little
closer; perhaps it gets within pinching distance of the C equivalent's
buttocks.
The rest of my reactions and questions follow.
- Indentation is in a rather evil state in TR. Could DrRacket have
more than one regexp for each "*-like keyword"? That would make it
easier to auto-indent TR's built-in loop syntax, or any other syntax
(like forall) that is in a state of flux. The indentation rules for
for/*: loops could be tricky because of the required "return" type - but
see the next item.
- Why require "return" or body types for for/*: loops in TR? I haven't
needed them in forall/*: loops. Also, writing the "Listof" in "for/list:
: (Listof T)" is annoying. I know it's a list from reading "for/list:",
and for/list: knows it, too. I also know the return type of a
"for/fold:" from the accumulators' types; why require them twice? I'm
also annoyed by having to give a body type for every named "let:".
Similarly, why require return types for functions defined with
"define:"? I'd almost rather write lambdas than give another annotation.
(Not that I use define: very much.)
I don't think it's just a preference for less verbosity. Here, TR can
support good "contracts" practice: it would usually give a more specific
body type or return type than I do. On the rare occasions it confuses
itself, I can annotate the body.
- I'm impressed by TR's dogged consistency, even though sometimes it
makes me want to go to the local animal shelter and flip off all the
kittens. I'm also impressed by its safety. I've occasionally tried to
break it for performance reasons, but couldn't.
- Related: can we get a runtime cast/refine macro? Occurrence typing
makes a naive one easy to implement: (let ([x <expr>]) (if (pred? x) x
(error ...))). Easy implementation means everyone will duplicate it;
might as well incorporate a good one.
- I've found it useful to have a macro shaped like (with-refine* ([x
pred?] ...) body ...). I have a lot of functions that take Integer and
(Listof Integer) arguments, but actually operate only on
Nonnegative-Fixnum indexes. (Nonnegativity and fixnum-ness are hard for
TR to prove.) The function bodies are wrapped with this macro.
- Requiring the 3500-line array library makes compilation take 5-10
more seconds on my desktop machine. On my laptop, it takes an
excruciating *minute* extra. It's an Eee-PC, but Racket is generally
only 2x slower on it. I think it's the extra magic syntax that types
introduce, not the checking itself, because it takes a minute to either
run the code or to tell me that I've misspelled an identifier.
I haven't felt so impatient with a compiler since programming in C++
with templates.
- Polymorphic structs being proper subtypes of their parent structs
would be really nice. As it is, I can't figure out how to cleanly have a
"(vector-array T)" subtype of "(array T)" that gives private array
functions access to the vector backing an array. If I had that, I could
collapse compositions of certain array ops at runtime and remove some
duplicate bounds checks.
- Futures don't work with TR. I had to use require/typed to get them,
so I gather that they're not officially supported. From what I can tell,
for TR code, the JIT gives a large max_let_depth to even simple thunks
like (lambda () 1). It's a shame, because splitting up forall loops with
bodies that use nothing but float ops seems like a killer app for futures.
- Pie-in-the-sky: notice that "<-flvectorn" above is really just a
type annotation that the forall macro understands. It would be nice if
compositional macros could get the types of their arguments - I could
have forall map over any array-like thing without requiring a
declaration of what it is.
I understand why this is hard: the inferred types depend on expansion,
and the expansion would depend on types. While tricky, it seems that
finding a fixpoint w.r.t. the subtype relation could work. Most macros
would iterate zero times or once. Expanding to expressions with
uncomparable types would be an error.
Typeclasses allow function dispatch on the types of arguments; this
would allow a sort of macro dispatch on the types of expanded inner
syntax. You could probably define typeclasses in terms of it.
Don't attack it too fiercely, though, as I haven't given it much deep
thought. :) Also, it is a pie... in the sky.
Neil T
_________________________________________________
For list-related administrative tasks:
http://lists.racket-lang.org/listinfo/users
Sam Tobin-Hochstadt
> This email is feedback on using Typed Racket to develop a new library (i.e.
> it isn't originally untyped code) that's about 3500 lines long, and some
> questions.
Thanks for the feedback!
> Some macros with names starting with "forall" provide syntactic sugar for
> mapping over arrays simultaneously. Here's an example of use:
>
> (foralln/flvectorn:
> ([x : Float (<-flvectorn xs)]
> [y : Float (<-flvectorn ys)])
> (for/fold: : Float ([dm : Float 0.0]) ([pt : vec2 (in-list pts)])
> (+ dm (delta-mass-from pt (vec2 x y))))))
>
> Here, "flvectorn" is an N-dimensional flvector, and "<-flvectorn" is special
> syntax like "in-list" (i.e. forall recognizes it as creating an array backed
> by an flvectorn and inlines unsafe-flvectorn-ref accordingly).
Is this the same as the (brand-new) `for/flvector' and `in-flvector'?
> - Why require "return" or body types for for/*: loops in TR? I haven't
> needed them in forall/*: loops. Also, writing the "Listof" in "for/list: :
> (Listof T)" is annoying. I know it's a list from reading "for/list:", and
> for/list: knows it, too. I also know the return type of a "for/fold:" from
> the accumulators' types; why require them twice? I'm also annoyed by having
> to give a body type for every named "let:".
>
> Similarly, why require return types for functions defined with "define:"?
> I'd almost rather write lambdas than give another annotation. (Not that I
> use define: very much.)
In general, `define:' and `let:' require return types since they
define (potentially) recursive functions, and therefore a type needs
to be given to the function, which wouldn't be known without
typechecking the body, which could reference the function. This is
also why `for/list:' needs a return type annotation - it's expanding
into a `let loop' underneath.
> - Related: can we get a runtime cast/refine macro? Occurrence typing makes
> a naive one easy to implement: (let ([x <expr>]) (if (pred? x) x (error
> ...))). Easy implementation means everyone will duplicate it; might as well
> incorporate a good one.
See `assert' in the docs.
> - Polymorphic structs being proper subtypes of their parent structs would
> be really nice. As it is, I can't figure out how to cleanly have a
> "(vector-array T)" subtype of "(array T)" that gives private array functions
> access to the vector backing an array. If I had that, I could collapse
> compositions of certain array ops at runtime and remove some duplicate
> bounds checks.
I'm not sure exactly what you mean here. Can you give an example?
> - Futures don't work with TR. I had to use require/typed to get them, so I
> gather that they're not officially supported. From what I can tell, for TR
> code, the JIT gives a large max_let_depth to even simple thunks like (lambda
> () 1). It's a shame, because splitting up forall loops with bodies that use
> nothing but float ops seems like a killer app for futures.
I'll add type annotations for `future' and `touch'. (lambda () 1)
should be the same in TR as in regular Racket, so I'm surprised the
JIT sees them differently.
> - Pie-in-the-sky: notice that "<-flvectorn" above is really just a type
> annotation that the forall macro understands. It would be nice if
> compositional macros could get the types of their arguments - I could have
> forall map over any array-like thing without requiring a declaration of what
> it is.
>
> I understand why this is hard: the inferred types depend on expansion, and
> the expansion would depend on types. While tricky, it seems that finding a
> fixpoint w.r.t. the subtype relation could work. Most macros would iterate
> zero times or once. Expanding to expressions with uncomparable types would
> be an error.
>
> Typeclasses allow function dispatch on the types of arguments; this would
> allow a sort of macro dispatch on the types of expanded inner syntax. You
> could probably define typeclasses in terms of it.
>
> Don't attack it too fiercely, though, as I haven't given it much deep
> thought. :) Also, it is a pie... in the sky.
Yes, other people have wanted this as well. It isn't at all obvious
how to do this in TR current architecture, but I'll keep thinking.
For the particular `<-flvector' case, right now the optimizer makes
this:
(for ([i some-vector]) ...)
just as fast as this:
(for ([i (in-vector some-vector)]) ...)
so perhaps the same can be done for `in-flvector' and other such operations.
Thanks again for the feedback.
--
sam th
sa...@ccs.neu.edu
Will M. Farr
> Is this the same as the (brand-new) `for/flvector' and `in-flvector'?
At the moment, these do not use the unsafe-... variants (though I can eventually change them to do so). Is Typed-Scheme smart enough to change them over even if I don't specify when somebody provides the correct flags?
Will
Sam Tobin-Hochstadt
> On Mon, Aug 23, 2010 at 9:57 AM, Will M. Farr <wmf...@gmail.com> wrote:
>> On Aug 23, 2010, at 6:52 AM, Sam Tobin-Hochstadt wrote:
>>
>>> Is this the same as the (brand-new) `for/flvector' and `in-flvector'?
>>
>> At the moment, these do not use the unsafe-... variants (though I can eventually change them to do so). Is Typed-Scheme smart enough to change them over even if I don't specify when somebody provides the correct flags?
>
No, sorry, that's not right. Some operations will be made unsafe, but
vector indexing won't be, since TR can't prove the absence of bounds
errors.
--
sam th
sa...@ccs.neu.edu
Sam Tobin-Hochstadt
>
>> Is this the same as the (brand-new) `for/flvector' and `in-flvector'?
>
> At the moment, these do not use the unsafe-... variants (though I can eventually change them to do so). Is Typed-Scheme smart enough to change them over even if I don't specify when somebody provides the correct flags?
Yes, it should be.
--
sam th
sa...@ccs.neu.edu
Matthias Felleisen
On Aug 23, 2010, at 12:31 AM, Neil Toronto wrote:
> This email is feedback on using Typed Racket to develop a new library (i.e. it isn't originally untyped code) that's about 3500 lines long, and some questions.
For the sake of enhancing Sam's research, it would have bee neat if you had written it all in Untyped first and ported it later. But I can see why you'd want to just get it to work. -- Matthias
Vincent St-Amour
Neil Toronto wrote:
> Vincent will be happy to know that all the flonum and fixnum ops are
> changed by TR's optimizer to be unsafe. (Except a certain add1 that TR
> can't prove doesn't overflow; I can prove it, so I changed it
> myself.)
I am indeed happy. I'm pleasantly surprised about the fixnum part,
since we can only optimize these in limited circumstances.
Was simply adding types enough to trigger all these optimizations, or
did you need to do a bit of extra work (except for that add1 case)?
> From my admittedly limited tests, I'd say that this particular forall
> gets within spitting distance of equivalent C code. ("Spitting distance"
> is a technical term meaning "within 3x to 5x time elapsed".) There's a
> "foralln!:" that destructively updates arrays, which might get a little
> closer; perhaps it gets within pinching distance of the C equivalent's
> buttocks.
That's impressive! If you get around to do precise measurements, I'm
really interested in the results.
> - Indentation is in a rather evil state in TR. Could DrRacket have
> more than one regexp for each "*-like keyword"? That would make it
> easier to auto-indent TR's built-in loop syntax, or any other syntax
> (like forall) that is in a state of flux. The indentation rules for
> for/*: loops could be tricky because of the required "return" type - but
> see the next item.
That would indeed be nice. I'll see what I can do.
> - Why require "return" or body types for for/*: loops in TR? I haven't
> needed them in forall/*: loops. Also, writing the "Listof" in "for/list:
> : (Listof T)" is annoying. I know it's a list from reading "for/list:",
> and for/list: knows it, too. I also know the return type of a
> "for/fold:" from the accumulators' types; why require them twice? I'm
> also annoyed by having to give a body type for every named "let:".
As Sam answered, we need at least some type information because the
expanded versions of the for: macros need it to typecheck.
However, you're right that the return type of a for/list: will always
be a list, making the Listof redundant. This is even more true of
for/fold:, and it annoys me too. In the case of for/fold:, it
shouldn't be a problem since the types of the accumulators tell us all
we need. I'll look into that.
But, in the case of for/list:, for/vector: and others, we would still
need an annotation to know the type of the elements of the resulting
list, vector, etc. We could remove the Listof, Vectorof and co from
the annotation, but that could lead to some ambiguity while reading
code.
For example, assuming we get annotate only the type of the elements of
the result sequence:
(for/list: : (Listof Integer) ...)
At first glance, what does this return? A list of integers, or a list
of lists of integers? It may be confusing.
> - I've found it useful to have a macro shaped like (with-refine* ([x
> pred?] ...) body ...). I have a lot of functions that take Integer and
> (Listof Integer) arguments, but actually operate only on
> Nonnegative-Fixnum indexes. (Nonnegativity and fixnum-ness are hard for
> TR to prove.) The function bodies are wrapped with this macro.
Having an assert* macro that would do something like that would be
useful to have in the core. Could you send me your with-refine* macro
so that I can include it in TR?
Vincent
Neil Toronto
> On Mon, Aug 23, 2010 at 12:31 AM, Neil Toronto <neil.t...@gmail.com> wrote:
>
>> This email is feedback on using Typed Racket to develop a new library (i.e.
>> it isn't originally untyped code) that's about 3500 lines long, and some
>> questions.
>
> Thanks for the feedback!
You're very welcome. BTW, it's actually only 1100 lines of code. There
was a mredit recovery file (I think that's what they are) in the
directory when I counted earlier, messing up the total.
>> (foralln/flvectorn:
>> ([x : Float (<-flvectorn xs)]
>> [y : Float (<-flvectorn ys)])
>> (for/fold: : Float ([dm : Float 0.0]) ([pt : vec2 (in-list pts)])
>> (+ dm (delta-mass-from pt (vec2 x y))))))
>>
>> Here, "flvectorn" is an N-dimensional flvector, and "<-flvectorn" is special
>> syntax like "in-list" (i.e. forall recognizes it as creating an array backed
>> by an flvectorn and inlines unsafe-flvectorn-ref accordingly).
>
> Is this the same as the (brand-new) `for/flvector' and `in-flvector'?
It works similarly, but it's not the same. Those use the sequence
abstraction; this uses a multidimensional random-access abstraction
called "arrayn". Also, "forall" and "foralln" semantics are meant to be
concurrent, so in principle they can always parallelize the work.
Further, arrays are read/write when their backing models are read/write
(e.g. vectors).
At first I tried to use the sequence abstraction. But Sequenceof is a
polymorphic type, so I couldn't get require/typed to import in-vector et
al. I don't want to use sequences now, though. Arrays should be
read/write. Destructive update can be useful in interactive programs
like games. Avoiding allocation reduces GC collects, which reduces
stutters and hitches.
> In general, `define:' and `let:' require return types since they
> define (potentially) recursive functions, and therefore a type needs
> to be given to the function, which wouldn't be known without
> typechecking the body, which could reference the function. This is
> also why `for/list:' needs a return type annotation - it's expanding
> into a `let loop' underneath.
Ahhh, okay. My loops destructively update a newly allocated vector (or
other array model) and iterate over one or more Nonnegative-Fixnum
indexes. The loops they expand to always have type Nonnegative-Fixnum or
similar.
It seems the macro system's ignorance of the type system is making
things difficult. I'm guessing this kind of thing will come up
frequently in TR programs, and in just a few different ways. It might be
helpful to catalog them.
>> - Polymorphic structs being proper subtypes of their parent structs would
>> be really nice. As it is, I can't figure out how to cleanly have a
>> "(vector-array T)" subtype of "(array T)" that gives private array functions
>> access to the vector backing an array. If I had that, I could collapse
>> compositions of certain array ops at runtime and remove some duplicate
>> bounds checks.
>
> I'm not sure exactly what you mean here. Can you give an example?
Yep. Here's the array type:
(define-type Index Nonnegative-Fixnum)
(define-struct: (T) array ([length : Index]
[unsafe-ref : (Index -> T)]
[unsafe-set! : (Index T -> Void)]))
(I'm not using struct: because I'm still on a build where it has
problems with struct-out.) Here's an operation that could be sped up for
vector-backed arrays. It's a lazy version of map for arrays:
(: array-map (All (A B) ((A -> B) (array A) -> (array B))))
(define (array-map f arr)
(define unsafe-ref (array-unsafe-ref arr))
(array (array-length arr)
(lambda: ([i : Index]) (f (unsafe-ref i)))
(lambda: ([i : Index] [v : B]) (error ...))))
The opportunity is in (f (unsafe-ref i)). When arr is backed by a
vector, unsafe-ref is a closure (over the vector) that just does an
unsafe-vector*-ref. If array-map knew that, it could return an array
with an unsafe-ref that does an unsafe-vector*-ref itself instead of
deferring to arr's unsafe-ref. But this:
(define-struct: (T) (vector-array array) ([vec : (Vectorof T)]))
has a predicate with type (Any -> Boolean : (vector-array Any)), so this
attempt at a faster unsafe-ref won't typecheck:
(if (vector-array? arr)
(let ([vec (vector-array-vec arr)])
(lambda: ([i : Index]) (f (unsafe-vector*-ref vec i))))
(let ([unsafe-ref (array-unsafe-ref arr)])
(lambda: ([i : Index]) (f (unsafe-ref i)))))
In the true branch, vec has type (Vectorof Any), so the lambda has the
wrong type.
There are examples involving bounds checks and other things more
expensive than just extra applications, but they're more complicated. If
there's an efficient workaround for now, I'd love to know what it is.
> I'll add type annotations for `future' and `touch'. (lambda () 1)
> should be the same in TR as in regular Racket, so I'm surprised the
> JIT sees them differently.
So was I. Thanks!
>> - Pie-in-the-sky: notice that "<-flvectorn" above is really just a type
>> annotation that the forall macro understands. It would be nice if
>> compositional macros could get the types of their arguments - I could have
>> forall map over any array-like thing without requiring a declaration of what
>> it is.
>>
>> *snip*
>
> For the particular `<-flvector' case, right now the optimizer makes
> this:
>
> (for ([i some-vector]) ...)
>
> just as fast as this:
>
> (for ([i (in-vector some-vector)]) ...)
>
> so perhaps the same can be done for `in-flvector' and other such operations.
Neet. I'll look at the latest optimizer and see what I can learn from it.
Thanks!
Neil T
Sam Tobin-Hochstadt
> Sam Tobin-Hochstadt wrote:
>> In general, `define:' and `let:' require return types since they
>> define (potentially) recursive functions, and therefore a type needs
>> to be given to the function, which wouldn't be known without
>> typechecking the body, which could reference the function. This is
>> also why `for/list:' needs a return type annotation - it's expanding
>> into a `let loop' underneath.
>
> Ahhh, okay. My loops destructively update a newly allocated vector (or other
> array model) and iterate over one or more Nonnegative-Fixnum indexes. The
> loops they expand to always have type Nonnegative-Fixnum or similar.
In that case, you can probably insert the annotation yourself in a
macro, if it's generated (such as with your `forall' macros). In
other cases, I don't have much help to offer.
>>> - Polymorphic structs being proper subtypes of their parent structs
>>> would
>>> be really nice. As it is, I can't figure out how to cleanly have a
>>> "(vector-array T)" subtype of "(array T)" that gives private array
>>> functions
>>> access to the vector backing an array. If I had that, I could collapse
>>> compositions of certain array ops at runtime and remove some duplicate
>>> bounds checks.
>>
>> I'm not sure exactly what you mean here. Can you give an example?
>
> Yep. Here's the array type:
[helpful example elided]
Hmm. I see why this doesn't work currently. A workaround would be to
use unions rather than struct subtyping, here, but I'll try to make
this work. If you could submit a bug report, that would help.
--
sam th
sa...@ccs.neu.edu
Neil Toronto
> At Sun, 22 Aug 2010 21:31:09 -0700,
> Neil Toronto wrote:
>> Vincent will be happy to know that all the flonum and fixnum ops are
>> changed by TR's optimizer to be unsafe. (Except a certain add1 that TR
>> can't prove doesn't overflow; I can prove it, so I changed it
>> myself.)
>
> I am indeed happy. I'm pleasantly surprised about the fixnum part,
> since we can only optimize these in limited circumstances.
With the fixnums, it's mostly comparisons that are made unsafe. What I'm
most pleased with is the fact that things like vector-length get changed
to unsafe-vector-length, and that they return Nonnegative-Fixnums like
they should. It seems every typed function I've used has the most
liberal argument types and constrained return types they could have been
given. Because of that, it's been quite easy to ensure that indexes
remain fixnums, and that flonum ops return flonums.
It's fun to open the macro stepper and see "unsafe" scattered
everywhere, in all the places I expect it. Pretty much every time it's
not there is when I expect TR to be able to prove something it can't prove.
> Was simply adding types enough to trigger all these optimizations, or
> did you need to do a bit of extra work (except for that add1 case)?
Here's the list of extra work in the array library itself:
- Abandon special handling of vector-backed arrays, which used
polymorphic struct sub-types, in favor of loop syntax (Sam is looking
into polymorphic struct sub-types)
- Change (add1 i) into (unsafe-fx+ 1 i), prove it's safe
- Handle type syntax in macros (no big deal)
- Add extra checks to ensure that lexical indexes are fixnums in
multidimensional arrays (e.g. ds : (Listof Fixnum) is only a valid array
shape if (apply * ds) is a fixnum)
- Replace match-define with multiple defines
For the last, IIRC, on my version of Racket, match-define calls a
predicate to ensure the right struct type, but it's redundant in TR.
Every little bit counts when it's in a tight loop. (FWIW, I like seeing
all the unsafe struct refs as well.) I also recall TR reporting internal
errors a few times when I used match or match-define, but I didn't file
a bug report. I will next time.
I had to do the following in my tests and test app:
- Use flsqrt, flfloor, flceiling instead of non-fl* versions
- Use (* x x) instead of (sqr x)
- Change literal numbers to literal floats (e.g. 1.0 instead of 1)
> However, you're right that the return type of a for/list: will always
> be a list, making the Listof redundant. This is even more true of
> for/fold:, and it annoys me too. In the case of for/fold:, it
> shouldn't be a problem since the types of the accumulators tell us all
> we need. I'll look into that.
Excellent, thanks.
>> - I've found it useful to have a macro shaped like (with-refine* ([x
>> pred?] ...) body ...). I have a lot of functions that take Integer and
>> (Listof Integer) arguments, but actually operate only on
>> Nonnegative-Fixnum indexes. (Nonnegativity and fixnum-ness are hard for
>> TR to prove.) The function bodies are wrapped with this macro.
>
> Having an assert* macro that would do something like that would be
> useful to have in the core. Could you send me your with-refine* macro
> so that I can include it in TR?
You'll want to rename it to with-asserts*, I suppose. I think if I were
to spend more time on it, I'd make the type-name part optional, and in
those cases use pred?'s syntax as a string as the second argument to
raise-type-error.
Or maybe just leave it. Type errors should be friendly, yes? :)
#lang typed/racket
(require (for-syntax syntax/parse))
(define-syntax (with-refine* stx)
(syntax-parse stx
[(_ ([x:id pred? type-name] ...) body:expr ...+)
(syntax/loc stx
(cond [(not (pred? x))
(raise-type-error 'with-refine* type-name x)]
...
[else (let () body ...)]))]))
(: fixnum-id (Number -> Fixnum))
(define (fixnum-id x)
(with-refine* ([x fixnum? "Fixnum"])
x))
(fixnum-id 1)
;; 1
(fixnum-id 0.0)
;; with-refine*: expected argument of type <Fixnum>; given 0.0
It would be nice if assert were capable of this. To do that, though, I
think the type checker would have to treat the expression after the "if"
in this case:
(begin (if (pred? x)
<something useful>
(error ...))
<some other useful thing...>)
as part of the "then" branch. (And as part of the "else" branch when the
error is in the "then".)
Neil T
Sam Tobin-Hochstadt
>
> It would be nice if assert were capable of this. To do that, though, I think
> the type checker would have to treat the expression after the "if" in this
> case:
>
> (begin (if (pred? x)
> <something useful>
> (error ...))
> <some other useful thing...>)
>
> as part of the "then" branch. (And as part of the "else" branch when the
> error is in the "then".)
This is something I've wanted for a while. It comes up a lot in code like this:
(unless (foo? x) (error 'bad-input))
(foo-fun x)
It requires some involved-but-I-hope-straightforward to the machinery
of occurrence typing, but it's something I plan to add eventually.
--
sam th
sa...@ccs.neu.edu
Neil Toronto
> On Mon, Aug 23, 2010 at 6:12 PM, Neil Toronto <neil.t...@gmail.com> wrote:
>> Sam Tobin-Hochstadt wrote:
>> Yep. Here's the array type:
>
> [helpful example elided]
>
> Hmm. I see why this doesn't work currently. A workaround would be to
> use unions rather than struct subtyping, here, but I'll try to make
> this work. If you could submit a bug report, that would help.
Cool. Bug 11099 is close, but is really about subtypes with (Vectorof T)
fields specifically. I've made 11122 for this.
Thanks!
Neil T
Noel Welsh
> It works similarly, but it's not the same. Those use the sequence
> abstraction; this uses a multidimensional random-access abstraction called
> "arrayn". Also, "forall" and "foralln" semantics are meant to be concurrent,
> so in principle they can always parallelize the work. Further, arrays are
> read/write when their backing models are read/write (e.g. vectors).
This is great stuff. If you're not familiar with Single Assignment C
take a look at it. It's the only modern functional language I know
that takes arrays seriously. It has an interesting array comprehension
system.
> At first I tried to use the sequence abstraction. But Sequenceof is a
> polymorphic type, so I couldn't get require/typed to import in-vector et al.
> I don't want to use sequences now, though. Arrays should be read/write.
> Destructive update can be useful in interactive programs like games.
> Avoiding allocation reduces GC collects, which reduces stutters and hitches.
The example you gave is something that could be written with
for/vector. One could equally implement for/vector! that mutates an
existing vector. It is really when you move to higher dimensions that
for/* variants have problems, as the order you construct the matrix
becomes difficult to express.
N.
Neil Toronto
> On Aug 23, 2010, at 12:31 AM, Neil Toronto wrote:
>
>> This email is feedback on using Typed Racket to develop a new library (i.e. it isn't originally untyped code) that's about 3500 lines long, and some questions.
>
> For the sake of enhancing Sam's research, it would have bee neat if you had written it all in Untyped first and ported it later. But I can see why you'd want to just get it to work. -- Matthias
>
I hope it can be useful anyway. In my early move to Typed Racket, there
were a few things I had to do besides annotate, which I put in my reply
to Vincent. There's that, at least.
The more of Racket that's made available in Typed Racket, the more we'll
see things written specifically for Typed Racket. Most of a TR library
or API can be made available to Racket as-is - the functions,
specifically. The macros can be tricky, especially those that bind
variables and inline things, like forall does. I plan to attempt it and
do another reaction/question email about that.
Although TR is made for annotating and checking untyped Racket code, it
seems to encourage a slightly different problem-solving or coding style.
I can't really explain it right now, as my impressions are colored by
programming for runtime efficiency, which I've never done in Racket before.
Neil T
Vincent St-Amour
Neil Toronto wrote:
> It's fun to open the macro stepper and see "unsafe" scattered
> everywhere, in all the places I expect it. Pretty much every time it's
> not there is when I expect TR to be able to prove something it can't prove.
Do you have examples besides fixnum operations?
> - Change (add1 i) into (unsafe-fx+ 1 i), prove it's safe
We're looking into adding a OneLessThanMaxFixnum type that, when used
as argument to add1 gives a return type of Fixnum. That would solve
this problem.
> - Replace match-define with multiple defines
>
> For the last, IIRC, on my version of Racket, match-define calls a
> predicate to ensure the right struct type, but it's redundant in TR.
Removing predicates made redundant by typechecking in the general case
is on my todo list.
> I had to do the following in my tests and test app:
>
> - Use flsqrt, flfloor, flceiling instead of non-fl* versions
sqrt can indeed return a complex number, but if you pass it a
Nonnegative-Float, the result should be a Nonnegative-Float. As for
floor and ceiling, they should already preserve flonum-ness, and as
such should be optimized. Can you send me an example where these could
not be optimized?
> - Use (* x x) instead of (sqr x)
sqr should give you the right types. However, its type does not
currently express its full behavior wrt the sign of the result. I'll
fix that.
> You'll want to rename it to with-asserts*, I suppose. I think if I were
> to spend more time on it, I'd make the type-name part optional, and in
> those cases use pred?'s syntax as a string as the second argument to
> raise-type-error.
Thanks, I'll add that. We're also thinking of having assert (and thus
with-asserts*) take types as arguments, instead of just predicates.
Vincent