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

From: Neil Van Dyke (neil at neilvandyke.org)
Date: Wed Dec 22 14:50:17 EST 2010

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/


Posted on the users mailing list.