More generally, this is a case where you want some form of negation (plus bounded polymorphism) in the type system, but that's not something I know how to add straightforwardly to Typed Racket.
Sam On Tue, Aug 7, 2012 at 1:07 PM, Eric Dobson <[email protected]> wrote: > 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 <[email protected]> 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 -- sam th [email protected] _________________________ Racket Developers list: http://lists.racket-lang.org/dev
