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 <[email protected]> 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/ _________________________________________________ For list-related administrative tasks: http://lists.racket-lang.org/listinfo/users
