So, is Haskell a category?

AlexandreBMasse

Hi, everyone!

First, I would like to thank all people involved in the organization of this class, especially the three instructors, and for making the videos and the material available for remote participants. This is fantastic! I particularly appreciate the concerns about making this understandable to mathematicians as well as computer scientists.

I have two questions about Definition 1.72 (page 33 of the companion notes http://brendanfong.com/programmingcats_files/cats4progs-DRAFT.pdf), where the category Hask is defined:

1) The hom-sets Hask(A, B) are defined as the set of all compiling Haskell functions A -> B which terminate for every input. If I understand correctly, it would mean that we exclude functions that return infinite lists, for instance f :: Int -> [Int] defined by f n = [n..]? Shouldn't these functions also be included in Hask? Or is it a reasonable assumption to exclude them for sake of simplicity?

2) In page 34, it is mentioned that "[...] we believe we have circumvented his objections. Please let us know if we’ve missed anything!", referring to the blog post http://math.andrej.com/2016/08/06/hask-is-not-a-category/. I am not sure I understand how you answered to the following objection:

Presumably “function” here means “closed expression”. It is then immediately noticed that there is a problem because the supposed identity morphisms do not actually work correctly: seq undefined () = undefined and seq (undefined . id) () = (), therefore we do not have undefined . id = undefined.

Is it possible to have more details about that? I can accept the other assumptions, but this one seems more problematic to accept Hask as a category. I'm not very familiar with seq and strict evaluation, but why do we have seq (undefined . id) () = () instead of seq (undefined . id) () = undefined.

Thank you!

Alexandre B.M.

MatthewDoty

@AlexandreBMass

(1) If you permitted f n = [n...], then you couldn't permit sum xs = foldr (+) (0 :: Integer) xs. This is because there's no inhabitant of Integer that sum . f maps to for any input. In the setting of programming, category theory only makes sense when you can reason about the outputs of your programs.

(2) Try evaluating seq undefined () and seq (undefined . id) () in ghci. You'll see that seq undefined () throws an exception, just like evaluating undefined would. On the other hand seq (undefined . id) () evaluates to (). This is because seq obeys the following two rules (according to the wiki):

⊥ `seq` b = ⊥
a `seq` b = b

Here ⊥ represents a diverging computation such as undefined or Data.Function.fix id.

When Haskell encounters the expression undefined . id, it just sees an unevaluated function. Without any input it doesn't do further analysis to know that undefined . id will crash. So the rules say it should evaluate to (), which is what it does.

Fong et al.'s answer is to this criticism is to not allow for undefined since it throws exceptions, and therefore isn't total. They also don't allow Data.Function.fix, nor [1..], or the infinite sequence of Fibonacci numbers defined by fibs = 1 : 1 : zipWith (+) fibs (tail fibs).

Knowing which functions are allowed or not is the same as solving the halting problem. So in a sense we cannot say exactly which programs are in Hask.

Another approach they could have chosen would be to use the Calculus of Constructions (CoC), rather than Hask. The course would presumably be taught with a computer proof assistant like Lean or Coq instead of Haskell. Every function in CoC is provably total, so there's less debate over whether category theory really applies. And to be honest much of the syntax is basically the same. CoC also has a more powerful type system thank Haskell. With it would be possible to define the category of categories, which you can't do in Haskell as far as I know.

But there are pragmatic reasons for picking Haskell. For instance, being able to define a catamorphism like cata alg = alg . fmap (cata alg) . unFix is convenient. Such recursion isn't allowed in CoC. And while Haskell has a steep learning curve compared to other programming languages, computer proof assistants have a steeper learning curve. It would take a long time to become productive. It would be harder for students to realize the ideas they are being taught.

Outside of this class, Haskell programmers who like category theory just ignore undefined and do their thing. In many cases it does not matter. See Fast and Loose Reasoning Is Morally Correct, Danielsson et. al (2006).