[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
<robby at 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 <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



-- 
sam th
samth at ccs.neu.edu