Altho in Neil's case, it maybe that he can positively state the types allowed in the leaves.
Robby On Tue, Aug 7, 2012 at 12:55 PM, Sam Tobin-Hochstadt <[email protected]> wrote: > 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 _________________________ Racket Developers list: http://lists.racket-lang.org/dev
