Comment by zoogeny | Hacker News Reader

Comment by zoogeny | Hacker News Reader

I like that things like this exist even if I recognize that they are not for me. For some class of system I am sure these languages will shine. It reminds me of Julia - every time I come across it I love the idea of it but I have no personal use for it. I'm always interested in reading articles on dependent type languages like Coq and Idris but I haven't even tried to write a "Hello, World!" in them.

I may just be jaded with promises of sufficiently smart compilers. I actually hold out more hope for AI code assistance than I do for easy-to-use formal verification.

It is a bit like Esperanto or something like that. Maybe I am just brain damaged from growing up in a world with English and other messy spoken languages but my intuition suggests that perfectly structured languages are possibly the wrong approach.

Even though at the time I wanted xhtml to win the battle of structured formats for the web, in hindsight I now believe messy html 5 was the way to go.

> We still get buffer overflows and integer overflows. The compiler still cannot tell when our loops will terminate (yes, this is possible). Aliasing is still a complete unbridled mess.

As strange as it sounds, I've learned to love the flaws. I don't see my job in life is to remove every possible source of error. There seems to be a balance point where the cure is worse than the disease and I wish to find that balance point rather than some theoretical perfect.

So I do hate those things listed. But so far, the balance point for me is with languages that sacrifice perfectly solving those problems.

Highly regular natural languages exist and thrive. I'd say that Japanese is a way, way more regularly structured language than English.

Loving flaws like buffer overflows looks more like a Stockholm syndrome to me: when the reality is terrible, people learn to find lovable bits in it, just to avoid insanity. C has its place, but its place is very, very close to hardware. (And I hope Zig will push it from there, too, eventually.)

I don't think that better static guarantees are going to come from direct adoption of languages like Haskell, or some tools like Coq or Agda. They will continue coming the same way Rust and Typescript gone mainstream: by integrating them into practical (not research) languages, and allowing escape hatches, prominently marked. Advanced features need adaptation to be ergonomic, after that they feel natural. This happens to every scientific achievement that has a large practical value: compare a laser on an optical workbench in a lab to a laser in a DVD drive, or a laser pointer.

I would likely laugh if someone told me in 1995 that pure FP approaches will conquer GUI development. Nevertheless, this happened twice: first with XSLT in 2000s, then with React in 2010s.

react is not an example for a library that is supposed to be or even possible to be used in a pure functional programming way.

Right, there's definitely functional-inspired bones (e.g., a view is a function of state); but every hook is a side effect, even the redux ones.

And I don't think it would even be improved by being pure; Elm has much more boilerplate to do similar things.

haha, Adam from SM, is it you?

React can still be viewed as functional programming if you assume Hooks operate in/on/with an unnamed/untyped monad. ("Pure" of course depends on your take of monadic programming from there.) It might be nice if that monad were better typed and/or at least parametric (reflected in input or output parameters), but it all exists in an untyped language to begin with, so it is mostly fine how it works right now. Mostly.

I don't know. I haven't used hooks much, but while you might consider it pure-functional in a way within a component that uses (a single) hook, I think using multiple hooks and having everything integrated is certainly not pure-functional.

It's easy to test right? Can you replace calls/expressions with their result-value? If no, it's not pure-functional.

Like I said, I don't think it counts as "pure" functional because it is heavily monadic. Many Haskell users still think non-monadic code is "more pure" than say anything that uses the IO Monad and Hooks are "worse" than the IO Monad. (Especially some of the "Suspense" project Hooks which combine IO and Futures and State and more from a Haskell standpoint into one super weird monad.)

You can certainly replace most hooks with static return values. Many hooks are heavily memoizable and in turn heavily memoized which is how they find their performance in practice.

Multi-hook interactions generally follow a lot of the laws of monadic binding and a lot of the "hooks rules" aren't that strange in terms of monads: monadic binds have sequencing that matters (and dependencies you might track). The order of hooks matter in the same way that the order of IO binds or the order of Futures/Promises awaits.

Again, it is certainly hard to call it "pure" functional in most ways, it has a lot of impurity, but it is certainly "deeply" functional. There's not really a better paradigm to call what is React is doing with Hooks than "functional programming". The language of monads is somewhat helpful in reasoning about how Hooks work and where they sit in the paradigm. They definitely make everything a bit more "impure", especially from the strict mathematical sense of "pure functions are entirely dependent on their parameters". Especially with Hooks not being represented parametrically (which I did mention I think can be something of a problem and I wish wasn't the case).

> You can certainly replace most hooks with static return values.

"most" is not good enough. The idea of PFP is precisely that there is no exception, otherwise all guarantees are void. If I cannot rely on an expression to be referential transparent, then it means I have to look into to find out - and with that, the advantage of PFP goes through the window.

> The order of hooks matter in the same way that the order of IO binds or the order of Futures/Promises awaits.

