Hask

hask.markdown

https://www.reddit.com/r/haskell/comments/6i7nil/kinderfunctor_using_typeintype_with_a_polykinded/

https://www.reddit.com/r/haskell/comments/6i7nil/kinderfunctor_using_typeintype_with_a_polykinded/

See https://github.com/ekmett/hask/blob/master/src/Hask/Category.hs#L88 for my first real serious foray into a good kind polymorphic Functor. I have code lying around in other repositories that make better or worse use of the concepts I encoded there, sometimes using UndecidableSuperclasses.

In that repo I used old GHC type system features to abuse the power of 'Any'.

After he saw what I did with it, SPJ decided to take that power away from me.

=/ Easy come easy go.

The version you have here is weak enough that you'll run into problems later on when you get to categorical products.

Unfortunately, parametricity is not naturality! It implies naturality, but parametricity is a stronger claim.

A parametric function (forall a. f a -> g a) is saying there is one function that can be given all of those types and can't act differently based on a.

A natural transformation is a set of morphisms indexed by objects, such that, given any morphism f :: a -> b, eta_b . fmap f = fmap f . eta_a. Each eta_x can be unrelated to any other eta_x, except through this requirement. If the category you start with is, say, a discrete category with two objects, they eta_a and eta_b have no responsibilities with respect to each other, and we can use this two object source category and the limit of a functor from it to define a categorical product.

Without this ability to do different things based on different objects it as such means that when you derive the diagonal functor and the notion of limits/colimits they won't be strong enough to encode products as limits, coproducts as colimits. This shuts the doors on all sorts of foundational category theory.

Fixing this requires that, among other things, Natural needs to know that the endpoints are functors and the better notion of a category needs to be able to prove some constraint about the types of its arguments, or things start to fall apart later on when you go to model bifunctors as functors to a functor category, build categorical products as limits, etc.