Comments on A Neighborhood of Infinity: From Löb's Theorem to Spreadsheet Evaluation

Henning,

In both the 'humour' and 'proposal...

2007-05-05T14:51:00.000-07:00

Henning,

In both the 'humour' and 'proposal' categories!

Do you know my opinion of a Num instance for functions?

Nick, If you're still reading, I just worked out ...

2007-02-03T12:32:00.000-08:00

Nick,

If you're still reading, I just worked out a tiny bit more detail here.

Nick, Well spotted! I looked hard on the web for ...

2007-01-31T15:08:00.000-08:00

Nick,

Well spotted! I looked hard on the web for something with the same signature as loeb but couldn't find anything. I haven't yet fully proved to myself that loeb and cfix are the same thing. They look like they do the same thing but it seems curious that I'm able to define loeb for any Functor, not just for a Comonad. When I have some time I'll investigate further - comonads being a bit of a hobby of mine these days.

You have a neat derivation of "cfix" there! I bum...

2007-01-31T14:25:00.000-08:00

You have a neat derivation of "cfix" there!

I bumped into this once myself when attempting to improve on the Essence of Dataflow semantics. I eventually found this post by David Menendez.

cfix :: Comonad d => d (d a -> a) -> a

which is dual to

mfix :: Monad t => (a -> t a) -> t a

We know mfix needs a special Haskell definition for each monad, but cfix does not, it's applicable to all comonads.

Usually, modal box matches a comonads an modal diamond matches a monad. S4's theorems support the functions:

a -> Dia a
Dia (Dia a) -> Dia a
Box a -> a
Box a -> Box (Box a)

which are (co)unit and (co)join of the (co)monad.

Along the lines of your spreadsheet analogy, you're not alone! I've written up a "non-empty graph" data structure as a comonad with the intent of making a cool spreadsheet semantics in Haskell. I need to dust that off someday...

In regards to fmap not being provable in modal logic, there might be a nuance here. In haskell, the type A matches Box A from a corresponding modal logic: values in Haskell are immutable and thus "necessary" (i.e. Haskell always assumes the trivial Identity comonad). So the type of fmap (for a monad) actually corresponds to:

fmap :: Box (a -> b) -> Dia a -> Dia b

which is a modal logic theorem (called Dia-K).

Satoshi Kobayashi's "Monad as Modality" is good reference (but sometimes hard to obtain). In regards to Yakeley's Code modality, monads seem to play a role in staged-computing, don't remember a reference though. Template Haskell maybe?

- Nick Frisby

Modal logics usually have these rules: f (a ...

2007-01-28T10:39:00.000-08:00
Modal logics usually have these rules:

f (a -> b) -> f a -> f b

(This corresponds to the Applicative class, which may one day be made a superclass of Monad.)

f a -> a

Monads do not in general satisfy this. Perhaps comonads or something?

Yes, they are connected to comonads.

Two functions
extract :: w a -> a
and
extend :: (w a -> b) -> w a -> w b
which follow these laws:
extend extract == id
extract . extend f == f
extend f . extend g == extend (f . extend g)
define a comonad.

David, Num's sneaky!

2006-12-27T18:10:00.000-08:00
David,

Num's sneaky!

Disregard my last comment. After loading up the po...

2006-12-27T15:28:00.000-08:00
Disregard my last comment. After loading up the post in GHCi, I see why it works. The Num definition for functions allows 3 and 17 to be functions which are basically const 3 and const 17.

I realise this is now something of an old post but...

2006-12-27T15:25:00.000-08:00
I realise this is now something of an old post but hopefully you're still picking up the comments. Just a quick question.

Your test3 doesn't seem to be a monomorphic list (and therefore ill-typed in Haskell), is this deliberate? Or were the 3 and 17 meant to be const 3 and const 17 respectively?

Great mind-boggling stuff, by the way :)

matthias, Just had a look at that paper, which I ...

2006-11-24T17:08:00.000-08:00
matthias,

