tag:blogger.com,1999:blog-11295132.post8648682395870958209..comments2014-09-11T11:37:51.563-07:00Comments on A Neighborhood of Infinity: Exceptions, Disjunctions and ContinuationsDan Piponihttps://plus.google.com/107913314994758123748noreply@blogger.comBlogger11125tag:blogger.com,1999:blog-11295132.post-28190205672925082632008-09-28T20:21:00.000-07:002008-09-28T20:21:00.000-07:00This is a fantastic post. One of my favorite prog...This is a fantastic post. One of my favorite programming related articles in recent memory.<BR/><BR/>Thanks to you and your readers for a lot of good old fashioned logic.devinhttp://www.blogger.com/profile/01183566927646186069noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-11374530735359455052007-11-04T10:10:00.000-08:002007-11-04T10:10:00.000-08:00This stuff still continues to bake my noodle. In ...This stuff still continues to bake my noodle. In the same spirit, I was playing with combinator types this lazy sunday afternoon, and came up with:<BR/><I><BR/> K : a -> (b -> a)<BR/>==><BR/> a -> (!b or a)<BR/>==><BR/> !a or (!b or a)<BR/>==><BR/> b -> (a or !a)<BR/></I><BR/>which I read as "if <I>b</I> is true, the law of the excluded middle holds for <I>a</I>." That is, the K combinator sets up a classical-logic sandbox for <I>a</I> guarded by <I>b</I>'s truth. (Or, more likely, I'm totally confused. It's entertaining either way.)Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-37226479536151110302007-09-18T16:49:00.000-07:002007-09-18T16:49:00.000-07:00Thanks for your nice post!Thanks for your nice post!Michaelhttp://free-ps3-for-me.blogspot.comnoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-24066487085082511602007-02-14T00:43:00.000-08:002007-02-14T00:43:00.000-08:00import Control.Monadimport Control.Monad.Cont-- co...import Control.Monad<BR/>import Control.Monad.Cont<BR/><BR/>-- compare with scheme at http://sigfpe.blogspot.com/2007/02/exceptions-disjunctions-and.html<BR/><BR/>right b = (\exit -> return b)<BR/>left a = (\exit -> exit a)<BR/><BR/>f x = return ("Left",x)<BR/>g x = return ("Right",x)<BR/><BR/>either_ f g x = flip runCont id $ do<BR/> callCC (\exit -><BR/> (x (\y -> f y >>= exit)) >>= g)<BR/><BR/><BR/>And then<BR/><BR/>*Main> either_ f g (left 'a')<BR/>("Left",'a')<BR/>*Main> either_ f g (right 'a')<BR/>("Right",'a')TuringTesthttp://www.blogger.com/profile/15256574983181139425noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-6177712422496145192007-02-12T10:10:00.000-08:002007-02-12T10:10:00.000-08:00Lots of answers to my exercise! Good thing I was a...Lots of answers to my exercise! Good thing I was away from a net connection for most of the weekend and had a chance to figure it out for myself without seeing other people's answers!<BR/><BR/>Understanding, in detail, exactly why control operators relate to classical logic has taken me a while to figure out. But having thought I grasped it, Derek has now pointed out a deeper level on which this can be viewed. I'll be busy thinking about that now...sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-8928819875452203882007-02-11T03:20:00.000-08:002007-02-11T03:20:00.000-08:00I posted some comments over in the reddit submissi...I posted some comments over in the reddit submission for this blog entry of yours:<BR/><BR/>http://programming.reddit.com/info/13tjo/comments<BR/><BR/>To summarize, i appears to me that catch should have type ((a -> _|_) -> a) -> a, not ~~a. That looks like Peirce's law to me, which should be equivalent to ~~a -> a (but not ~~a), so maybe that's what you meant to write.<BR/><BR/>I also posted a proposed solution to your exercise. It seemed too easy, so I'm sure I must have missed something!<BR/><BR/>Anyway, great article!Per Vognsenhttp://www.blogger.com/profile/06042681400980641198noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-44026453600378478282007-02-10T19:28:00.000-08:002007-02-10T19:28:00.000-08:00In category theory we can define function types vi...In category theory we can define function types via the parameterized adjunction,<BR/>Ax- -| A => -. Symmetry leads us to hope for another parameterized adjunction FA- -| A+-, but what is F? In Set, it's nothing, A+- does not have a left adjoint. However, in other categories, we it does. Let's write it, - <= A. It can be thought of something like a computation that either evaluates to a value of type - or throws a value of type A. Filinski explores this in his <A HREF="http://www.diku.dk/hjemmesider/ansatte/andrzej/papers" REL="nofollow"/>.Derek Elkinsnoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-21235617843122941352007-02-10T19:11:00.000-08:002007-02-10T19:11:00.000-08:00I haven’t read the post properly but just skimming...I haven’t read the post properly but just skimming through the following struck me as odd:<BR/><BR/>In other words, if we use the symbol ∨ to mean either, then exactly in classical logic, we have a ∨ b = ~a → b.<BR/><BR/>But ∨ doesn’t mean either ≠ does. Then we only have a ≠ b → ~a → b.Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-2919265337341153222007-02-10T19:05:00.000-08:002007-02-10T19:05:00.000-08:00Well, one thing we can do with DeMorgan's law is d...Well, one thing we can do with DeMorgan's law is do the classical to intuitionist embedding, and then interpret that in terms of, say Haskell types.<BR/><BR/>a /\ b<BR/>becomes<BR/>(a -> r) -> r /\ (b -> r) -> r<BR/>which would correspond to the pair type:<BR/>((a -> r) -> r, (b -> r) -> r)<BR/><BR/>~(~a \/ ~b)<BR/>becomes<BR/>~(~((a -> r) -> r) \/ ~((b -> r) -> r))<BR/>and, expanding the negations, and using ~~~a -> ~a, we have:<BR/>~(a -> r \/ b -> r)<BR/>or:<BR/>(a -> r \/ b -> r) -> r<BR/>for which in Haskell, we'd use:<BR/>Either (a -> r) (b -> r) -> r<BR/><BR/>The isomorphisms between these two types are easy to exhibit:<BR/><BR/>f :: ((a -> r) -> r, (b -> r) -> r)<BR/> -> (Either (a -> r) (b -> r) -> r)<BR/>f (a,b) (Left c) = c a<BR/>f (a,b) (Right d) = d b<BR/><BR/>g :: (Either (a -> r) (b -> r) -> r)<BR/> -> ((a -> r) -> r, (b -> r) -> r)<BR/>g a = (\b -> a (Left b), \c -> a (Right c))<BR/><BR/>So this might be interpreted as saying that if we have an (a consumer) consumer, and a (b consumer) consumer, then it's the same as having something which can consume either an a consumer or b consumer.Cale Gibbardhttp://www.blogger.com/profile/02239068589033148700noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-67156247660191732962007-02-10T18:36:00.000-08:002007-02-10T18:36:00.000-08:00Just like the identity a ∨ b = ~a -> b was a hint ...Just like the identity <I>a ∨ b = ~a -> b</I> was a hint as to how <I>Either</I> could be implemented, <I>a ∧ b = ~(~a ∨ ~b)</I> similarly hints at an implementation of pairs. <I>(,) a b</I> should thus return a thrower, that is, a function which takes an <I>Either ~a ~b</I> and which does not return:<BR/><BR/><I>(,) :: a -> b -> ~(Either ~a ~b)</I><BR/>-- or, expanding the '~'s<BR/><I>(,) :: a -> b -> (Either (a -> ⊥) (b -> ⊥)) -> ⊥</I><BR/><I>(,) a _ (Left a_thrower) = a_thrower a</I><BR/><I>(,) _ b (Right b_thrower) = b_thrower b</I><BR/><BR/>Getting the values back is a bit trickier, so let's build some scaffolding. When applying <I>call-with-current-continuation</I> to a function of type <I>~a -> b</I>, the result could be either of type <I>a</I> or <I>b</I>, depending on whether the function calls its continuation or returns normally. Thus, <I>call<B>/</B>cc</I> itself must have type <I>(~a -> b) -> Either b a</I>.<BR/><BR/>As a special case, let <I>get<B>/</B>a</I> be the result of applying <I>call<B>/</B>cc</I> to the identity function of type <I>~a -> ~a</I>. This result must have type <I>Either ~a a</I>. When <I>get<B>/</B>a</I> first returns, it will return a <I>Left ~a</I>. If this thrower is applied to some value <I>a</I>, control flow will bungee back to <I>get<B>/</B>a</I> and this time it will return a <I>Right a</I>. We can use this construction to define our accessors as follows:<BR/><BR/><I>fst :: ~(Either ~a ~b) -> a</I><BR/><I>fst meta_thrower = case get<B>/</B>a of</I><BR/><I> Left a_thrower -> meta_thrower (Left a_thrower)</I><BR/><I> Right a -> a</I><BR/><BR/><I>snd</I> is defined symmetrically. When <I>fst</I> is called, it captures the current continuation <I>a_thrower</I> and passes it to the pair through <I>meta_thrower</I>, along with the selector <I>Left</I>. The pair then switches on the selector and gives the value <I>a</I> to <I>a_thrower</I>, which bungees <I>a</I> back to <I>fst</I>, which returns it.gelisamhttp://www.blogger.com/profile/15650058092785119000noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-72161162928759532672007-02-10T15:40:00.000-08:002007-02-10T15:40:00.000-08:00Here is my interpretation of 'a&b = ~(~a | ~b)'.Go...Here is my interpretation of 'a&b = ~(~a | ~b)'.<BR/><BR/>Going from the left to right is valid even constructively, so I don't find it too strange.<BR/>It's realized by<BR/>f (a, b) = \ c -><BR/> case c of<BR/> Left d -> d a<BR/> Right e -> e b<BR/><BR/>Going from right to left involves throwing.<BR/><BR/>So are given a function (~a | ~b) -> _|_ and we have to produce an 'a' and a 'b'.<BR/>First give the function 'Left throw', it has no choice but to use that throw eventually and then we catch the 'a'.<BR/>Similarly, give it 'Right throw' and when it throws, catch the 'b'. And the return (a, b).augustsshttp://www.blogger.com/profile/05153404423721072935noreply@blogger.com