But this works:
#lang typed/racket
(define-type My-Function
(All (arg result)
(arg -> result)))
(: f : (My-Function Any Zero))
(define (f x) 0)
But after trying a few things, I think that maybe ellipses don’t work with
apply-able types, even though All (without the ellipses) does.
On Jun 18, 2014, at 12:09 AM, Stevie Strickland <sstri...@ccs.neu.edu> wrote:
> 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 <alexan...@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 <i...@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" <spen...@florence.io>
>>> To: "racket" <users@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
>
____________________
Racket Users list:
http://lists.racket-lang.org/users
