[racket] confusion on Typed Racket, pairs, and lists
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/