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 _________________________________________________ For list-related administrative tasks: http://lists.racket-lang.org/listinfo/users
