tag:blogger.com,1999:blog-5195188167565410449.post9216149184343758597..comments2024-01-16T07:18:01.728+00:00Comments on Haskell for Maths: Coproducts of lists and free vector spacesDavidAhttp://www.blogger.com/profile/16359932006803389458noreply@blogger.comBlogger5125tag:blogger.com,1999:blog-5195188167565410449.post-44625550331742489002011-03-06T20:19:10.028+00:002011-03-06T20:19:10.028+00:00Hi Loren,
Sorry, your comment got lost in the sys...Hi Loren,<br /><br />Sorry, your comment got lost in the system, and I only just noticed it.<br /><br />So in category theory, monic arrow is defined as left-cancellable, rather than as injective. However, I guess I assumed that was so that the definitions worked in categories where the arrows are not functions (and hence can't be injective), such as the category of tangles, or of 2-cobordisms. I assumed that in a category where the arrows are functions, monic and injective would be the same thing. However, on reflection, I suspect that might be wrong - you could just define a category with very few arrows, and it might turn out that some non-injective function is monic, just because there aren't enough parallel arrows around for left cancellability to be an issue.<br /><br />But I think your concern was more about whether we can witness that a function is injective (or let's say just, do a quickCheck and fail to refute it). It's not immediately clear to me why we need to witness it, although I guess it would be nice if we could set things up so we could.<br /><br />(Mind you, I'm not sure how left-cancellability improves matters as regards witnessing.)DavidAhttps://www.blogger.com/profile/16359932006803389458noreply@blogger.comtag:blogger.com,1999:blog-5195188167565410449.post-86907925912310178872011-01-23T16:27:26.394+00:002011-01-23T16:27:26.394+00:00David, I'm troubled slightly by 'injective...David, I'm troubled slightly by 'injective', because I think that it requires `Eq` constraints on its domain and codomain; that's why I spoke of left cancellability, because it requires `Eq` constraints only on sets of morphisms, which feels more natural to me.<br /><br />I'll make a fuzzy definition. Say that an object `S` admits 'point subobjects' (my probably non-standard terminology), i.e., any time that, every `v :: S` is the image of a map `() -> S`. Then, for morphisms from an object with point subobjects, left cancellability is the same as injectivity. (Proof: If `i v1 == i v2`, then let `j1, j2 :: () -> S` be the maps with `j1 () == v1`, `j2 () == v2`, and observe that `i . j1 == i . j2`.)<br /><br />"Isn't that obvious?" you may say. "Just *define* `j :: () -> S` by `j () == v`." Here's where it gets a little fuzzy. It seems to me that, more or less by definition, the images of maps `() -> Real` are the *computable* real numbers (http://en.wikipedia.org/wiki/Computable_number), which aren't all of them. However, 'witnessing' that would require producing a non-computable `v :: Real`, which, more or less by definition, I can't do within `Hask`. I don't know how to de-fuzz that, but I suspect that it's a genuine issue.<br /><br />Other than that, you're right that letting the type class `Monoid` stand in for my big type `T` is more natural. Thanks!L Shttps://www.blogger.com/profile/10866289941226429119noreply@blogger.comtag:blogger.com,1999:blog-5195188167565410449.post-74344139379970331052011-01-23T14:44:17.654+00:002011-01-23T14:44:17.654+00:00Loren, thanks, that's helpful. So to paraphras...Loren, thanks, that's helpful. So to paraphrase:<br /><br />In place of Set, we use Hask.<br />In place of an algebraic category such as Mon, we might use a type class such as Monoid (or at least an implied type class, such as asking for ++ and [] to be defined).<br />Then given some type x, we say that x' is the closure of x in Mon/Monoid if:<br />- There is an injective (Haskell) function i: x -> x'<br />- x' is an (implied) Monoid instance<br />- Whenever y is another (implied) Monoid instance, and there exists an injective (Haskell) function f: x -> y, then there exists an injective monoid homomorphism f': x' -> y with f = f' . i.<br /><br />I think that's right.DavidAhttps://www.blogger.com/profile/16359932006803389458noreply@blogger.comtag:blogger.com,1999:blog-5195188167565410449.post-83569996361169731232011-01-22T21:01:21.029+00:002011-01-22T21:01:21.029+00:00By the way, I guess I could get away with 'onl...By the way, I guess I could get away with 'only' assuming that `S -> S -> T` (rather than `T` itself) is an instance of `Eq` by requiring the existence of a function `oS` such that `(\v1 v2 -> o $ j v1 $ j v2) == (\v1 v2 -> j $ oS v1 v2)`.L Shttps://www.blogger.com/profile/10866289941226429119noreply@blogger.comtag:blogger.com,1999:blog-5195188167565410449.post-71565955082209709122011-01-22T20:56:13.029+00:002011-01-22T20:56:13.029+00:00I'm not sure I understand your worries about e...I'm not sure I understand your worries about expressing the notion of closure in `Hask`, but here's a go at it. It's a pretty straightforward translation of the mathematical notion. We need the idea of a *subobject*; say that `(s, i)`is a subobject of `S` if `i :: s -> S` is left cancellable, in the sense that, whenever `j1, j2 :: s' -> s` satisfy `i . j1 == i . j2`, we have `j1 == j2`. (Here, I'm assuming that `s' -> S` and `s' -> s` are instances of `Eq`. These assumptions, and similar ones below, are irritating; probably a category theorist would know how to get rid of them. See http://ncatlab.org/nlab/show/strict+category.) One defines a superobject, and a tower of objects, in the obvious way; and suppresses the names of morphisms when convenient.<br /><br />Now say that `(s, i)` is a subobject of `T`, and that `o :: T -> T -> T`. Then an overclosure of `s` in `T` is a tower `T/(S, j)/s` such that, for all `v1, v2 :: S`, we have `o $ j v1 $ j v2 == j v3` for some `v3 :: S`. (Here I need to assume that `T` is an instance of `Eq`.) A closure of `s` is an overclosure `S` such that, for any overclosure `S'`, we have a tower `T/S'/S/s` of objects.L Shttps://www.blogger.com/profile/10866289941226429119noreply@blogger.com