
On Fri, 21 Dec 2012, Chris Smith
It would definitely be nice to be able to work with a partial Category class, where for example the objects could be constrained to belong to a class. One could then restrict a Category to a type level representation of the natural numbers or any other desired set. Kind polymorphism should make this easy to define, but I still don't have a good feel for whether it is worth the complexity.
Indeed this sort of thing can obviously be done. But it will require some work. The question is where, when, and how much effort, which may mean money, it will take. One encouraging thing is that recently more people understand that type checking/inference in the style of ML/Haskell/etc. is not so hard, and that general constraint solvers/SMT systems can do the job. Getting the compiler to make use of the results of such type estimates/assignments is the hard part today I think. Last night I discovered the best blurb for the program: http://www.cis.upenn.edu/~sweirich/plmw12/Slides/plmw12-Pierce.pdf via the subReddit: http://www.reddit.com/r/dependent_types/ oo--JS.
On Dec 21, 2012 6:37 AM, "Tillmann Rendel"
wrote: Hi,
Christopher Howard wrote:
instance Category ...
The Category class is rather restricted:
Restriction 1: You cannot choose what the objects of the category are. Instead, the objects are always "all Haskell types". You cannot choose anything at all about the objects.
Restriction 2: You cannot freely choose what the morphisms of the category are. Instead, the morphisms are always Haskell values. (To some degree, you can choose *which* values you want to use).
These restrictions disallow many categories. For example, the category where the objects are natural numbers and there is a morphism from m to n if m is greater than or equal to n cannot be expressed directly: Natural numbers are not Haskell types; and "is bigger than or equal to" is not a Haskell value.
Tillmann
______________________________**_________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/**mailman/listinfo/haskell-cafehttp://www.haskell.org/mailman/listinfo/haskell-cafe