[Haskell-cafe] category design approach for inconvenient concepts

[Jay Sulzberger]

On Thu, 20 Dec 2012, Oleksandr Manzyuk <manzyuk at gmail.com> wrote:

>> the category of Haskell types and Haskell functions[1]
>>
>> [1] Note that this may not actually work out to be a category, but the basic
>> idea is sound.
>
> I would be curious to see this example carefully worked out.  I often
> hear that Haskell types and Haskell functions constitute a category,
> but I have seen no rigorous definition.
>
> I have no problems with the statement "Objects of the category Hask
> are Haskell types."  Types are well-defined syntactic entities.  But
> what is a morphism in the category Hask from a to b?  Commonly, people
> say "functions from a to b" or "functions a -> b", but what does that
> mean?  What is a function as a mathematical object?  It is a plausible
> idea to say that a function from a to b is a closed term of type a ->
> b (and terms are again well-defined syntactic entities).  How do we
> define composition?  Presumably, by
>
> f . g = \x -> f (g x)
>
> This however already presupposes that we are dealing not with raw
> terms, but with their alpha-equivalence classes (otherwise the above
> is not well-defined as it depends on the choice of the variable x).
> Even if we mod out alpha-equivalence, so defined composition fails to
> be associative on the nose, up to equality of (alpha-equivalence
> classes of) terms.  Apparently, we want to consider equivalence
> classes of terms modulo some finer equivalence relation.  What is this
> equivalence relation?  Some kind of definitional equality?
>
> Apparently, this (rather non-trivial) exercise has already been
> carried out for the simply typed lambda-calculus.  I'd be curious to
> see how that generalizes to Haskell (or some equivalent formal
> system).
>
> Sasha

Yes.  It would be well worth carefully carrying out your program
for some approximation of a large part of Haskell as she lives in
GHC.  As mentioned earlier, we should not ignore the distinctions
between

       a. the text of a Haskell program
       b. the binary of the now compiled program
       c. the running of the program
       d. the input output behavior of the program

Attempting to force the hoped for clarification to operate only
on one part of the whole at least four part structure is likely
to not give us what we, ah, I, really want to see.

There is some work directly dealing with part of the program:

   http://www.haskell.org/haskellwiki/Hask

oo--JS.


> -- 
> Oleksandr Manzyuk
> http://oleksandrmanzyuk.wordpress.com