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
