[racket] confusion on Typed Racket, pairs, and lists

This works for me:

> (ann (cons 'a (ann (cons 'b '()) (List Symbol))) (List Symbol Symbol))
- : (List Symbol Symbol)
'(a b)

As does this:

> (: pair (All [X Y] (X Y -> (Pairof X Y))))
> (define pair cons)
> (pair 'a (pair 'b '()))
- : (List 'a 'b)
'(a b)
> (ann (pair 'a (pair 'b '())) (List Symbol Symbol))
- : (List Symbol Symbol)
'(a b)

The trick is that the type of cons is:

> cons
- : (All (a b) (case-lambda (a (Listof a) -> (Listof a)) (a b -> (Pairof a b))))
#<procedure:cons>

Notice that the Listof clause comes first, so whenever cons can
produce a Listof type, it will.  So each time you apply cons, if you
don't want a Listof type you have to "convince" it to build something
else.  Do this by either annotating each step, or binding cons with a
simpler type.

(This all worked in 5.0.2, but I don't recall any changes between
5.0.1 and 5.0.2 that would affect this.)

Carl Eastlund

On Wed, Dec 22, 2010 at 2:50 PM, Neil Van Dyke <neil at neilvandyke.org> wrote:
> Any guidance on how to deal with constructing objects of list types using
> "cons" in Typed Scheme?
>
> Here is an illustration of one of the difficulties I'm having: trying to
> produce a "(List Symbol Symbol)" using "cons"...
>
> 1. Use "cons" to produces a list of one element, annotated as different list
> types:
>
>> (cons 'a '())
> - : (Listof 'a)
> (a)
>> (ann (cons 'a '()) (List 'a))
> - : (List 'a)
> (a)
>> (ann (cons 'a '()) (List Symbol))
> - : (List Symbol)
> (a)
>
> 2. Using "cons" to produce a list of two different objects of the same type
> also produces a "Listof":
>
>> (cons 'b (cons 'a '()))
> - : (Listof (U 'a 'b))
> (b a)
>
> 3. Unfortunately, that produced "(Listof (U 'a 'b))" cannot be a "(List
> Symbol Symbol)":
>
>> (ann (cons 'b (cons 'a '())) (List Symbol Symbol))
> . . Type Checker: Polymorphic function cons could not be applied to
> arguments:
> Types: a (Listof a) -> (Listof a)
>      a b -> (Pairof a b)
> Arguments: 'b (Listof 'a)
> Expected result: (List Symbol Symbol)
> in: (cons (quote b) (cons (quote a) (quote ())))
>
> 4. But we *can* avoid the "(Listof (U 'a 'b)" by making it a "(List Symbol)"
> or "(Listof Symbol)":
>
>> (cons 'b (ann (cons 'a '()) (List Symbol)))
> - : (Listof Symbol)
> (b a)
>
> 5. With that "(Listof Symbol)", we can then make it our intended "(List
> Symbol Symbol)":
>
>> (ann (cons 'b (ann (cons 'a '()) (List Symbol))) (List Symbol Symbol))
> - : (List Symbol Symbol)
> (b a)
>
> 6. In this particular case, it seems that the system isn't able to make the
> leap from "(Listof (U 'a 'b))" to "(List Symbol Symbol)" for the "cons"
> expression, even though we can make it a "(Listof Symbol)":
>
>> (ann (cons 'b (cons 'a '())) (Listof Symbol))
> - : (Listof Symbol)
> (b a)
>> (ann (ann (cons 'b (cons 'a '())) (Listof Symbol)) (List Symbol Symbol))
> . . Type Checker: Polymorphic function cons could not be applied to
> arguments:
> Types: a (Listof a) -> (Listof a)
>      a b -> (Pairof a b)
> Arguments: 'b (Listof 'a)
> Expected result: (List Symbol Symbol)
> in: (cons (quote b) (cons (quote a) (quote ())))
>
> 7. Other "(Listof Symbol)" *can* be make a "(List Symbol Symbol)", or at
> least doesn't give an error like above does:
>
>> (list 'a 'b)
> - : (List 'a 'b)
> (a b)
>> (ann (list 'a 'b) (Listof Symbol))
> - : (Listof Symbol)
> (a b)
>> (ann (ann (list 'a 'b) (Listof Symbol)) (List Symbol Symbol))
> - : (Listof Symbol)
> (a b)
>
> Perhaps I'm not thinking about this in the intended way?
>
> (This is with Racket 5.0.1, if it matters.  I am building 5.0.2 right now.)
>
> --
> http://www.neilvandyke.org/