Comments on A Neighborhood of Infinity: Exceptions, Disjunctions and Continuations

This is a fantastic post. One of my favorite prog...

2008-09-28T20:21:00.000-07:00

This is a fantastic post. One of my favorite programming related articles in recent memory.

Thanks to you and your readers for a lot of good old fashioned logic.

This stuff still continues to bake my noodle. In ...

2007-11-04T10:10:00.000-08:00

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:

K : a -> (b -> a)
==>
a -> (!b or a)
==>
!a or (!b or a)
==>
b -> (a or !a)

which I read as "if b is true, the law of the excluded middle holds for a." That is, the K combinator sets up a classical-logic sandbox for a guarded by b's truth. (Or, more likely, I'm totally confused. It's entertaining either way.)

Thanks for your nice post!

2007-09-18T16:49:00.000-07:00

Thanks for your nice post!

import Control.Monad
import Control.Monad.Cont<...

2007-02-14T00:43:00.000-08:00

import Control.Monad
import Control.Monad.Cont

-- compare with scheme at http://sigfpe.blogspot.com/2007/02/exceptions-disjunctions-and.html

right b = (\exit -> return b)
left a = (\exit -> exit a)

f x = return ("Left",x)
g x = return ("Right",x)

either_ f g x = flip runCont id $ do
callCC (\exit ->
(x (\y -> f y >>= exit)) >>= g)

And then

*Main> either_ f g (left 'a')
("Left",'a')
*Main> either_ f g (right 'a')
("Right",'a')

Lots of answers to my exercise! Good thing I was a...

2007-02-12T10:10:00.000-08:00

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!

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...

I posted some comments over in the reddit submissi...

2007-02-11T03:20:00.000-08:00

I posted some comments over in the reddit submission for this blog entry of yours:

http://programming.reddit.com/info/13tjo/comments

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.

I also posted a proposed solution to your exercise. It seemed too easy, so I'm sure I must have missed something!

Anyway, great article!

In category theory we can define function types vi...

2007-02-10T19:28:00.000-08:00

In category theory we can define function types via the parameterized adjunction,
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 .