tag:blogger.com,1999:blog-11295132.post7800915298217494425..comments2017-02-23T14:47:15.917-08:00Comments on A Neighborhood of Infinity: "What Category do Haskell Types and Functions Live In?"Dan Piponihttps://plus.google.com/107913314994758123748noreply@blogger.comBlogger22125tag:blogger.com,1999:blog-11295132.post-2692199656965514772009-11-05T11:23:12.439-08:002009-11-05T11:23:12.439-08:00Cory,
(A suitable fragment of) linear logic is an...Cory,<br /><br />(A suitable fragment of) linear logic is another nice example of an internal language. This time for closed symmetric monoidal categories. And again it gives rise to a fragment of a programming language.sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-88166490232601786892009-11-05T11:17:01.074-08:002009-11-05T11:17:01.074-08:00Thanks, Dan, that makes perfect sense. Linear logi...Thanks, Dan, that makes perfect sense. Linear logic is one of those things that's right on the edge of the horizon of things I need to learn.Coryhttp://www.blogger.com/profile/07752328226179627747noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-36757633831673028622009-10-29T00:33:35.287-07:002009-10-29T00:33:35.287-07:00Hopefully Neel won't mind if I answer some.
L...Hopefully Neel won't mind if I answer some.<br /><br />Linear logic tracks resource usage explicitly (aside from the modalities that let you express ordinary logical statements in it). If you think about linear logic through the lens of type systems, then something with type:<br /><br />A -o B<br /><br />is a function that uses its argument A exactly once to produce a B, -o being the linear implication connective. So:<br /><br />\_ -> b<br /><br />is not acceptable, nor is:<br /><br />\a -> f a a<br /><br />But, what about something with type:<br /><br />A * B -> C<br /><br />There are two ways you can think about eliminating products:<br /><br />\(a,b) -> ... a ... b ...<br />\p -> ... fst p ...<br />\p -> ... snd p ...<br /><br />In Haskell, those two are mixed, because you can do:<br /><br />\p -> ... fst p ... snd p ...<br />\(a,b) -> ... a ...<br />\(a,b) -> ... b ...<br /><br />But those are not acceptable in linear logic, because the first uses p twice, and the others leave one thing unused. So, linear logic has to types of conjunction/product to distinguish these two cases:<br /><br />f, g : A & B -o C<br />f p = ... fst p ...<br />g p = ... snd p ...<br /><br />h : A x B -o C<br />h (a,b) = ... a ... b ...<br /><br />A & B can be used to prove/obtain either an A or a B, but not both, while A x B provides both A and B, and you must use both. There's also A + B which is similar to the sum types in Haskell (classical linear logic also has "multiplicative disjunction" ⅋, but I'm not familiar enough with the classical stuff to tell you about it).<br /><br />Anyhow, back in total type theory, we're allowed to use values as many times as we wish, so the only difference between matching and using fst/snd would be the order in which things are evaluated (if that), and in a total language, normal forms are reached regardless of evaluation order.<br /><br />However, in a language like Haskell, you can again distinguish the two usages, because evaluation order can make a difference as to whether or not things terminate. Using pairs as if they were A & B is noticeably different from using them as if they were A x B. If you were dedicated to keeping them separate (and not writing fst for A x B even though you can in Haskell, etc.), the types could give you (vague, probably) information about the strictness/evaluation order of your program.<br /><br />Or, of course, you could go whole hog, and build a type system based on linear logic, and program in that (which has been done; one reason people are interested in such type systems is that they track precisely when you're allowed to deallocate things, so you can be, in theory, more eager in that regard than a garbage collector; closer to manual memory management, if that's what you're after).Dan Doelhttp://www.blogger.com/profile/16761291400347369301noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-59975368727190250992009-10-28T09:49:22.386-07:002009-10-28T09:49:22.386-07:00Neel, Your point about the two types of pairs seem...Neel, Your point about the two types of pairs seems interesting, but I don't quite understand it. Would you be so kind as to explain it at a slightly lower level?Coryhttp://www.blogger.com/profile/07752328226179627747noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-86192720174949163362009-10-27T06:45:35.314-07:002009-10-27T06:45:35.314-07:00Extending Dan's comments: there are actually t...Extending Dan's comments: there are actually two sorts of pair, which both Haskell and ML (unfortunately) conflate. There's the strict pair, whose elimination is by pattern matching, and the lazy pair, whose elimination is by projection. <br /><br />These two notions of pair coincide for total functional languages, but they are naturally different in linear logic -- where they show up as the tensor and with connectives, with entirely different linearity behavior. The distinction becomes visible again in impure functional languages (such as Haskell and ML) where nontermination lets you distinguish them. The strict pair gives rises to symmetric monoidal structure, and the lazy pair gives you Cartesian product structure. (Both of these are closed, so there's a strict and lazy function space, as well.) <br /><br />It's this ambiguity that Dan is exploiting when he observes that seq can be defined using pattern matching for any algebraic datatype -- you can inductively follow the structure to figure out where to use the "wrong" elim-form. Seq is even worse than that, though, because it lets you distinguish between \x. bot and bot.Neel Krishnaswamihttp://www.blogger.com/profile/06853898957395028131noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-21600589613493357172009-10-24T11:53:17.273-07:002009-10-24T11:53:17.273-07:00Yeah, mentioning Haskell as an internal language o...Yeah, mentioning Haskell as an internal language of various sorts of categories is good if only because it's a fairly interesting fact that such languages, which look rather concrete, in that we're talking about values that inhabit types, which is a no-no in category theory, can actually be made sense of in categories that aren't so concrete.<br /><br />However, I don't want to oversell my last point. It's true that Haskell's semantics ruin it categorically, but that probably doesn't matter. We typically don't intend to write programs where functions end up as _|_; that'd be a bug that'd need to be fixed (the usual time it shows up intentionally, instead of as a semantic necessity, is during type hackery). So it's probably the case that:<br /><br />id . f = f = f . id<br /><br />for all fs that we actually care about. And similarly for eta rules for data.<br /><br />And this point is made more rigorous in the (relatively) famous paper <a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.59.8232" rel="nofollow">Fast and Loose Reasoning is Morally Correct</a>. In fact, at the end, they even give a category with which one can reason about the portion of Haskell we care about behaving categorically.Dan Doelhttp://www.blogger.com/profile/16761291400347369301noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-65395437629906296552009-10-24T08:34:04.061-07:002009-10-24T08:34:04.061-07:00Dan,
Good example of Haskell functions and types ...Dan,<br /><br />Good example of Haskell functions and types not even forming a category. I'm liking the internal language view more and more as a way of making sense of CT talk about Haskell programs.sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-74424982953391283432009-10-24T00:45:04.511-07:002009-10-24T00:45:04.511-07:00seq (the primitive) isn't necessary to keep Ha...seq (the primitive) isn't necessary to keep Haskell tuples from being products. Pattern matching is enough. Take the eta rule for pairs, for instance:<br /><br />p = (fst p, snd p)<br /><br />This is invalidated by the function:<br /><br />f :: (Int, Int) -> Int<br />f (_,_) = 1<br /><br />for p = _|_. In fact, you can implement seq for any algebraic type using case analysis. Merely making tuples strict doesn't work, either, because we're supposed to have commutativity rules like:<br /><br /> f : A -> B<br /> g : A -> C<br /><br /> fst . <f,g> = f<br /> snd . <f,g> = g<br /><br />but if we have element-strict tuples, then:<br /><br /> f _ = _|_<br /> g _ = 1<br /><br /> snd . <f,g> = \_ -> _|_<br /><br />so, an actual categorical product would seem to be an unlifted tuple, where<br /><br /> (f,g) = _|_ iff f = _|_ & g = _|_<br /><br />seq does break the eta rule for functions, which normally wouldn't be possible, though, which means that haskell-types-and-functions technically don't even meet the definition of a category, because:<br /><br />id . _|_ = \x -> id (_|_ x)<br />_|_ . id = \x -> _|_ (id x)<br /><br />both of which seq recognizes as non-bottom, when according to the definition of a category, they should be bottom (and they are, extensionally, but seq doesn't respect expected extensional equality).Dan Doelhttp://www.blogger.com/profile/16761291400347369301noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-7821943870625639302009-10-21T14:24:17.628-07:002009-10-21T14:24:17.628-07:00Good stuff!
Your comments on "plumbing"...Good stuff!<br /><br />Your comments on "plumbing" and index notation reminded me of the results on TQFT and Frobenius algebras. I don't know how (or if) Penrose's index notation is related, but I've seen Einstein summation notation turned into something that looks very much like a plumbing diagram - or, if you prefer, a game of PipeMania :-) See Joachim Kock's book on the subject if you're not familiar with it.mileshttp://www.blogger.com/profile/07136909835648629963noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-36937924636616401272009-10-18T09:03:56.970-07:002009-10-18T09:03:56.970-07:00yitz,
Not sure what you mean by "usual tweak...yitz,<br /><br />Not sure what you mean by "usual tweaks". My main goal here is to justify using Haskell to illustrate ideas from category theory. I have done lots of this, but usually it takes the form "here's what happens when we specialise this theorem to Hask (whatever that means) and by analogy you can see how it might work for more general categories". Now I can say "this purely Haskell based argument can be mechanically converted into a genuine proof for some family of categories".sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-80732499465640913592009-10-18T08:45:52.535-07:002009-10-18T08:45:52.535-07:00Existential Type,
You're right. Any time you ...Existential Type,<br /><br />You're right. Any time you have a mechanism for translating from (a fragment of) one formal system to another, in a way that carries over proofs and intuition, you have a useful tool. It doesn't matter whether the source is Haskell, ML, ZFC or anything else.<br /><br />I think this is an interestingly non-trivial thing in practice. In the case of typed lambda calculus you make repeated use of the deduction lemma to turn lambda expressions into the language of CCC and it's not obvious at first that this can be done.sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-66297520561002687972009-10-18T05:57:36.953-07:002009-10-18T05:57:36.953-07:00But the pointfree version of "iso" is no...But the pointfree version of "iso" is not the same as the pointed version - it is less strict. So I still don't see how your "mechanical" translation is any different than the usual tweaks - either ignore strictness, or use strict function composition.yitznoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-33653637342000159622009-10-18T03:19:35.804-07:002009-10-18T03:19:35.804-07:00No, this isn't correct. In the presence of rec...No, this isn't correct. In the presence of recursion, laziness means you lose the eta-rule for coproducts, and strictness means you lose the eta-rule for products and function types.<br /><br />Ie, in a strict language with general recursion, the equation (f e == case e of Inl x -> f (Inl x) | Inr y -> f (Inr y)) holds. This is because e will always be evaluated, and so this eta-expansion will not change the termination behavior of the program. In a lazy language, e might not be evaluated, and the eta-expansion can cause it to be run.<br /><br />There's a dual property for products; it should be the case that e == (fst e, snd e) in a lazy language. Unfortunately, this doesn't hold in Haskell, because of seq -- Haskell tuples are not categorical products. <br /><br />It's easiest to see this with the unit type; it ought to be the case that () == bot at unit type -- but seq lets you distinguish those two cases.Neel Krishnaswamihttp://www.blogger.com/profile/06853898957395028131noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-58722012631018840812009-10-17T22:16:45.330-07:002009-10-17T22:16:45.330-07:00How so? Haskell is readily transliterated into ML...How so? Haskell is readily transliterated into ML (but not conversely). Every expression in Haskell literally _is_ an expression in ML (but not conversely).Existential Typehttp://www.blogger.com/profile/05595505123938492280noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-3490755832636326382009-10-17T22:08:00.012-07:002009-10-17T22:08:00.012-07:00True, CPO can provide semantic models for the exec...True, CPO can provide semantic models for the <em>execution</em> of programs.<br /><br />In the context of your post, where you are referring to the category of the <em>type system</em> for a programming language, the implication is we are talking about properties of <em>syntactic representations</em> of programs. <br />It is this latter sort of category I'm suggesting doesn't exist.<br /><br />The intuition I'm promoting is that the very reason that categories which include non-termination lose the nice "language" properties, such as coproducts, is because of the loss of information that is introduced by non-termination.<br /><br />The only option to regain these nice "language" properties in the presence of termination is to over-extend the model to include obviously excessive arrows as well.Marc Hamannhttp://www.blogger.com/profile/11526878435261617011noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-29662321210663092412009-10-17T22:06:37.575-07:002009-10-17T22:06:37.575-07:00Existential Type,
Yes, any strongly typed pure fu...Existential Type,<br /><br />Yes, any strongly typed pure functional language would do. But one advantage Haskell has over strict languages is that because of laziness, many more mathematical expressions give rise to terminating programs.sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-33415788083259944792009-10-17T21:32:57.105-07:002009-10-17T21:32:57.105-07:00There's nothing special about Haskell as an in...There's nothing special about Haskell as an internal language for a class of categories; one could just as well use any other decently functional language for the same purpose.Existential Typehttp://www.blogger.com/profile/05595505123938492280noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-84802170295515702662009-10-17T21:30:28.761-07:002009-10-17T21:30:28.761-07:00Marc,
Even if we can't determine what program...Marc,<br /><br />Even if we can't determine what programs terminate, computability is a well-defined mathematical concept. In fact, there are perfectly good categories for representing functions that might not terminate (eg. the category of CPOs). But these categories don't have the properties that people take for granted - like that the type (a,b) the product of a and b.sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-38970581872178685552009-10-17T20:41:23.861-07:002009-10-17T20:41:23.861-07:00Having thought about the problem for quite a long ...Having thought about the problem for quite a long time, I'm inclined to go a step further and claim that there can be <em>no</em> category that is exactly equivalent to a Turing-complete language.<br /><br />The intuitive reason is that any category worthy of the name is defined by its arrows: those it has by definition or those that it can be inferred to have.<br /><br />Since there is no <em>a priori</em> way to determine what functions are computable, we can't have a satisfactory definition for the arrows in a category of all (and only) computable functions.<br /><br />Why do functions in Haskell still show category-theoretic properties so often? <br /><br />In practice, we tend to write programs that are:<br /><br />- provably terminating<br />- provably non-terminating under-known circumstances<br />- provably "correct" if we were allowed to non-terminate in a well-behaved way.<br /><br />In general, such functions <em>do</em> tend to be arrows in some well-defined category that is either an embedded sub-space of the computable functions (e.g. typed λ-calculus) or a conservative super-space of them (e.g. Set).<br /><br />Does this match your thinking in suggesting a "better question"?Marc Hamannhttp://www.blogger.com/profile/11526878435261617011noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-22484059288413003882009-10-17T19:26:58.959-07:002009-10-17T19:26:58.959-07:00Saizan,
Yes, just like type classes, but they'...Saizan,<br /><br />Yes, just like type classes, but they're sort of implicit depending on which features of Haskell you use.sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-43273890452398375422009-10-17T18:26:17.779-07:002009-10-17T18:26:17.779-07:00So the idea is that in this context we should thin...So the idea is that in this context we should think of haskell as something even more general than what the conventional denotational semantics would suggest.<br /><br />It shouldn't be a so weird notion to haskell programmers, when we write typeclass polymorphic context we already have to avoid thinking only in terms of specific instances if we want to understand the code in its full scope.<br /><br />This is taking it a step further, and realizing that things like seq aren't part of what we should overload.<br /><br />am i getting the point of this post?Saizanhttp://www.blogger.com/profile/07314943153376710289noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-31859038787768879472009-10-17T16:39:30.998-07:002009-10-17T16:39:30.998-07:00Thank you for this post. I've often wondered w...Thank you for this post. I've often wondered whether Haskell fits easily into a category and what the value of category theory is to Haskell if it doesn't.<br /><br />I believe there is a missing quote mark here:<br /><br /><i>In their book Introduction to Higher-Order Categorical Logic, Lambek and Scott showed that "pure typed λ-calculus is the internal language of CCCs. Even though expressions in the λ-calculus contain named variables these can always be eliminated and replaced by point-free forms. Theorems about typed λ-calculus are actually theorems about CCCs.<br /></i>Jason Dusekhttp://www.blogger.com/profile/15702067426651391511noreply@blogger.com