[racket] Typed racket puzzle (ii)

On Wed, Aug 17, 2011 at 11:04 AM, Norman Gray <norman at astro.gla.ac.uk> wrote:
>
> Sam,
>
> We may be drifting off the point, so I'd better rein back, but...
>
> On 2011 Aug 17, at 15:10, Sam Tobin-Hochstadt wrote:
>
>>> Thanks for 'contravariant' in this context.  It's led me to the relevant application of category theory, which I think is the underlying structure I was looking for.  I suppose it's effectively a combination of 'define' and ':' which is in practice the functor in TR terms, with subtyping being the morphism in the type category.  Or something like that.
>>
>> I don't think `define' and `:' are functors in any sensible category
>> of Typed Racket types.  But I've been surprised before.  In
>> particular, `define' is solely about computation, not about types.
>
> I was trying to make sense of the similar remark in <http://en.wikipedia.org/w/index.php?title=Covariance_and_contravariance_(computer_science)&oldid=444339536#Origin_of_the_terms>.
>
> Any function definition (in any language) implicitly creates an object in the type category; implicit, because it's actually talking, as you say, about computation rather than types.

No, that's not right.  The objects in the category described in the
wikipedia article are *types*, not functions.

>  The ':' form makes this explicit, by creating a manipulable object in the type category.  So I suppose the real functor is the implicit statement that the things created by the 'define' and ':' forms are 'the same thing'.

The `:' form doesn't allow you to manipulate types; it's part of the
implementation of Typed Racket.  It tells the implementation how to
handle other occurrences of the identifier that is its first subform.
Also, I have no idea what a "manipulable object" would be, anyway.

Category theory can sometimes produce useful insights for programming
languages, but it's very important to be precise about what you're
talking about when you try to use mathematics to understand a system.
-- 
sam th
samth at ccs.neu.edu