[Haskell-cafe] Categories (cont.)

[Jay Sulzberger]

On Fri, 21 Dec 2012, Chris Smith <cdsmith at 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" <rendel at 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 at haskell.org
>> http://www.haskell.org/**mailman/listinfo/haskell-cafe<http://www.haskell.org/mailman/listinfo/haskell-cafe>
>>
>