It looks like you're new here. If you want to get involved, click one of these buttons!
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.
Comments
@AlexandreBMass
(1) If you permitted
f n = [n...]
, then you couldn't permitsum xs = foldr (+) (0 :: Integer) xs
. This is because there's no inhabitant ofInteger
thatsum . 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 ()
andseq (undefined . id) ()
inghci
. You'll see thatseq undefined ()
throws an exception, just like evaluatingundefined
would. On the other handseq (undefined . id) ()
evaluates to()
. This is becauseseq
obeys the following two rules (according to the wiki):Here
⊥
represents a diverging computation such asundefined
orData.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 thatundefined . 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 allowData.Function.fix
, nor[1..]
, or the infinite sequence of Fibonacci numbers defined byfibs = 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).@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](https://wiki.haskell.org/Seq)): ⊥ `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](https://en.wikipedia.org/wiki/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)](https://en.wikipedia.org/wiki/Calculus_of_constructions), rather than **Hask**. The course would presumably be taught with a computer proof assistant like [Lean](https://leanprover.github.io/) or [Coq](https://coq.inria.fr/) 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)](https://www.cs.ox.ac.uk/jeremy.gibbons/publications/fast+loose.pdf).