Löb and möb: strange loops in Haskell (2015)

https://github.com/quchen/articles/blob/master/loeb-moeb.md

by hjnkk • 3 years ago

153 60 3 years ago

github.com

ktpsns• 3 years ago

tl,dr; (extracted from the article itself)

In a sense this is like a generalization of a fixed point combinator.

lynx23• 3 years ago

Feeling smart? Lets change that.

Great quote, I gotta remember that.

chpatrick3• 3 years ago

Another weird type signature is:

  excludedMiddle :: Cont c (Either (b -> c) b)
  excludedMiddle = cont $ \c -> (c . Left) (c . Right)

platz2• 3 years ago

why is it weird; a breif description of the observation would be helpful

chpatrick3• 3 years ago

Because at first glance it looks like it produces a value of type

  Either (b -> c) b

out of "thin air". (Really it comes from the continuation but intuitively it looks unusual).

tel• 3 years ago

A value of type

    forall a b. Either (a -> b) a

is particularly dangerous because we can pick b to be uninhabited (Void)

    forall a. Either (a -> Void) a

which is the law of excluded middle, for any type we either can immediately summon an example or prove that no example exists, as having a function (A -> Void) would allow us to create a value of the uninhabited type if we had a value of A.

But forall r a. Cont r (Either (a -> r) a) is fine. Let's see what happens when we set c = Void and unwrap the Cont

    lem               : forall r a. Cont r (Either (a -> r) a)
    runCont lem @Void : forall a. (Either (a -> Void) a -> Void) -> Void

It turns into a weird statement, a double-negation, that there exists no proof that (Either (a -> Void) a), the true LEM type, is uninhabited. Not the same as actually having such a value.

Consider the challenge of constructing (Either (A -> Void) A -> Void) for different types A.

Let's say you have a positive capability of generating values of type A. This is constructive proof that (A -> Void) cannot exist so you know that any caller of your function will give you (Right value) if they are capable of calling you at all. That's not particularly helpful since you're on the hook to generate an uninhabited type Void, now.

Alternatively, let's say you lack a method to construct values of A. Now either you (a) never get called, (b) get called with a parameter like (Right value), proving to you that values of A exist but asking you to use one to produce a value of type Void (impossible!), or (c) you get a value of type (Left fn), which constructively proves that no values of type A can be constructed.

So in this double-negative formulation, allowing for the potential that you simply never get called, nothing about this LEM-like type is problematic.

But it sure looks close to something dangerous.

---

You can see how this construction works by stripping away the Cont wrapper.

    runCont (cont f) = f
    runCont (cont (\c -> (c . Left) (c . Right))) = \c -> (c . Left) (c . Right)

       \c -> (c . Left) (c . Right)
    lem :: forall a . (Either (a -> Void) Void -> Void) -> Void
    lem c = c (Left (\x -> c (Right x)))

So we see that our callback, discussed above, is always called with a value of shape (Left fn), which appears to be a constructive proof that no values of type `a` exist. It works via a trick, though. If you were to attempt to disprove the statement of that function (a -> Void) by offering it a value of type `a`, that function will just use the value you constructed and hand it back to you as (Right value), forcing you to yourself prove (a -> Void).

This is messy circular logic, but common in this kind of construction. The only way to "construct a value" of Void is to somehow pass the buck and force someone else to do it.

And so this formulation of "LEM" does just what it says on the tin: shows that it's impossible to prove that LEM is impossible. Any such proof can be turned against itself.

moomin3• 3 years ago

I've been very excited about this myself before, but unfortunately, it's something of a stupid trick. The big problem is circular dependencies: they produce infinite loops and there's no particularly good way of detecting them. Regular old catamorphisms with `Either CycleDetected a` are probably a better idea in practice.

hacker_junky• 3 years ago

Can you elaborate on what kind of circular dependencies are you referring to and how would catamorphisms with `Either CycleDetected a` help to reduce those dependencies?

