Re: [racket-dev] Is it possible to write `flatten' in TR?
On 08/07/2012 12:52 PM, Prabhakar Ragde wrote: Neil wrote: (define (flatten lst) (cond [(list? lst) (append* ((inst map (Listof A) (Listof* A)) flatten lst))] [else (list lst)])) This version of flatten has quadratic worst-case running time. Is that an issue? A linear-time implementation is possible. Eli has a nice post somewhere about this. That would probably run into the same type issues (no better, no worse). --PR For closure, quadratic-time and linear-time `flatten' in Typed Racket: #lang typed/racket (define-type (Listof* A) (Rec T (U A (Listof T (: flatten-quadratic (All (A) ((Listof* A) ((Listof* A) - Boolean : A) - (Listof A (define (flatten-quadratic lst pred?) (let loop ([lst lst]) (cond [(pred? lst) (list lst)] ; must check this first! [else (append* (map loop lst))]))) (: flatten (All (A) ((Listof* A) ((Listof* A) - Boolean : A) - (Listof A (define (flatten lst pred?) (reverse (let loop ([lst lst] [#{acc : (Listof A)} empty]) (cond [(pred? lst) (cons lst acc)] [else (for/fold ([acc acc]) ([x (in-list lst)]) (loop x acc))] (flatten 4 number?) - : (Listof Complex) '(4) (flatten '(()) number?) - : (Listof Complex) '() (flatten '(((1 2) (3 4)) ((5 6) (7 8))) number?) - : (Listof Complex) '(1 2 3 4 5 6 7 8) (define-predicate listof-number? (Listof Number)) (flatten '(()) listof-number?) - : (Listof (Listof Complex)) '(()) (flatten '() listof-number?) - : (Listof (Listof Complex)) '(()) (flatten '((4 5) ((6 7) (8 9))) listof-number?) - : (Listof (Listof Complex)) '((4 5) (6 7) (8 9)) The array library does something a little different. At the point where `flatten' is required, it knows the shape of the intended array (thus the size), so it allocates a vector and bangs the elements into it. I tried doing the same in `flatten', but it ended up a little slower. Neil ⊥ _ Racket Developers list: http://lists.racket-lang.org/dev
[racket-dev] Is it possible to write `flatten' in TR?
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
Re: [racket-dev] Is it possible to write `flatten' in TR?
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
Re: [racket-dev] Is it possible to write `flatten' in TR?
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
Re: [racket-dev] Is it possible to write `flatten' in TR?
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 _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] Is it possible to write `flatten' in TR?
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
[racket-dev] Is it possible to write `flatten' in TR?
Neil wrote: (define (flatten lst) (cond [(list? lst) (append* ((inst map (Listof A) (Listof* A)) flatten lst))] [else (list lst)])) This version of flatten has quadratic worst-case running time. Is that an issue? A linear-time implementation is possible. Eli has a nice post somewhere about this. That would probably run into the same type issues (no better, no worse). --PR _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] Is it possible to write `flatten' in TR?
On 08/07/2012 12:52 PM, Prabhakar Ragde wrote: Neil wrote: (define (flatten lst) (cond [(list? lst) (append* ((inst map (Listof A) (Listof* A)) flatten lst))] [else (list lst)])) This version of flatten has quadratic worst-case running time. Is that an issue? A linear-time implementation is possible. Eli has a nice post somewhere about this. That would probably run into the same type issues (no better, no worse). --PR Ah! I'll have to have a look at my `list-flatten' and `vector-flatten' that use a predicate to distinguish elements, to make sure they don't have this problem. Thanks for pointing it out! Neil ⊥ _ Racket Developers list: http://lists.racket-lang.org/dev