Just had a look at that paper, which I didn't know. It looks like it addresses stuff I've been tossing about in my head for a little while. Not being in academia, I've no idea what are the good papers to read unless they get posted on Lambda the Ultimate. :-)

Do you know Benton et al.'s paper?

Lennart, In the special case where f is the ident...

2006-11-24T14:03:00.000-08:00
Lennart,

In the special case where f is the identity functor, loeb is precisely the usual Y combinator, so it's about as circular as you can get. I just used the type corresponding to Löb's theorem as inspiration for a function definition of that type. However, I must read this paper which makes proper use of a complete provability logic.

Is your way of proving Löb's theorem anything like...

2006-11-24T12:44:00.000-08:00
Is your way of proving Löb's theorem anything like the regular proof? Your code uses recursion in a way that looks dangerously like a circular proof.

Interesting application for a compiler. The other ...

2006-11-24T01:07:00.000-08:00
Interesting application for a compiler. The other approach would be to type a constant t as "t" and code that calculates t as "Code t". Less like modal logic, though.

I've been playing around with the axioms to se...

2006-11-24T00:23:00.000-08:00
I've been playing around with the axioms to see if either □ or ◊ behave like some well-known Haskell class.

Firstly, neither of them are Functors, since you cannot prove either of these even in S5:

  (a→b)→(□a→□b)
  (a→b)→(◊a→◊b)

The second is less obvious than the first, but consider temporal logic: just because 'a' implies 'b' now, and 'a' is sometimes true, it doesn't mean that 'b' is ever true.

This is unfortunate, since axioms T and 4 are suggestive of Monads for ◊:

  T: a → ◊a
  4: ◊◊a → ◊a

K on the other hand doesn't look like anything I've seen in Haskell:

  K: (◊a → ◊b) → ◊(a → b)

ashley, OK, I have some spare moments now. I've s...

2006-11-23T19:24:00.000-08:00
ashley,

OK, I have some spare moments now. I've spent quite a bit of time tinkering round with various axioms of modal logic but as you notice, things have a habit of not quite working out the way you want. There *is* a nice interpretation of □ as something like C/C++'s 'const'. There's a bunch of papers about it and I said something about it here. I've also seen some papers that uses the axiom GL (ie. Loeb's theorem) as a basis for describnig recursive types.

ashley, As I say, I'm not sure there's a deep con...

2006-11-23T15:44:00.000-08:00
ashley,

As I say, I'm not sure there's a deep connection with Loeb's theorem! (But there is surely some link.)

Eeep! The defining property of a functor is this: ...

2006-11-23T14:56:00.000-08:00
Eeep! The defining property of a functor is this:

  fmap :: (a -> b) -> f a -> f b

and not

  ap :: f (a -> b) -> f a -> f b

fmap is definitely not provable in any modal logic.

Modal logics usually have these rules:   f (a -&g...

2006-11-23T14:34:00.000-08:00
Modal logics usually have these rules:

  f (a -> b) -> f a -> f b

(This corresponds to the Applicative class, which may one day be made a superclass of Monad.)

  f a -> a

Monads do not in general satisfy this. Perhaps comonads or something?

Comments on A Neighborhood of Infinity: From Löb's Theorem to Spreadsheet Evaluation

Henning,In both the 'humour' and 'proposal...

Do you know my opinion of a Num instance for functions?

Nick, If you're still reading, I just worked out ...

Nick, Well spotted! I looked hard on the web for ...

You have a neat derivation of "cfix" there! I bum...

Modal logics usually have these rules: f (a ...

David, Num's sneaky!

Disregard my last comment. After loading up the po...

I realise this is now something of an old post but...

matthias, Just had a look at that paper, which I ...

Do you know Benton et al.'s paper?

Lennart, In the special case where f is the ident...

Is your way of proving Löb's theorem anything like...

Interesting application for a compiler. The other ...

I've been playing around with the axioms to se...

ashley, OK, I have some spare moments now. I've s...

ashley, As I say, I'm not sure there's a deep con...

Eeep! The defining property of a functor is this: ...

Modal logics usually have these rules: f (a -&g...

Henning,

In both the 'humour' and 'proposal...