[racket-dev] Is it possible to write `flatten' in TR?

That's currently what I'm doing. The `list->array' function receives a 
predicate that identifies the elements' type.

There are cases where no predicate exists, though (functions, most 
obviously), so I needed another solution. Special array-constructing 
syntax is turning out to be a nice one. I'm working on it now.

Interestingly, I still need to distinguish between (syntax) lists that 
are meant to be rows and (syntax) lists that are meant to be elements. 
I'm detecting bracket shape for that. So this is an array of vectors:

 > (array [(vector 1 2) (vector 3 4)])
- : (View-Array (Vector Integer Integer))
(view-array ['#(1 2) '#(1 2)])

This is an array of something else:

 > (array [vector 1 2])
- : (View-Array (U Positive-Byte (All (a) (a * -> (Vectorof a)))))
(view-array [#<procedure:vector> 1 2])

And this is an error:

 > (array (1 2))
Type Checker: Cannot apply expression of type One, since it is not a 
function type in: (1 2)

As a bonus, I'll finally be able to make printed arrays read as 
equivalent arrays, if their elements are readable.

Neil ⊥

On 08/07/2012 12:11 PM, Sam Tobin-Hochstadt wrote:
> 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
>
>
>