[Haskell-cafe] category design approach for inconvenient concepts

Alexander Solla alex.solla at gmail.com
Fri Dec 21 03:40:59 CET 2012


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

> 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?
>

I don't see how associativity fails, if we mod out alpha-equivalence.  Can
you give an example?  (If it involves the value "undefined", I'll have
something concrete to add vis a vis "moral" equivalence)
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20121220/01f960ff/attachment.htm>


More information about the Haskell-Cafe mailing list