Yes, if you can do that, then it will all work nicely. On Tue, Aug 7, 2012 at 1:59 PM, Robby Findler <ro...@eecs.northwestern.edu> wrote: > 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 <sa...@ccs.neu.edu> > 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 <eric.n.dob...@gmail.com> 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 <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 >> >> >> >> -- >> sam th >> sa...@ccs.neu.edu >> >> _________________________ >> Racket Developers list: >> http://lists.racket-lang.org/dev
-- sam th sa...@ccs.neu.edu _________________________ Racket Developers list: http://lists.racket-lang.org/dev