[racket] define-type on List and Listof

One problem here is that the type (All (a) t) means that the client provides the type t' for the parameter and then the server of the value has to provide a value that works at the type t[a |-> t'] (t with t' substituted for a appropriately). So, for example, take the type (All (a) (Listof a)). There is a value that works for any type t': the empty list.

Now, with (All (a ...) (List a ... a)), then for any sequence of types the client gives the server to replace into the body of the List type, the value the server gives back to you has to work at that type.  But here, it's not just a single element type; the sequence the client gives the server not only encodes the element types in order, but also the length of the list.  And remember, the client gets to choose that sequence of types without restriction.  Thus, there is no single value that the server can return that satisfies all possible types, since the client requires, by instantiation, a particular list length (so returning the empty list like in the previous example will fail to typecheck for non-empty type sequences).

Stevie

On Jun 17, 2014, at 6:48 PM, Alexander D. Knauth <alexander at knauth.org> wrote:

> Could you represent it with something like (All (a …) (List a … a))?  
> 
> From reading the documentation it seems like it should work, but
> When I tried it, I got this:
> 
> #lang typed/racket
> 
> (define-type MyList (All (a ...) (List a ... a)))
> 
> (ann '(1 2 3) (MyList 1 2 3))
> 
> . Type Checker: Type MyList cannot be applied, arguments were: (One 2 3) in: (MyList 1 2 3)
> 
> On Jun 17, 2014, at 8:33 PM, J. Ian Johnson <ianj at ccs.neu.edu> wrote:
> 
>> I imagine it's because there are no variable-arity type constructors in TR, and (List A ...) is fancy syntax for (Pairof A (Pairof ...  '()) ...) if that notation makes any sense.
>> -Ian
>> ----- Original Message -----
>> From: "Spencer Florence" <spencer at florence.io>
>> To: "racket" <users at racket-lang.org>
>> Sent: Tuesday, June 17, 2014 5:32:55 PM GMT -05:00 US/Canada Eastern
>> Subject: [racket] define-type on List and Listof
>> 
>> 
>> 
>> Hi all, 
>> 
>> I'm trying to rename some types in typed/racket but something odd is happening: 
>> 
>> 
>> (define-type A Listof) 
>> 
>> works but: 
>> 
>> 
>> (define-type B List) 
>> 
>> errors with "Type Checker: parse error in type; type name `List' is unbound in: List" 
>> 
>> Is this a bug or am I missing something? 
>> 
>> --Spencer 
>> ____________________
>> Racket Users list:
>> http://lists.racket-lang.org/users
>> ____________________
>> Racket Users list:
>> http://lists.racket-lang.org/users
> 
> 
> ____________________
>  Racket Users list:
>  http://lists.racket-lang.org/users