[racket] typed/racket: type of sequence-filter

From: Tim Brown (tim.brown at cityc.co.uk)
Date: Fri Apr 11 09:17:24 EDT 2014

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.

Posted on the users mailing list.