[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.toronto at 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