Hacker Newsnew | past | comments | ask | show | jobs | submit | steego's commentslogin

You can think of a calculus as a mathematical system one can use to define the essential computational basis for how a programming language or a runtime works mathematically.

Lambda calculus is often the foundation for functional programming languages, but lambda calculus is also a mathematical system you can calculate things with pencil and paper.

What makes lambda calculus interesting is it’s a relatively simple mathematical system where EVERYTHING is defined as a function. I’m serious. Imagine a programming language where you don’t have numbers, bools, if statements, while loops, gotos, etc.

You only have functions. All functions accept one argument (a function) and they always return functions.

Tree calculus is like lambda calculus, but it takes the idea a bit further. Not only can tree calculus do all this stuff where you create functions from other functions, tree calculus is fundamentally capable of reflecting on itself in a way that allows it to easily understand and transform its own interpreter.

In other words, if you base a programming language on tree calculus, your programming language or interpreter will allow you to create programs that can reflect on and transform other programs just like it was any other piece of data.

It’s pretty remarkable, especially when you find out how simple a core tree calculus based language can be implemented.


This introduction to this paper explains the motivation:

https://dl.acm.org/doi/pdf/10.1145/3704253.3706138

Tree Calculus is an alternative to lambda calculus that is capable of doing meta-theory without having to construct or bolt on something else entirely.

If lambda calculus provides a theoretical foundation for a language like Lisp. Tree calculus provides a theoretical foundation for a Lisp with a macro system that is fundamentally part of the core calculus.

You don’t have to write parsers and other stuff to do meta programming. It’s fundamentally built in and the paper I posted above explores how to construct type systems as a library, not as something that is outside of the runtime environment.

Here’s what’s really cool about it too: Just like lambda calculus, you can evaluate tree calculus with pencil and paper.

It’s very slick.


For people wondering what this is and whether to take this seriously, I’ll try to provide some context:

Tree Calculus is a novel alternative to lambda calculus as a minimal model of computation. Unlike most minimal systems, tree calculus is fundamentally capable of being fully reflective.

If you were ever interested in creating a programming language that could fully reflect and enhance itself with libraries, this is one of a very few number of known minimal system you can use as a starting point. Think of it as a lambda calculus with macros built into the underlying calculus, not something bolted on afterward based on a partially implemented meta-theory.

If you’re into formal proofs, you can find Rocq proofs of his work in his repo.

https://github.com/barry-jay-personal/tree-calculus

If you’re interested in how something like tree calculus can express a type system, here’s a recent ACM paper:

https://dl.acm.org/doi/pdf/10.1145/3704253.3706138

Personal context, Barry Jay is a respected academic and researcher who’s collaborated with people like Simon Peyton Jones and Eugenio Moggi. His PhD advisor was Joachim Lambek (from the Curry-Howard-Lambek correspondence). He’s not a random professor with a neat toy, Barry’s been working with many of the best minds on the foundations of computation long before most of us knew category theory existed. He’s been formalizing and defining pattern matching, higher-ordered patterns and has been searching/separating what is truly essential from what is not essential for decades.

Seriously, look at his research history on Google Scholar.

I think it will take the rest of us a while to understand and unpack the insight he’s already imbued into such a small and simple calculus.


I think people MOSTLY foresee and anticipate events in OUR training data, which mostly comprises information collected by our senses.

Our training data is a lot more diverse than an LLMs. We also leverage our senses as a carrier for communicating abstract ideas using audio and visual channels that may or may not be grounded in reality. We have TV shows, video games, programming languages and all sorts of rich and interesting things we can engage with that do not reflect our fundamental reality.

Like LLMs, we can hallucinate while we sleep or we can delude ourselves with untethered ideas, but UNLIKE LLMs, we can steer our own learning corpus. We can train ourselves with our own untethered “hallucinations” or we can render them in art and share them with others so they can include it in their training corpus.

Our hallucinations are often just erroneous models of the world. When we render it into something that has aesthetic appeal, we might call it art.

If the hallucination helps us understand some aspect of something, we call it a conjecture or hypothesis.

We live in a rich world filled with rich training data. We don’t magically anticipate events not in our training data, but we’re also not void of creativity (“hallucinations”) either.

Most of us are stochastic parrots most of the time. We’ve only gotten this far because there are so many of us and we’ve been on this earth for many generations.

Most of us are dazzled and instinctively driven to mimic the ideas that a small minority of people “hallucinate”.

There is no shame in mimicking or being a stochastic parrot. These are critical features that helped our ancestors survive.


> We can steer our own learning corpus

This is critical. We have some degree of attentional autonomy. And we have a complex tapestry of algorithms running in thalamocortical circuits that generate “Nows”. Truncation commands produce sequences of acts (token-like products).


They do.

I suspect that you are not only ignoring the existing safeguards that have already come of those discussions, but I suspect you’re also ignoring or pretending like those public discussions never happened in the first place.

Furthermore, I suspect you’re also trivializing what is and is not in contention with moral issues as these companies are trying to compete against each other.

I also think you’re probably assuming the slower options are the safer options because you haven’t really considered the risks of ceding power/investment to a less scrupulous competitor.

I’m not claiming any of these men are moral upstanding people or that they’ve done enough.

I think people should be very critical, but they should at least make the effort to ENGAGE in the moral issues and consequences.

Your cheap four word response only adds cheap rhetoric to the conversation.

