[racket] Typed racket puzzle (ii)

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.  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'.

But here we drift into applied philosophy, which cannot be safely done without a drink in hand, so I'd better stop.

Thanks!

Norman


-- 
Norman Gray  :  http://nxg.me.uk
School of Physics and Astronomy, University of Glasgow, UK