moomin3• 3 years ago

Okay, imagine you've got a list of securities and their underlyers. You've got a flat file that represents this information. You try to represent it as

Security Underlying Security (Security)

Where that's the Security object, not the Security ID.

This works great for moeb, until the day that someone accidentally introduces a cycle. Instead you want a representation that looks like:

Security Either CycleDetected a

You can call traverse to make that `Either CycleDetected Security a`.

Is that making any sense at all?

You rapidly realize that X knows Y and Y knows X.

quchen6• 3 years ago

Worth noting that I wrote this as a result of a discussion on #haskell on Freenode/IRC. I have to say it’s quite (happily) surprising to me that people on HN enjoy it after all those years :-D

bmacho2• 3 years ago

I can't find any source in your post, the loeb function may originate from [0] ?

[0] http://blog.sigfpe.com/2006/11/from-l-theorem-to-spreadsheet...

quchen6• 3 years ago

My source really was people talking about it on #freenode and playing with LambdaBot at the time. There’s a good chance the linked blog post is a transitive source though!

1letterunixname2• 3 years ago

Haskell, Ruby, COBOL, FORTRAN, and MISRA C need a yearly Monty Python "I'm not dead yet" doodle. tcl, Forth, and Squeak... that's enough out of them. Never Expect dejagnu.

cormacrelf• 3 years ago

See also Löb’s theorem: https://en.wikipedia.org/wiki/L%C3%B6b%27s_theorem

Compare Löb’s theorem with the signature of `loeb` with some renaming to make them match up:

in any formal system F, for any formula P, if it is provable in F that "if P is provable in F then P is true", then P is provable in F

    loeb :: Functor f => f (f p -> p) -> f p

To see it even better, look at the section that introduces the modal logic operator (the square that operates on formulae).

See more on the Löb-spreadsheet equivalence here http://blog.sigfpe.com/2006/11/from-l-theorem-to-spreadsheet...

thomastjeffery• 3 years ago

I really dislike the $ operator. If you need to change precedence, use parenthesis.

Does that mean more typing? Yes. Does it mean better readability? Yes.

It's not like you are typing that much code in the first place! The goal of Haskell should not be maximum terseness: it should be elegance.

whateveracct6• 3 years ago

Stacking dollar signs is elegant to me

    f
  $ g
  $ h
  $ some expression etc

bmacho2• 3 years ago

If I'm not mistaken, it reads from bottom to top. I hated the function application direction my whole life, even in math (I read and write from left to right, so f applied to x should be x f, and g after that should be x f g), but it is ridiculously bad in Haskell. Transforming data, filtering and piping should be where it excels due to the lazy data structures, but bottom to top piping order is annoying.

quchen6• 3 years ago

The use here is as a section, not to change precedence: `($ x)` could also have been written as `\f -> f x`, which I think is even less readable.

As for the usage on the lower code snippets like `for […] $ \x -> …`, then it saves some parentheses. Opinions on this go both ways, with some people preferring lisp-style syntax, others use more Python-like indentation code formatting. Both are okay, and I’ve switched my preference multiple times.

Where I agree $ is terrible is in expressions like `foo x . bar y z $ abc`, often (!) much harder to read than just adding parentheses.

ghostwriter2• 3 years ago

Where I agree $ is terrible is in expressions like `foo x . bar y z $ abc`, often (!) much harder to read than just adding parentheses.

This case is actually valuable for the clear delineation of the lefthand-side that's relatively fixed and can be moved to an outer scope (or even toplevel) and the righthand-side that's contextual and is dependent on a more dynamic value-part.

wyager3• 3 years ago

For chains of function applications, `$` is more readable than like 5 nested parens, especially if the thing at the end of your `f $ g $ ...` is a do-block, which will span multiple lines.

quchen6• 3 years ago

My preferred way is `(f . g . h) x`: parentheses have good editor support, are very readable when there aren’t that many.

