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

[Olaf Klinke]

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