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