[racket] typed/racket: type of sequence-filter
Folks,
I am trying to use typed/racket to generate a sequence of primes
(actually, it's a sequence of a special class of prime, but primes will
do).
(: natural->odd-prime (Natural -> Natural))
(define (natural->odd-prime x) (+ 1 (* x 2)))
(: odd-primes (Sequenceof Natural))
(define odd-primes (sequence-map natural->odd-prime (in-naturals 1)))
(: prime-sequence (Sequenceof Natural))
(define prime-sequence (sequence-filter prime? odd-primes))
^^^^^^^^^^^^^^^
Type checker error here
The error is:
Type Checker: Polymorphic function `sequence-filter' could not be
applied t...nteger) Expected result: (Sequenceof Nonnegative-Integer)
in: (sequence-filter prime? odd-primes)
#(903 35)
A :print-types of sequence-filter shows:
> (:print-type sequence-filter)
(All (a b)
(case->
(-> (-> a Any) (Sequenceof a) (Sequenceof b))
(-> (-> a Any) (Listof a) (Sequenceof a))))
Should the type of sequence-filter not be "(a -> Any) (Sequenceof a) ->
(Sequenceof a)" since the type (and data) of the successful elements of
the sequence are identical.
Is there any reason for this particular type declaration of
sequence-filter?
I've just forked a copy of the racket repository, and changed the type of
sequence-filter (in
./pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-env.rkt)
to:
[sequence-filter
(-poly (a b)
(cl->*
((asym-pred a Univ (-FS (-filter b 0) -top))
(-seq a)
. -> .
(-seq a))
((a . -> . Univ) (-lst a) . -> . (-seq a))))]
This gives a similar error; but changing the type to:
[sequence-filter
(-poly (a b)
(cl->*
((a . -> . Univ)
(-seq a)
. -> .
(-seq a))
((a . -> . Univ) (-lst a) . -> . (-seq a))))]
Giving a :print-type of:
(All (a b)
(case->
(-> (-> a Any) (Sequenceof a) (Sequenceof a))
(-> (-> a Any) (Listof a) (Sequenceof a))))
Lets it behave correctly. Unfortunately, I don't comprehend the description
of the (asym-pred ...) clause, what it does and how it breaks my typing. So
could someone look at what's happening here?
Tim
FYI: "Welcome to DrRacket, version 6.0 [3m]."
--
Tim Brown <tim.brown at cityc.co.uk> | City Computing Limited |
T: +44 20 8770 2110 | City House, Sutton Park Road |
F: +44 20 8770 2130 | Sutton, Surrey, SM1 2AE, GB |
-----------------------------------------------------------------------|
BEAUTY: What's in your eye when you have a bee in your hand |
-----------------------------------------------------------------------'
City Computing Limited registered in London No. 1767817.
Registered Office: City House, Sutton Park Road, Sutton, Surrey, SM1 2AE
VAT number 372 8290 34.