# [Haskell-cafe] Is there a name for this?

Thu Mar 12 21:23:30 UTC 2015

```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 <f,barbaz> 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 <Foo’,barbaz=id> 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 <f,barbaz> to <Foo’,id>.

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