rowanG077• 3 years ago

I write haskell daily. A well placed $ is MUCH, MUCH more readable then deeply nesting parenthesis.

Y_Y2• 3 years ago

It's just a infix id, there's nothing special about it. You also object to infix + I suppose?

thriftwy• 3 years ago

I really liked $ when I was writing Haskell one-liners because it behaves like a UNIX pipe. You can trivially reason about a system of pipes.

During the same voyage, almost no uses of dot - it might be super elegant when writing complex functions for something else, but not for doing things.

whateveracct6• 3 years ago

I love type signatures like this. Not hard to implement - it's like a game. But then it's like..wtf does this do? And you can kind of guess by reading the type as well as you can the body.

jheriko• 3 years ago

Feeling smart? Lets change that.

No. No you did not.

Thanks for reminding me why academia is a wasteland.

swagmoney1606• 3 years ago

Can you elaborate on what you are saying here? Why is academia a wasteland?

nh23423fefe• 3 years ago

Sometimes people read jokes and they get self-conscious and lash out.

reikonomusha2• 3 years ago

I'll try to elaborate in a productive manner.

More likely than not, the author was just trying to make joke—possibly even self-deprecating. From Haskell programmer to Haskell programmer, this specific joke might even be kind of funny: What's ahead is clearly not "normal" Haskell, and will be quite puzzling at first glance. Haskell has lots of these zingers that Haskell programmers have come to either enjoy or respect. (The "zygohistomorphic prepromorphism" joke is another old one.) The joke being made, while in jest, may also serve to be a sort of hook; the reader may respond internally "I am smart enough!" and proceed to try to crack the puzzle.

However, the joke might feel tone-deaf to the non-Haskell community, and feel absurdly pretentious. To many, Haskell itself is already quite unapproachable. Even with efforts to make Haskell seem like a "normal programmer's language", it still has a reputation for being academic, mathematical, buried in abstraction, and otherworldly. To a non-Haskell programmer, the joke comes across as pretentious: I will show you one simple line of code that I guarantee you are not intelligent enough to understand. It's a joke the author really savors too, since the author spends a couple paragraphs dedicated to it.

The HN crowd is probably one of the best audiences to share something interesting about Haskell, because curiosity is a sort of "core tenet" of the culture here. But I think those who are curious like learning from people who want to share their knowledge with empathy and compassion. Haskell, deserved or not, is so steeped in its reputation of unapproachability—something many HNers are carrying with them into the article—that the final stomp of "you're not smart" is just a perfect way to turn somebody off and away.

I do think that, in this case, the general academic feeling of Haskell is a critical component to understanding why this joke may be a turn-off to many. If it were a goofy piece of JavaScript, where everybody and their dog knows that it's "Bad JavaScript" (TM), it wouldn't have the same feeling of lacking compassion for the reader, I think.

Just my 2¢. :)

quchen6• 3 years ago

FWIW I program my CNC with Haskell, how's that for academic

1letterunixname2• 3 years ago

Unfortunately, it's nothing new. America's mainstream historical ethos derives from a deep anti-intellectual sentiment of an expat merchant class who frowned upon academia and the Old World. The Puritans at least left a positive legacy in Boston, despite generally shunning ideas and people who dared to think differently. The American frontier acted as a risk tolerance filter of peoples from around the world to emigrate. There are systemic problems of economic and policing inequality, and under-socialism in the US.

How does America receive those from distant lands now?

What future does America have without prestigious, selective academic institutions except a brain drain exodus?

love2read• 3 years ago

How hard would it be to describe this in terms of javascript?

lalaithion• 3 years ago

Pretty hard. The key to this implementation is Haskell's laziness, so you have to implement laziness in Javascript, which will probably not be very ergonomic. You can write

    let loeb = (structure => {
      let inner = () => structure.map(item => item(inner()));
      return inner;
    })
  
    let fs = [ _ => 1
             , x => x[0] + 1
             , x => x[1] + 1
             , x => x[2] + 1
             ]
 
    console.log(loeb(fs)())

