On Fri, 21 Dec 2012, Chris Smith <cdsm...@gmail.com> wrote:
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" <ren...@informatik.uni-marburg.de>
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-cafe<http://www.haskell.org/mailman/listinfo/haskell-cafe>
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
