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 <zeppi...@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" <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
