[HN Gopher] Lob and mob: strange loops in Haskell (2015)
___________________________________________________________________
Lob and mob: strange loops in Haskell (2015)
Author : hjnkk
Score : 127 points
Date : 2023-01-30 11:29 UTC (11 hours ago)
(HTM) web link (github.com)
(TXT) w3m dump (github.com)
| whateveracct wrote:
| 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.
| thomastjeffery wrote:
| 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.
| whateveracct wrote:
| Stacking dollar signs is elegant to me f
| $ g $ h $ some expression etc
| bmacho wrote:
| 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.
| nimih wrote:
| The & operator in Data.Function--which is just flipped $
| with slightly higher, but still very low, operator
| precedence--at least gives you a way to deal with this in
| base; it's unfortunate it isn't more widely used in
| tutorials and example code (at least from what I've seen).
| azurelake wrote:
| You can use `>>>` from `Control.Arrow` to switch the order
| if you don't mind make your code more esoteric.
| whateveracct wrote:
| Control.Arrow is in base at least :)
| whateveracct wrote:
| I prefer it, personally. Especially when pointfree. Way
| easier for me to read at a glance.
| thriftwy wrote:
| 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.
| rowanG077 wrote:
| I write haskell daily. A well placed $ is MUCH, MUCH more
| readable then deeply nesting parenthesis.
| quchen wrote:
| 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.
| ghostwriter wrote:
| > 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.
| wyager wrote:
| 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.
| quchen wrote:
| My preferred way is `(f . g . h) x`: parentheses have good
| editor support, are very readable when there aren't that
| many.
| wyager wrote:
| That's good too, but you still need one $ for a do block.
| whateveracct wrote:
| Not with -XBlockArguments you don't :)
| Y_Y wrote:
| It's just a infix id, there's nothing special about it. You
| also object to infix + I suppose?
| love2read wrote:
| How hard would it be to describe this in terms of javascript?
| lalaithion wrote:
| 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 wrote:
| 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.
| ktpsns wrote:
| tl,dr; (extracted from the article itself)
|
| > In a sense this is like a generalization of a fixed point
| combinator.
| moomin wrote:
| 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 wrote:
| 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?
| moomin wrote:
| 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.
| Y_Y wrote:
| Can you detect cycles in general though? At first blush it
| feels like a halting problem.
| chowells wrote:
| You can't detect all possible cycles statically, but you
| can definitely detect them when they happen at runtime.
| When calculating a value, track its dynamic dependencies.
| If it ends up depending on itself, you have a cycle.
| chpatrick wrote:
| Another weird type signature is: excludedMiddle
| :: Cont c (Either (b -> c) b) excludedMiddle = cont $ \c ->
| (c . Left) (c . Right)
| platz wrote:
| why is it weird; a breif description of the observation would
| be helpful
| chpatrick wrote:
| 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).
| platz wrote:
| Cont r a
|
| is a CPS computation that produces an intermediate result
| of type "a", within a CPS computation whose final result
| type is "r"
|
| In your example of type "Cont c (Either (b -> c) b)", it
| produces a final value of type "c". (There is no Either in
| the final result, i.e. there is no "excluded middle")
|
| It produces an intermediate result of type (Either (b -> c)
| b) by feeding values through Left and Right constructors,
| calling the continuation multiple times, once for Left and
| once for Right.
|
| I don't see what you mean by "thin air" because the Left
| and Right constructors in the definition are creating the
| Either, first creating the Right, and then feeding that
| result to the Left.
|
| If you think the (Either (b -> c) b) is the final result,
| then you don't understand or are misrepresenting the
| meaning of the definition of Cont r a
|
| (don't make the mistake of thinking the final result is of
| type "a". it is of type "r")
|
| There is no excluded middle here. It just uses the Either
| as a way to encode & pass 2 different functions to the
| continuation.
|
| The naming of the function as "excludedMiddle" is
| disingenuous.
| chpatrick wrote:
| Actually I called it that because it's derived from the
| law of excluded middle: "A OR not A" is always true.
|
| You can encode logical statements in the Haskell type
| system as follows: a OR b: Either a b
| a AND b: ( a, b ) not A: a -> Void
| a implies b: a -> b
|
| With this encoding, having a well-formed value for a
| given type is a proof of its validity.
|
| The one thing we can't use directly is double negation,
| because we would have to make A appear out of nowhere:
| ((a -> Void) -> Void) -> a
|
| However, this is exactly the type of Cont Void. This
| means we can use the Cont Void monad to make logical
| proofs, including double negation. The type:
| Cont Void (Either (a -> Void) a))
|
| Encodes the law of excluded middle, and the value I wrote
| is a proof of it. It so happens that you can use a type
| parameter instead of Void because an arbitrary type can
| also not be used for anything.
| hgsgm wrote:
| Are you saying it's weird that a function has an explicit
| type in Haskell? ("First-class" functions)
|
| https://en.m.wikipedia.org/wiki/First-class_function
| mrkeen wrote:
| You can read those lower case letters as preceded by "for
| all", and it's up to the caller to choose which concrete
| type the letter should represent, as the function
| promises to return an implementation "for all" concrete
| types.
|
| So if wrote the function foo, foo ::
| Int -> b
|
| and you happened to need a BufferedReader, you could just
| get it by calling (foo 3). That's what the "thin air"
| comment is. Where could the implementation of
| BufferedReader possibly have come from?
| tel wrote:
| 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.
| quchen wrote:
| 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
| bmacho wrote:
| 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...
| quchen wrote:
| _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!
| cormacrelf wrote:
| See also Lob's theorem:
| https://en.wikipedia.org/wiki/L%C3%B6b%27s_theorem
|
| Compare Lob'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 Lob-spreadsheet equivalence here
| http://blog.sigfpe.com/2006/11/from-l-theorem-to-spreadsheet...
| jheriko wrote:
| > Feeling smart? Lets change that.
|
| No. No you did not.
|
| Thanks for reminding me why academia is a wasteland.
| quchen wrote:
| FWIW I program my CNC with Haskell, how's that for academic
| [deleted]
| swagmoney1606 wrote:
| Can you elaborate on what you are saying here? Why is academia
| a wasteland?
| reikonomusha wrote:
| 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 2C/. :)
| ghostwriter wrote:
| > However, the joke might feel tone-deaf to the non-Haskell
| community, and feel absurdly pretentious. [...] 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.
|
| How's that different to a humorous
| basketball/hockey/football dribbling demonstrated by a pro-
| player on a youtube video for their audience's awe and
| admiration? I bet no one is treating it as "pretentious" at
| those moments, in fact many of the younger folks regularly
| get inspired by this kind of performances to start in the
| sport.
|
| These types of depreciating and other-party-blaming
| comments tend to come from ego-offended senior developers
| who're used to thinking that they can always pick a new
| programming language in 20 minutes or so, because all of
| them resemble their favourite flavour of $java (not
| really).
| reikonomusha wrote:
| I think the critical difference is that said basketball
| player doesn't open their demonstration by challenging
| the audience's intelligence explicitly.
|
| I don't want to personally say whether the joke in the
| article is in good taste or not, and I don't want to
| assess whether programmers' egos are too fragile or
| sensitive. I don't think that's productive.
|
| I do, however, want to emphasize that when read by a
| broader audience than just the community of Haskell
| programmers, due in part to Haskell's reputation, the
| joke lands as off-color, as the G*P comment demonstrates.
| klabb3 wrote:
| This is extremely well put.
|
| I think the curse of knowledge is at work in both with
| monads and C preprocessor hacks, they both make sense only
| within a domain-specific context - if you're living and
| breathing in that context, you can appreciate the
| techniques. At the same time, if you never step outside you
| can forget that programming is a tool for humans, and think
| that your tools, systems and languages are infallible.
| nh23423fefe wrote:
| Sometimes people read jokes and they get self-conscious and
| lash out.
| mrkeen wrote:
| Easy fix - just read the reply charitably as well. Now you
| have two jokes.
| lynx23 wrote:
| > Feeling smart? Lets change that.
|
| Great quote, I gotta remember that.
___________________________________________________________________
(page generated 2023-01-30 23:00 UTC)