### Ashley Yakeley

Shared publicly  -

Hask does not have sums or products, or initial or terminal objects. I rewrote this page, but there's more one could add. #CategoryTheory

4

Many people, on seeing that Hask isn't a category are tempted to look for a substructure that is a category. I think it's better to concentrate on how theorems about categories can be converted into propositions about Hask. I think you get a lot more true propositions that way. In particular, theorems about CCCs have wider applicability than "The corresponding category [which] has the expected initial and terminal objects, sums and products, and instances of Functor and Monad really are endofunctors and monads."

Of course someone needs to document how you translate these theorems. The Fast and Loose paper is one example.﻿

I believe Hask is a category. Regardless of how they've been defined, two functions f,g are the same morphism iff for all x, f x = g x.﻿

So mostly, I'm interested in being confident that my program terminates and generally has no bottom values in it. For example:

inflist = ():inflist

len [] = 0
len (_:l) = 1 + len l

Since "len inflist" is bottom, it's useful if I can ban one or the other. My approach is to say len is fine because it's primitive recursive, but inflist is not because it's one of those nasty lazy infinite data things. I may have no concept of codata, so inflist just looks like "bad attempt at data" to me, something that shouldn't exist.

But takes the opposite approach, inflist is perfectly good codata, while len is bad because, if I understand him correctly, it's trying to make data from codata in a bad way. It's a bad attempt at a function and shouldn't exist.

It seems to me our two different approaches correspond to two different categories, each with faithful functors to Hask, and we use these functors to write our programs and to carry across assurances (i.e. theorems). But we can't mix them! We each have to pick a category to work in. I want to know what these categories are.﻿

Even if Hask can be considered a category (I'm trying to remember why I doubted whether it was), the useful theorems about it might not be categorial - for example you might have theorems that say "as long as you don't apply this function to this particular value you know that this equals that".﻿

Can these be expressed with types? This value has type A1, and this function has type A2 -> B, and both A1 and A2 map to A under the functor to Hask.﻿

So in Coq, objects like inflist and len can exist, functions are total, but types and functions do not form a category, is that correct?﻿

I hope a Coq person comes along and explains because I've never looked closely at codata on Coq. But if finite lists and infinite lists have separate types and len can only be applied to finite lists then you might still have a category.﻿

, in Agda and, I guess, in Coq too, the type of inflist is different from the type of the argument of len, so len can not be applied to inflist. Does that clarify anything? I believe the types and functions there do form a category.﻿

Awesome! And if Agda can generate Haskell code, presumably there's a faithful functor from this category to Hask.﻿

Oh dear. I think Isabelle's code generator does a bit better than this.﻿

Is that even safe? My understanding is that the only guarantee of unsafeCoerce is "unsafeCoerce :: a -> a = id".﻿

Well, I guess if the code was well-typed in Agda, then all the types should match, but the Haskell compiler could sometimes fail to see that.﻿

After working on Isabelle's code base for some time, I can pretty definitively state that Isabelle probably doesn't do anything better than anything.﻿

Was it you who described Isabelle as "the C++ of proof assistants"?﻿

My main gripe with it is mostly on a user interface level, as well as my personal objection to the horrible code style used in the ML source.﻿

(I also find it somewhat irritating that the only way to add new tactics, macros, or shortcuts to Isabelle is to use ML, which works on a lower abstraction level than Isar or proof scripts).﻿