[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.dobson at 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.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
>
> _________________________
>   Racket Developers list:
>   http://lists.racket-lang.org/dev



-- 
sam th
samth at ccs.neu.edu