[racket-dev] Should I expect this program to typecheck?
#lang typed/racket (: vector-first (All (A B) ((U (Vectorof A) (Vectorof B)) - (U A B (define (vector-first vs) (vector-ref vs 0)) I can't think of a reason this shouldn't work, but I may not be taxing my imagination enough to come up with one. Neil ⊥ _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] Should I expect this program to typecheck?
How do you determine the difference between the two vector types is the question... -Ian - Original Message - From: Neil Toronto neil.toro...@gmail.com To: dev@racket-lang.org dev@racket-lang.org Sent: Monday, August 6, 2012 4:12:53 PM GMT -05:00 US/Canada Eastern Subject: [racket-dev] Should I expect this program to typecheck? #lang typed/racket (: vector-first (All (A B) ((U (Vectorof A) (Vectorof B)) - (U A B (define (vector-first vs) (vector-ref vs 0)) I can't think of a reason this shouldn't work, but I may not be taxing my imagination enough to come up with one. Neil ⊥ _ Racket Developers list: http://lists.racket-lang.org/dev _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] Should I expect this program to typecheck?
I can't distinguish the elements' types in the simplified example I
gave. The code I'm actually working on is this:
(: check-array-indexes (Symbol (Vectorof Index)
(U (Vectorof Index) (Vectorof Integer))
- (Vectorof Index)))
(define (check-array-indexes name ds js)
(define (raise-index-error)
(error name expected indexes for shape ~e; given ~e ds js))
(define dims (vector-length ds))
(unless (= dims (vector-length js)) (raise-index-error))
(define: new-js : (Vectorof Index) (make-vector dims 0))
(let loop ([#{i : Nonnegative-Fixnum} 0])
(cond [(i . . dims)
(define di (vector-ref ds i))
(define ji (vector-ref js i))
(cond [(and (0 . = . ji) (ji . . di))
(vector-set! new-js i ji)
(loop (+ i 1))]
[else (raise-index-error)])]
[else new-js])))
I get type errors on every expression involving `ji', because TR has
determined that it has type `Any'.
I would use a `case-' type, but I have an array transformation function
that receives an argument with type
((Vectorof Index) - (U (Vectorof Integer) (Vectorof Index)))
whose output has to be bounds-checked by `check-array-indexes', and I
can't apply a function with a case type to an argument with a union type.
The question will of course be moot when TR has something like a `Const'
type constructor. I'm anticipating that, and changing the user-facing
array API to receive (U (Vectorof Integer) (Vectorof Index)) for array
indexes instead of (Listof Integer). (It should eventually be (Const
(Vectorof Integer)) or similar, which should be covariant.)
So are the type errors an error in TR, or a known limitation?
Neil ⊥
On 08/06/2012 02:25 PM, J. Ian Johnson wrote:
How do you determine the difference between the two vector types is the
question...
-Ian
- Original Message -
From: Neil Toronto neil.toro...@gmail.com
To: dev@racket-lang.org dev@racket-lang.org
Sent: Monday, August 6, 2012 4:12:53 PM GMT -05:00 US/Canada Eastern
Subject: [racket-dev] Should I expect this program to typecheck?
#lang typed/racket
(: vector-first (All (A B) ((U (Vectorof A) (Vectorof B)) - (U A B
(define (vector-first vs)
(vector-ref vs 0))
I can't think of a reason this shouldn't work, but I may not be taxing
my imagination enough to come up with one.
Neil ⊥
_
Racket Developers list:
http://lists.racket-lang.org/dev
_
Racket Developers list:
http://lists.racket-lang.org/dev
Re: [racket-dev] Should I expect this program to typecheck?
I don't get the type Any, rather it doesn't know how to go from the union of
vectors to a (vector a) for some a. Vector ref expects a vector, not a union of
vectors, and because vectors are invariant, it cannot simplify this to (vector
Integer).
-Ian
- Original Message -
From: Neil Toronto neil.toro...@gmail.com
To: J. Ian Johnson i...@ccs.neu.edu
Cc: dev dev@racket-lang.org
Sent: Monday, August 6, 2012 5:07:38 PM GMT -05:00 US/Canada Eastern
Subject: Re: [racket-dev] Should I expect this program to typecheck?
I can't distinguish the elements' types in the simplified example I
gave. The code I'm actually working on is this:
(: check-array-indexes (Symbol (Vectorof Index)
(U (Vectorof Index) (Vectorof Integer))
- (Vectorof Index)))
(define (check-array-indexes name ds js)
(define (raise-index-error)
(error name expected indexes for shape ~e; given ~e ds js))
(define dims (vector-length ds))
(unless (= dims (vector-length js)) (raise-index-error))
(define: new-js : (Vectorof Index) (make-vector dims 0))
(let loop ([#{i : Nonnegative-Fixnum} 0])
(cond [(i . . dims)
(define di (vector-ref ds i))
(define ji (vector-ref js i))
(cond [(and (0 . = . ji) (ji . . di))
(vector-set! new-js i ji)
(loop (+ i 1))]
[else (raise-index-error)])]
[else new-js])))
I get type errors on every expression involving `ji', because TR has
determined that it has type `Any'.
I would use a `case-' type, but I have an array transformation function
that receives an argument with type
((Vectorof Index) - (U (Vectorof Integer) (Vectorof Index)))
whose output has to be bounds-checked by `check-array-indexes', and I
can't apply a function with a case type to an argument with a union type.
The question will of course be moot when TR has something like a `Const'
type constructor. I'm anticipating that, and changing the user-facing
array API to receive (U (Vectorof Integer) (Vectorof Index)) for array
indexes instead of (Listof Integer). (It should eventually be (Const
(Vectorof Integer)) or similar, which should be covariant.)
So are the type errors an error in TR, or a known limitation?
Neil ⊥
On 08/06/2012 02:25 PM, J. Ian Johnson wrote:
How do you determine the difference between the two vector types is the
question...
-Ian
- Original Message -
From: Neil Toronto neil.toro...@gmail.com
To: dev@racket-lang.org dev@racket-lang.org
Sent: Monday, August 6, 2012 4:12:53 PM GMT -05:00 US/Canada Eastern
Subject: [racket-dev] Should I expect this program to typecheck?
#lang typed/racket
(: vector-first (All (A B) ((U (Vectorof A) (Vectorof B)) - (U A B
(define (vector-first vs)
(vector-ref vs 0))
I can't think of a reason this shouldn't work, but I may not be taxing
my imagination enough to come up with one.
Neil ⊥
_
Racket Developers list:
http://lists.racket-lang.org/dev
_
Racket Developers list:
http://lists.racket-lang.org/dev
Re: [racket-dev] Should I expect this program to typecheck?
This type checks. Not sure if it is the same thing as the original
however.
(: check-array-indexes (Symbol
(Vectorof Index)
(U (Vectorof Index) (Vectorof Integer))
- (Vectorof Index)))
(define (check-array-indexes name ds js)
(define (raise-index-error)
(error name expected indexes for shape ~e; given ~e ds js))
(: dims Integer)
(define dims (vector-length ds))
(unless (= dims (vector-length js)) (raise-index-error))
(: new-js (Vectorof Index))
(define new-js (make-vector dims 0))
(let: loop : (Vectorof Index) ([i : Integer 0])
(if ( i dims)
(let: ((di : Index (vector-ref ds i))
(ji : Integer (assert (vector-ref js i) exact-integer?)))
(if (and (= 0 ji)
( ji di))
(begin
(vector-set! new-js i (assert ji index?))
(loop (add1 i)))
(raise-index-error)))
new-js)))
On Mon, Aug 6, 2012 at 5:47 PM, J. Ian Johnson i...@ccs.neu.edu wrote:
I don't get the type Any, rather it doesn't know how to go from the union
of vectors to a (vector a) for some a. Vector ref expects a vector, not a
union of vectors, and because vectors are invariant, it cannot simplify
this to (vector Integer).
-Ian
- Original Message -
From: Neil Toronto neil.toro...@gmail.com
To: J. Ian Johnson i...@ccs.neu.edu
Cc: dev dev@racket-lang.org
Sent: Monday, August 6, 2012 5:07:38 PM GMT -05:00 US/Canada Eastern
Subject: Re: [racket-dev] Should I expect this program to typecheck?
I can't distinguish the elements' types in the simplified example I
gave. The code I'm actually working on is this:
(: check-array-indexes (Symbol (Vectorof Index)
(U (Vectorof Index) (Vectorof Integer))
- (Vectorof Index)))
(define (check-array-indexes name ds js)
(define (raise-index-error)
(error name expected indexes for shape ~e; given ~e ds js))
(define dims (vector-length ds))
(unless (= dims (vector-length js)) (raise-index-error))
(define: new-js : (Vectorof Index) (make-vector dims 0))
(let loop ([#{i : Nonnegative-Fixnum} 0])
(cond [(i . . dims)
(define di (vector-ref ds i))
(define ji (vector-ref js i))
(cond [(and (0 . = . ji) (ji . . di))
(vector-set! new-js i ji)
(loop (+ i 1))]
[else (raise-index-error)])]
[else new-js])))
I get type errors on every expression involving `ji', because TR has
determined that it has type `Any'.
I would use a `case-' type, but I have an array transformation function
that receives an argument with type
((Vectorof Index) - (U (Vectorof Integer) (Vectorof Index)))
whose output has to be bounds-checked by `check-array-indexes', and I
can't apply a function with a case type to an argument with a union type.
The question will of course be moot when TR has something like a `Const'
type constructor. I'm anticipating that, and changing the user-facing
array API to receive (U (Vectorof Integer) (Vectorof Index)) for array
indexes instead of (Listof Integer). (It should eventually be (Const
(Vectorof Integer)) or similar, which should be covariant.)
So are the type errors an error in TR, or a known limitation?
Neil ⊥
On 08/06/2012 02:25 PM, J. Ian Johnson wrote:
How do you determine the difference between the two vector types is the
question...
-Ian
- Original Message -
From: Neil Toronto neil.toro...@gmail.com
To: dev@racket-lang.org dev@racket-lang.org
Sent: Monday, August 6, 2012 4:12:53 PM GMT -05:00 US/Canada Eastern
Subject: [racket-dev] Should I expect this program to typecheck?
#lang typed/racket
(: vector-first (All (A B) ((U (Vectorof A) (Vectorof B)) - (U A B
(define (vector-first vs)
(vector-ref vs 0))
I can't think of a reason this shouldn't work, but I may not be taxing
my imagination enough to come up with one.
Neil ⊥
_
Racket Developers list:
http://lists.racket-lang.org/dev
_
Racket Developers list:
http://lists.racket-lang.org/dev
_
Racket Developers list:
http://lists.racket-lang.org/dev
Re: [racket-dev] Should I expect this program to typecheck?
#lang typed/racket
(: vector-first (All (A B) ((U (Vectorof A) (Vectorof B)) - (U A B
(define (vector-first vs)
(vector-ref vs 0))
I doubt this will typecheck without more work in the typechecker. The
issue is that it should work for a union type of as many vectors as
you want.
If there was a readable-vector type it would be trivial as subtyping
would do all of the real work. As (U (ReadVector A) (ReadVector B)) :
(ReadVector (U A B)). But that cannot be done with real vectors, as
they are invariant.
On Mon, Aug 6, 2012 at 5:15 PM, Ray Racine ray.rac...@gmail.com wrote:
This type checks. Not sure if it is the same thing as the original
however.
(: check-array-indexes (Symbol
(Vectorof Index)
(U (Vectorof Index) (Vectorof Integer))
- (Vectorof Index)))
(define (check-array-indexes name ds js)
(define (raise-index-error)
(error name expected indexes for shape ~e; given ~e ds js))
(: dims Integer)
(define dims (vector-length ds))
(unless (= dims (vector-length js)) (raise-index-error))
(: new-js (Vectorof Index))
(define new-js (make-vector dims 0))
(let: loop : (Vectorof Index) ([i : Integer 0])
(if ( i dims)
(let: ((di : Index (vector-ref ds i))
(ji : Integer (assert (vector-ref js i) exact-integer?)))
(if (and (= 0 ji)
( ji di))
(begin
(vector-set! new-js i (assert ji index?))
(loop (add1 i)))
(raise-index-error)))
new-js)))
On Mon, Aug 6, 2012 at 5:47 PM, J. Ian Johnson i...@ccs.neu.edu wrote:
I don't get the type Any, rather it doesn't know how to go from the union
of vectors to a (vector a) for some a. Vector ref expects a vector, not a
union of vectors, and because vectors are invariant, it cannot simplify this
to (vector Integer).
-Ian
- Original Message -
From: Neil Toronto neil.toro...@gmail.com
To: J. Ian Johnson i...@ccs.neu.edu
Cc: dev dev@racket-lang.org
Sent: Monday, August 6, 2012 5:07:38 PM GMT -05:00 US/Canada Eastern
Subject: Re: [racket-dev] Should I expect this program to typecheck?
I can't distinguish the elements' types in the simplified example I
gave. The code I'm actually working on is this:
(: check-array-indexes (Symbol (Vectorof Index)
(U (Vectorof Index) (Vectorof Integer))
- (Vectorof Index)))
(define (check-array-indexes name ds js)
(define (raise-index-error)
(error name expected indexes for shape ~e; given ~e ds js))
(define dims (vector-length ds))
(unless (= dims (vector-length js)) (raise-index-error))
(define: new-js : (Vectorof Index) (make-vector dims 0))
(let loop ([#{i : Nonnegative-Fixnum} 0])
(cond [(i . . dims)
(define di (vector-ref ds i))
(define ji (vector-ref js i))
(cond [(and (0 . = . ji) (ji . . di))
(vector-set! new-js i ji)
(loop (+ i 1))]
[else (raise-index-error)])]
[else new-js])))
I get type errors on every expression involving `ji', because TR has
determined that it has type `Any'.
I would use a `case-' type, but I have an array transformation function
that receives an argument with type
((Vectorof Index) - (U (Vectorof Integer) (Vectorof Index)))
whose output has to be bounds-checked by `check-array-indexes', and I
can't apply a function with a case type to an argument with a union type.
The question will of course be moot when TR has something like a `Const'
type constructor. I'm anticipating that, and changing the user-facing
array API to receive (U (Vectorof Integer) (Vectorof Index)) for array
indexes instead of (Listof Integer). (It should eventually be (Const
(Vectorof Integer)) or similar, which should be covariant.)
So are the type errors an error in TR, or a known limitation?
Neil ⊥
On 08/06/2012 02:25 PM, J. Ian Johnson wrote:
How do you determine the difference between the two vector types is the
question...
-Ian
- Original Message -
From: Neil Toronto neil.toro...@gmail.com
To: dev@racket-lang.org dev@racket-lang.org
Sent: Monday, August 6, 2012 4:12:53 PM GMT -05:00 US/Canada Eastern
Subject: [racket-dev] Should I expect this program to typecheck?
#lang typed/racket
(: vector-first (All (A B) ((U (Vectorof A) (Vectorof B)) - (U A B
(define (vector-first vs)
(vector-ref vs 0))
I can't think of a reason this shouldn't work, but I may not be taxing
my imagination enough to come up with one.
Neil ⊥
_
Racket Developers list:
http://lists.racket-lang.org/dev
_
Racket Developers list:
http://lists.racket-lang.org/dev
_
Racket Developers list:
http://lists.racket