The difference is that if you create an effect in a PFP style (like in Haskell), the effect itself doesn't do anything. You can now combine that effect with another effect in some way, e.g. by sequencing, which means first effect A and then afterwards effect B is executed. Yes. But what you get back is, again, an effect that doesn't do anything. So what you need to do is to build a datastructure of effects.

Do you do that with hooks? I don't think so. With hooks, you call one, then call another, and yeah, the result depends on the order just like with an effect monad like IO. But the difference is that once the line of code that calls the hook is executed, something happens and the world has changed. This is not true when you can the line of code that builds the datastructure for the effect execution.

You would have handle hooks like promises for this to work in a PFP way. But maybe I misunderstand and you can clarify it with a code example?

Otherwise, I just think it's about terminology. I agree that there is a relation between the two things, but we shouldn't give it the same name, because it is still not the same concept.

Hooks definitely build a complex data structure. They don't actually run immediately/imperatively. Even `useEffect(callback, undefined)` (no defined dependencies) which gives the illusion that it runs "immediately" on every render is still an illusion of sorts and there's a complex scheduler apparatus feeding on the data structures under the hood that useEffect builds.

The data structures that Hooks build in React gets built in a strangely bound, somewhat liminal `this` space so it effectively "disappears" in JS. That's certainly not how I would have built it. You are right that I probably would have used something more like JS Promises, given the choice. But I didn't build React's Hook systems, I'm just an outside critic. I'm very happy to agree that use of `this` bound things is about as impure functionally as you get in JS. (That said, it is a very JS solution that predates React and gets to old debates of whether or not JS is truly "OO". Prototypical OO is a gray space between OO and functional paradigms.)

Hooks are never imperative, even in the most complex multi-hook components. They use and build data structures. Those data structures are mostly hidden from view and hard to inspect, but they exist.

> Hooks definitely build a complex data structure

But you don't. It is react that builds the datastructure in the background, not you that builds and controls it. Hooks might be declarative, but this is actually orthogonal to being pfp or not.

All of that is totally fine btw., there is no need for everything to follow a pfp style. It's a tradeoff. But we shouldn't call something pfp that isn't, even if it is closely related.

Look, you have a large stream of pure functions that exchange immutable data. There is a place where you can thread in the effects, and it's not entirely like using >>=, but after it, it's immutable data and pure functions again.

It's very different from jQuery and the callback hell, or from any two-way bindings all the way to Visual Basic.

It teaches you to value immutability and purity, to crave it (then comes Ramda, etc).

Also, Promises are not entirely monadic, and `async` is not entirely the do-notation, but you can use a lot of monadic approaches, and reap some of the benefits.

> and it's not entirely like using >>=

Exactly, and that's why it is not pf. It's really as simple as that.

It's also not as if it would be theoretical distinction that has no meaning for praxis. It does. For instance, since I cannot control the execution of React's cycle (including rendering) it becomes hard(er) to do certain kind of page animations that should happen between renders.

> It's very different from jQuery and the callback hell

Yes, it is nicer to use. But it is not pfp-style.

What would you suggest as a pure enough example of FP GUI? Anything besides Elm, I mean? :)

I have never worked with one professionally (I rarely do frontend work anyways) and for my own projects I used react, dirty and productive as it is. ;)

JavaScript has never been and probably never will achieve any sort of purity due to the design decisions made in its debut. Frameworks can only paper over that so much.

I mean, there are fp-ts and ts-effect. Sure, internally they do nasty things, but at least as a user I think it's possible to write pf or at least mostly pf code. (without commenting on whether that is a good idea or not)

You can actually type JS to be incredibly more strict than TS does if you have the motivation. It still won’t be impossible to reach runtime errors, but it can be very close to “you really have to try and mean it”.

Funny enough, Japanese is incredibly fun and enjoyable when you use dialects and break the syntax to be "artsy"

But even that does not increase the number of irregular verbs past two and a half (くる, する, ありえる). I don't know enough Japanese to say if one can invent forms like "swole" or "boxen" in it, so that they would remain recognizable.

Archaisms, slang, and alternate pronunciations definitely exist in Japanese. And dialects, of course.

You can invent a lot of things in written Japanese using textspeak and other alphabets.

Spoken Japanese you can't break the rules because everyone else instantly becomes unable to understand you. They barely use local accents/dialects in media because of this.

> Loving flaws like buffer overflows looks more like a Stockholm syndrome to me:

Only if you are the developer (victim ) it is fun to work with buffer overflows if you are the security researcher (law enforcement) or a hacker (kidnapper )

It's funny that you picked the language with the single worst and most fundamentally broken orthographic system in the world as your example.

> It is a bit like Esperanto or something like that. Maybe I am just brain damaged from growing up in a world with English and other messy spoken languages but my intuition suggests that perfectly structured languages are possibly the wrong approach.

