It looks like you're new here. If you want to get involved, click one of these buttons!
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.