It looks like you're new here. If you want to get involved, click one of these buttons!

- All Categories 2.3K
- Chat 498
- Study Groups 16
- Petri Nets 7
- Epidemiology 3
- Leaf Modeling 1
- Review Sections 9
- MIT 2020: Programming with Categories 52
- MIT 2020: Lectures 21
- MIT 2020: Exercises 25
- MIT 2019: Applied Category Theory 339
- MIT 2019: Lectures 79
- MIT 2019: Exercises 149
- MIT 2019: Chat 50
- UCR ACT Seminar 4
- General 65
- Azimuth Code Project 110
- Statistical methods 2
- Drafts 2
- Math Syntax Demos 15
- Wiki - Latest Changes 3
- Strategy 113
- Azimuth Project 1.1K
- - Spam 1
- News and Information 147
- Azimuth Blog 149
- - Conventions and Policies 21
- - Questions 43
- Azimuth Wiki 707

Options

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 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):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

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

isconvenient. Such recursion isn't allowed in CoC. And while Haskell has a steep learning curve compared to other programming languages, computer proof assistants have asteeperlearning 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).`