On 2015-03-09 11:26 AM, Ben Franksen wrote:

...

Albert Y. C. Lai wrote:

...

Choose one:

Foo' is a free Foo

Foo' is a limit of the diagram of Foo

Foo' is a terminal object of the [sub]category of Foo

Interesting. Is the last variant how "free <whatever>" is usually defined? Or is it a coincidence that the two, well, coincide here? I remember I have seen other definitions that looked a lot less easy to understand.

I have not checked, and too lazy to.

The usual "free" is the less-easy-to-understand one: you need a forgetful functor, then you need its left adjoint, and you call it your free functor. Then the target objects hit by the free functor are the free things. In general when talking about free things and adjunctions one must pay attention to what the functions are.

The original definition of class Foo was coalgebraic: class Foo f where bar :: f -> Bool baz :: f -> Char -> Int meaning that the functions take an f and make something else rather than taking something and constructing an f (like e.g. the (:) of lists does). With the definition data Foo' = { bar' :: Bool, baz' :: Char -> Int} one can re-write class Foo f where barbaz :: f -> Foo’ Objects of our category Foo are instances of Foo, that are pairs where f is a Haskell type and barbaz is a function f -> Foo’. What are the morphisms? Well, we can consider Foo’ as a phantom type data F a = F Foo’ that is, a constant functor. Then instances of Foo are coalgebras for the functor F, and the right notion of function between coalgebras requires that some equations hold, namely: any h :: f -> f’ that wants to be a Foo-function must have barbaz . h = barbaz. Now we can see that Foo’ is indeed terminal: More precisely, the Foo-instance is terminal. Indeed, if we have some h :: f -> Foo’ with id . h = barbaz then h must be barbaz, so there is precisely one Foo-function from the Foo-instance to . I can’t see how Foo’ would be the free Foo in this category, however. Things change if we let Foo-functions be arbitrary functions. Then the documentation of the free package tells us that the free Foo over type t is the instance <(Foo’,t),barbaz=fst>. Olaf