No it is not possible to type flatten. Consider having flatten with this type:
(define-type (Listof* A) (Rec T (U A (Listof T)))) (: flatten (All (A) ((Listof* A) -> (Listof A)))) And then applying it as such: ((inst flatten (Listof Number)) (list (list 1 2 3))) This would typecheck and return the value (list 1 2 3) with the type (Listof (Listof Number)). This is bad and breaks soundness. On Tue, Aug 7, 2012 at 9:57 AM, Neil Toronto <neil.toro...@gmail.com> wrote: > Short version: Creating arrays from nested lists (and vectors) would be a > lot easier if I could write a `flatten' function in TR, but I haven't been > able to. Is it possible? > > Long version: Given this type: > > (define-type (Listof* A) (Rec T (U A (Listof T)))) > > I'd like this function: > > (: flatten (All (A) ((Listof* A) -> (Listof A)))) > > When I use `require/typed' to get it, it won't work: > >> (flatten 0) > - : (Listof Zero) > '(0) >> (flatten '(0 1)) > flatten: contract violation > two of the clauses in the or/c might both match: ... > > The problem is that an `A' might be a (Listof B), so the generated contract > is ambiguous. The ambiguity also shows up in TR, though it's harder to > understand from the error message: > > (: flatten (All (A) ((Listof* A) -> (Listof A)))) > (define (flatten lst) > (cond [(list? lst) (append* ((inst map (Listof A) (Listof* A)) > flatten > lst))] > [else (list lst)])) > > Expected (Listof (Rec T (U A (Listof T)))) > but got (U (Listof (Rec T (U A (Listof T)))) > (Pairof Any (Listof Any))) > > I think this error message is saying that if `lst' is a list, it really > could be any kind of list. I can't argue with that. > > Is there a way around this particular error message? > > More generally, is it possible to write `flatten' at all? > > Neil ⊥ > _________________________ > Racket Developers list: > http://lists.racket-lang.org/dev _________________________ Racket Developers list: http://lists.racket-lang.org/dev