You seem to be implying Esperanto's lack of popularity is related to its regularity, but I don't think it has anything to do with that - it comes down to network effects. It's not an official language in any country. There are very, very few native speakers of Esperanto. Of those blessed few, they obviously have at least one other native language, otherwise they'd be completely cut off from society.

And by the same token, English is popular as a second language due to network effects and the benefits learning it can confer (read: better economic opportunities) and little to do with its regularity. A lot of people have had the experience of learning a bit of Spanish and realizing that English's spelling system is atrociously irregular and we gain nothing by having so many spelling rules that have so many exceptions they can hardly be considered "rules". In fact, English's spelling used to be much more regular, it's just that our pronunciations have shifted a lot over time while the spelling has remained relatively static.

This is all tangential to your larger point, I just like talking about this kind of thing.

The dependent languages are interesting. But the theorem proving is not easy, and probably overkill for a lot of applications. Even for stuff like boundary conditions for binary search, which could be checked with Hoare logic, I usually handle by stealing the implementation from the Go standard library (so I don't have to think about it).

Last year I did advent of code in Lean4. I had written a heap implementation that I didn't end up using. As an exercise, I went back and added proofs for my indicies and a termination proof. I got the termination proof down to `0 < 0` and realized that I had an off by one error (I'd used the math for a 1-based array with a 0-based array).

My take-away was that this stuff can catch real bugs, but also that people are not going to do this stuff day-to-day. Maybe some equality saturation thing will make it possible for the compiler to sort out the proof in most cases. If the compiler can hit 80%, you could use it as a linter. (If you want something stricter, you can do totality checking but have escape hatches like Idris' assert_total / assert_smaller.)

> Even though at the time I wanted xhtml to win the battle of structured formats for the web, in hindsight I now believe messy html 5 was the way to go.

The structured vs unstructured thing is also interesting. I came to a similar conclusion years ago. I'd written some heuristics to pull recipes out of web pages, and also use embedded microdata on some pages. I found I got better results with my heuristics because of bad encoding of the structured data. E.g. a web site was missing entire ingredient blocks in their encoding because their process / data model didn't accommodate recipes with multiple ingredient blocks.

>The compiler still cannot tell when our loops will terminate (yes, this is possible).

    while(n < busy_bever(10))
        n++

Tell me when my loop terminates.

That's not a very good exemple because with BB we know the code terminates, by definition. The canonical tong-in-cheek argument is to use the Collatz conjoncture instead (but even that isn't a good example in practice: https://news.ycombinator.com/item?id=21440306)

I'm not asking if it terminates, I'm asking when it does. After all it's not much use if the number overflows the universe.

But that's not something these kinds of tools are supposed do, even with trivial functions… These tools have no idea about the run-time (and there's no way they coule, since it depends on the load you put on the hardware in parallel of running your program)

I agree. There are tools though which are specifically for determining worst-case execution time for e.g. embedded systems which can actually give accurate timing information (upto a point).

Yeah, so these tools will not tell you how long it will take to terminate --- only that it will eventually. In the vast majority of cases, that is what you want to know.

For practical reasons, it's enough to prove that it takes longer than some upper bound, say, 10 ms. The rest is not important.

    while(calculate_pi_stream(10 /* substring length */) != 0987654321);

Haha, yeah ... this one you would have a very hard time with :)

Hopefully, though, termination of your program does not depend on this ... otherwise could be a long wait!

I remember there was a theorem that one can find an arbitrary substring in a long enough output of infinite (stationary) random process. I also suppose that a decimal representation of pi may count as one, then your function provably terminates.

But this is of a theoretic interest. In practice the verifier says: "I can't prove that this function will terminate within (some reasonable window), program rejected". And this is what's actually needed: a program that provably has certain properties, where an automatic proof is tractable.

It is currently not known whether π is a normal number (that is, its representation in any base contains any finite sequence of digits with the same density as in a uniformly random string of digits).

> Tell me when my loop terminates.

I think the point is that even though one can't determine loop termination for all loops (easily provable), there are a huge number of useful loops that do useful work and for which you can prove properties like termination (and other static properties).

> there are a huge number of useful loops that do useful work and for which you can prove properties like termination

Exactly! If the loop doesn't terminate, then you obviously cannot show it. But if it does, then you should be able to (even if that requires some changes to help the tool)

> If the loop doesn't terminate, then you obviously cannot show it.

I don't think this is true for all loops either - some can be proven to never terminate, just like some can be proven to terminate. And some can't be proven either way.

Yeah, ok that’s fair enough!!

Assuming you meant 'busy_bever' to implement the busy beaver function, said function is in fact not a computable function, which means you can't write it down in a programming language.

This is true but somewhat misleading. The nth busy beaver numbers are known for n <= 4. It's within the bounds of possibility that we will some day learn the nth busy beaver numbers for n <= 10. (What we can say is that the parent's loop will never terminate for any known definition of "ever" that pertains to the physical universe.)

Reply on news.ycombinator.com