Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Yon – a topos-oriented language with a content-addressed lattice heap

yon-lang.org

Post reply on HN
Print view View original

51–60 of 93 posts

Re: Yon – a topos-oriented language with a content-addressed lattice heap

#51

Post by itishappy »

danieltanfh95 wrote: post #35
jrmg wrote: post #5

Just a comment: this sounds a lot like when someone I knew mildly succumbed to AI psychosis, and thought he, with Gemini, had made some physics/metaphysics breakthrough. If you’re losing sleep and feeling distressed or euphoric, maybe lay off for a few days, no matter how hard that is. Talk to friends and/or family about unimportant things. Get outside for a while. Go back to old hobbies (reading, hiking, just going…

There is nothing physics/metaphysics about this. If you don’t understand the terms, don’t pretend you do and write slop as a comment, it is really not that different from using LLM to generate slop.

The parent comment is not suggesting that Yon is about physics/metaphysics.

Understanding is important for readers. Demonstrating understanding is important for writers of both technical documentation and internet comments, and of critical importance in the era of AI.

Re: Yon – a topos-oriented language with a content-addressed lattice heap

#52

Post by ModernMech »

TimorousBestie wrote: post #47
canyp wrote: post #29

> Content addressing is extensionality made physical (chapter 11) Actually, that's in chapter 12; 11 is the standard library. Maybe the LLM got confused because the chapters are 0-indexed. I was curious about that topic but it seems over my head. I don't think it works outside of mathematics? In programming, one can have two objects that are identical in both structure and value but have different identities. It's wh…

> Why does the handle need floating point? I don’t know if Yon does this (the documentation is gibberish) but it’s possible to use f64 NaNs to hold convenient metadata. I had a professor who wrote a bespoke teaching language (roughly based on Scheme) that did that.

Here's an implementation of such: https://docs.rs/nanval/latest/nanval/

Re: Yon – a topos-oriented language with a content-addressed lattice heap

#53

Post by z4lis »

ModernMech wrote: post #49
Syzygies wrote: post #40

Earlier quoted context omitted.

As a mathematician, this reads to me as the most informed comment. Various priors inoculate me from feeling some of the rejection expressed in other comments. I knew Sammy Eilenberg, perhaps the most famous mathematician to work at Columbia University. He hired me. With friends, I ran into him one night out in NYC, and in his 70's we all stayed out past dawn. His late career focused on topos theory, and everyone in t…

Rapid prototyping was always possible in PL design. It was very possible to go from idea to a working proof of concept language with a couple weeks' work. There are thousands of POC projects like this that popped up before LLMs existed. What LLMs are doing now is allowing people to take prototypes and to publish them with an entire 200 page book no one (not even the author) has read, and a polished-looking website fi…

Yeah, early on in my evaluation of this thing was to check out the contributors and their work. Was expecting this to be the product of at least a small group. Imagine my surprise to see… one person…

Re: Yon – a topos-oriented language with a content-addressed lattice heap

#55

Post by canyp »

ModernMech wrote: post #52
TimorousBestie wrote: post #47

Earlier quoted context omitted.

> Why does the handle need floating point? I don’t know if Yon does this (the documentation is gibberish) but it’s possible to use f64 NaNs to hold convenient metadata. I had a professor who wrote a bespoke teaching language (roughly based on Scheme) that did that.

Here's an implementation of such: https://docs.rs/nanval/latest/nanval/

I still don't get what is the advantage over an unsigned integer. Yes, fp64 has unused bits. But why are you going to involve the FPU at all when a uint64 does the trick as well? Plus with a uint64 you get all the flexibility of what bits to dedicate to the address vs metadata.

Edit: I guess one advantage is that, if we later treat the handle like a pointer, NaN math gets you NaN again, whereas the uint64 math might get you an invalid address, or you'd need extra logic to check that the uint64 is not a valid handle?

Re: Yon – a topos-oriented language with a content-addressed lattice heap

#56

Post by ModernMech »

canyp wrote: post #55
ModernMech wrote: post #52

Earlier quoted context omitted.

Here's an implementation of such: https://docs.rs/nanval/latest/nanval/

I still don't get what is the advantage over an unsigned integer. Yes, fp64 has unused bits. But why are you going to involve the FPU at all when a uint64 does the trick as well? Plus with a uint64 you get all the flexibility of what bits to dedicate to the address vs metadata. Edit: I guess one advantage is that, if we later treat the handle like a pointer, NaN math gets you NaN again, whereas the uint64 math might…

Honestly I’m with you there I use uint64, but I guess if you’re already storing f64 as a base number type then you just keep everything in a float and it’s more convenient.

Re: Yon – a topos-oriented language with a content-addressed lattice heap

#58

Post by omegafixedpoint »

solomonb wrote: post #42
omegafixedpoint wrote: post #30

A few notes, because this is obviously vibe coded, and does not work in many ways. 1. Yon's documentation mentions "Homotopy type theory:" > the runnable HoTT fragment is refl/pair/fst/snd These are basic features of martin-lof type theory, not homotopy type theory. The documentation makes no reference of an interval type, which is generally the way to go for decidable type-checking in HoTT without univalence as an o…

How does `refl` work if its not even dependently typed?

Had some edits I made halfway through, so I was a bit hasty. It is dependently-typed in that the only valid codomain of a \Pi type is the identity type, Sigma, or another Pi. You can substitute variables, so Id can contain terms, but an arbitrary Pi type like:

\Pi (x : A) (y : B x), C x y

is not allowed. See the Ty definition here: https://github.com/yon-language/yon/blob/aa4617ced3abc92ac53.... Id is the only constructor of Ty that is indexed by a Term (there is another one, TyEl, but it is used nowhere in the type-checker).

This means I could not supply an arbitrary user-defined function (e.g., Fam : (x : A) -> Ty)) as the codomain, only the identity type, which is severely limiting.

I suspect this is why the only example I could find from the docs of dependent types was the Id example above.

I apologize for the poor wording. I didn't sleep well last night.

Do also take this critique with a grain of salt, since the codebase is very much obfuscated and the docs are quite vague.

Re: Yon – a topos-oriented language with a content-addressed lattice heap

#59

Post by danieltanfh95 »

ModernMech wrote: post #41
danieltanfh95 wrote: post #35

Earlier quoted context omitted.

There is nothing physics/metaphysics about this. If you don’t understand the terms, don’t pretend you do and write slop as a comment, it is really not that different from using LLM to generate slop.

"If you don’t understand the terms, don’t pretend you do" The comment you're replying to explicitly says "This language looks interesting, but I don’t understand the concepts." so I'm not sure what you're trying to say. Their note about physics/metaphysics was about "someone [they] knew", not TFA.

Then why even insinuate that these are similar? It's just using it to heavily suggest it is crankery.

Re: Yon – a topos-oriented language with a content-addressed lattice heap

#60

Post by danieltanfh95 »

Retr0id wrote: post #36
danieltanfh95 wrote: post #34

Earlier quoted context omitted.

This isn’t about whether the writer uses LLM or not at all, nor is it about respect. The core novelty it tries to introduce is not hard to understand (even if it is not really that novel). If you don’t want to spend time thinking about what interesting idea it is exploring, that is fine, but pretending or insinuating that it is a LLM problem is just lazy.

What is the core novelty?

Exploring if it makes sense to use maths (or, to be precise, this particular construction) to drive content addressable content + other exploration around the memory space. IMO, no.

https://news.ycombinator.com/item?id=48436337

Post reply on HN