If you really care about the moral issues, start typing.


Expressiveness tends to become a liability when the benefits of the expressiveness aren’t clear.

Dafny’s expressiveness tends to be more in the service of coherent specifications and less in the service of language abstraction for its own sake.


After watching a bunch of people use the live chat, I am not discouraged by live chat anymore.

I actually think one can make it work, one simply needs to account for moderation and flooding upfront.

The first feature you need is a way to instantly ignore people who are ruining the collective experience. I would think when a person is ignored by a certain threshold of people, their content should automatically be moderated.

The second feature that’s needed is some sort of flood protection or detection. If a user is pasting or trying to flood the chat with characters, they should be instantly hidden and their content be subject to moderation. Being able to distinguish between copying and pasting on occasion and flooding goes a long way.


The recently sunsetted Reddit public chat was a good example. They were tied to a subreddit, so only people with some shared interest came together. And the moderators could set an entry barrier based on karma. And you stood to lose your reddit account if you misbehaved in a public chat


I understand and appreciate Reddit’s approach.

On the other hand, I think there might be a way to solve this problem for live anonymous chat in a way that doesn’t rely on threats of “punishment” or “banning”.

I think most people looking at this problem don’t appreciate how much realtime information can be calculated from the event stream and how that information can be leveraged toward solving it in near realtime.


Why does people care if their Reddit account is banned? I've never understood this. Can't you just open a new one?


Replace “reddit” with “google” in your sentence. Now how does it sound?


Like you're talking about something completely different in function and purpose.


Not for quite a lot of people it isn’t, no.

I’m guessing you’re over 35 (as I am).

I know plenty of people in their 20s whose entire online life is centered on Reddit.

They make hundreds of comments a day. It’s where all of their social interaction is. it’s where they coordinate activities with people. It’s where they chat with people. it’s how they communicate with everyone.Losing that handle would be disastrous. You can’t just change it.


> The first feature you need is a way to instantly ignore people who are ruining the collective experience. I

Yeah, and we all know you're talking about Anon Pond Heron, lets be honest.


I am.

While I’m not the kind of person who races to test the most triggering racial slurs, I’m actually glad Anon Pond Heron did because I thought his behavior was informative, especially as you could watch him slowly type out the beginnings of a slur.

I actually think these types of CRDTs can be enhanced with a handful of simple mechanisms to ensure a higher quality chat experience.


Aren’t we being a little sensitive?

The OP didn’t say all of the reasons for male related injuries were needless, but if you look at the list, it’s dominated by activities that are inherently voluntary and risky.


aren't you being a little naive by calling dangerous activities men have to take to survive "inherently voluntary"? go to a 3° world country or works as an immigrant somewhere rich to check your options. transportation included. it's easy to say one shouldn't use a cheap motorcycle and go for the one way sardine packed 2 hours bus ride across the city to reach work, everyday


Only 3 out of 18 reasons on that list are work-related, 2 maybe can be work related (lawnmowing and powered tools/household machinery?). I think cycling accidents (5 positions on the list) are in part normal cycling (like when riding to work) without rider's fault, and in a larger part taking unnecessary risks while riding, or riding for sport. And I'd guess motorcycle accidents (4 on the list) are mostly taking risks and riding too fast. 3 reasons are "assault". And that leaves only 1 reason from the list, sports equipment.

So out of 18 reasons on the list, only a small part is "activities men have to take to survive", but many of the others aren't "inherently voluntary and risky" or cannot be blamed on the hospitalized person. The list is too short to be really interesting, when half of that list is the same thing with small variations (cycling/motorcycling), and the same for women (mostly pregnancy).


This data reflects the UK, not a 3rd world country and my comments are restricted to this dataset.

Included in that same dataset are assaults and sports related injuries, which are additional risky activities.

You might argue assaults aren’t voluntary. My personal experience suggests most assaults are the result of voluntary activity rather than involuntary activity, YMMV.

I’m not being naive. I have lived in a 3rd world country where it wasn’t uncommon to see a family of 5 on a motorcycle.

I would note that you will tend to see, proportionately speaking, more women on motorcycles in those countries for the reasons you suggested.


Honestly, if you build transit, developers will build.

I wouldn't call it "building a city", but if you look at Northern Virginia today, you'll find that vertical districts are popping up along the Silver Line metro that now extends past Dulles airport.

At the end of the metro, there is literally a "town center" residential area on one side with buildings around 5 stories tall. On the other side of the tracks is literally fields, but the roads have been laid out like Sim City with empty plots and developers are now beginning to construct buildings starting from the outside perimeter first, working their way toward the metro station.

Throughout the DC suburbs, you will find densely populated areas with relatively tall vertical buildings (15-20 stories) that simply were not there 20 years ago. Reston is a good example. I've watched 4-6 buildings (over 10 stories) get built in Reston alone. They mostly started when the the metro line was finished.


tysons is a good example as well. I always think the development of the DC metro is some of the most impressive in the sense of 'cities' popping up along the train lines.

I haven't travelled the entire country but I've never seen anything quite like Silver Spring, Bethesda, or as you say, Reston. Super interesting.


If I had Musk or Bezos levels of wealth my middle-age retirement project would be buying a million acres somewhere and playing real life SimCity.


The Github user doesn't even exist.

Who writes Lean code in the actual paper but doesn't create a repo or even a username?


Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: