[racket] define-type on List and Listof

Oh, of course. A polymorphic type just is a type constructor with
arrow kind. Sorry. -J


On Tue, Jun 17, 2014 at 11:06 PM, Alexander D. Knauth
<alexander at knauth.org> wrote:
> But apply-able types are represented as polymorphic types, with All being a kind of lamba-ish thing (I think),
> so this works:
> #lang typed/racket
> (define-type Type-Identity (All (t) t))
> (define-type MyZero (Type-Identity Zero))
> (ann 0 MyZero)
>
> And the documentation for define-type says that
> (define-type (name v …) t)
> is equivalent to
> (define-type name (All (v …) t))
>
> Given that, and the fact that (All (a … a ooo) t) is allowed, and that (List t … trest … bound) is allowed,
> (All (a …) (List a … a)) seems like should work, but it doesn’t.
>
> On Jun 17, 2014, at 10:51 PM, Jon Zeppieri <zeppieri at gmail.com> wrote:
>
>> Well, I think that's because MyList had a different kind than List. List is a type constructor but not a type. MyList, on the other hand, is a (polymorphic) type, and it can't be applied; rather, its type variables need to be instantiated. Though, given its definition, I don't see how you could instantiate all of them.
>>
>>> On Jun 17, 2014, at 8: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
>