and get an infinite loop, or

    let loeb = (structure => {
      let inner = () => structure.map(item => item(inner));
      return inner;
    })
  
    let fs = [ _ => 1
             , x => x[0] + 1
             , x => x[1] + 1
             , x => x[2] + 1
             ]
 
    console.log(loeb(fs)())

and get [1, null, null, null].

contravariant• 3 years ago

You can typically simulate laziness by lifting variables into functions. A 0-arity function works fine, but for lists it's slightly more elegant to define them as functions from an index to a value (in that case the functor map is just composition, which is neat).

So the following works

    let loeb = (structure => {
      let inner = (i) => structure(i)(inner);
      return inner;
    })

    let fs = (i) => {switch(i) {
      case 0: return _ => 1
      case 1: return (x) => x(0) + 1
      case 2: return (x) => x(1) + 1
      case 3: return (x) => x(2) + 1
    }}

If javascript was sensible you could just do

    let fs = [ _ => 1
             , x => x(0) + 1
             , x => x(1) + 1
             , x => x(2) + 1
             ].at

but alas that doesn't work, you can do

    let fs = (i) => [ _ => 1
             , x => x(0) + 1
             , x => x(1) + 1
             , x => x(2) + 1
             ][i]

though. In that case javascript may end up rebuilding the list every time, I'm not quite sure.

gowld4• 3 years ago

Python:

  def done(x):
    return (type(x) != type(lambda: None))

  def allof(f, *xs):
    return all(map(f, xs))

  def isnt(f):
    return lambda x: not f(x)

  def myprint(xs):
    print("\t-> ", "\t".join([str(x) if done(x) else "_" for x in xs]))

  def lazy(f, *deps):
    "Evaluate f(xs), only if dependencies (listed by index in xs) are resolved."
    def lazy_f(xs):
      if allof(done, *[xs[d] for d in deps]):
        return f(xs)
      else:
        return lazy(f, *deps)
    return lazy_f

  def loeb_unsafe(fs):
    "Loeb for lists, but doesn't detect dependency cycles."
    xs = fs[:]

    # THE IMPORTANT PART!
    while not allof(done, *xs):
      # 'if done(x) is special for Python: convert function to value, since
      # Python doesn't know how to evaluate/call a value like Haskell does.
      xs = [x if done(x) else x(xs) for x in xs]
    return xs

  def loeb_safe(fs):
    "Loeb for lists, stops when it detects a dependency cycle."
    xs = fs[:]

    # THE IMPORTANT PART!
    while not allof(done, *xs):
      myprint(xs)
      # 'if done(x) is special for Python: convert function to value, since
      # Python doesn't know how to evaluate/call a value like Haskell does.
      new_xs = [x if done(x) else x(xs) for x in xs]
      if list(filter(done, new_xs)) == list(filter(done, xs)):
        print("CYCLE DETECTED!")
        break
      xs = new_xs
    return xs

  fs = [
    lazy(lambda xs: xs[1] + xs[2], 1, 2),
    lazy(lambda xs: xs[3] + 1, 3),
    lazy(lambda xs: xs[1] + 1, 1),
    1,
    lazy(lambda xs: xs[5] + 1, 5),
    # unsafe!
    # lazy(lambda xs: xs[4] + 1, 4),
    lambda xs: 100,
    200
  ]
  
  print("safe:")
  myprint(loeb_safe(fs))
  print("\nunsafe:")
  myprint(loeb_unsafe(fs))

Output:

  safe:
    ->  _   _   _   1   _   _   200
    ->  _   2   _   1   _   100 200
    ->  _   2   3   1   101 100 200
    ->  5   2   3   1   101 100 200

  unsafe:
    ->  5   2   3   1   101 100 200

Löb and möb: strange loops in Haskell (2015)

Related Stories