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

71–80 of 93 posts

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

#71

Post by amenn »

dirkt wrote: post #25
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…

> Does this stuff make sense to other people? Nope, and I actually learned about application of category theory to programming language in university. I tried to get an idea about the main points, and then stumbled over > a thing is what you can observe of it. > > [...] > > Content addressing is extensionality made physical (chapter 11): two values indistinguishable by observation are not merely equal, they are the s…

I am using flat memory comparisons (memcmp)

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

#72

Post by amenn »

jrmg wrote: post #19
esafak wrote: post #8

Could you name a few languages you had in mind while developing this, their respective problems, and how your language improves them, feature by feature? > Yon allocates into xleech2, a content-addressed heap whose geometry is the Leech lattice Λ24: exactly 196,560 slots per heap. What is the computational complexity of memory allocation into this Leech lattice? What applications did you have in mind where making all…

I have trouble with the idea that these lattice structures could be less computationally complex or less likely to collide than a good simple hash table. I guess they could be more guaranteed to have stable access times? The more I try to understand, the more it appears that they are a hash table (hash-addressed-structure to be pedantic), but with way more complicated backing than a hash table.

[dead]

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

#73

Post by amenn »

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…

[dead]

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

#74

Post by amenn »

danieltanfh95 wrote: post #61
mccoyb wrote: post #37

Earlier quoted context omitted.

Explain away then my friend: surely your clear explanation will benefit many other readers who came away with similar confusion?

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

[dead]

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

#75

Post by amenn »

z4lis wrote: post #14

You must not mix up technical mathematical words with softer prose words. For instance, "Yon's data model is categorical. A world is a category, a semantic site;" So if you want to define a world, I expect you to tell me how to supply objects + morphisms + the composition law + the site structure. I don't know what a "semantic site" is, just what a "site" is. You'd need to define it. Anyway, we then get to our first…

[dead]

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

#77

Post by amenn »

Syzygies wrote: post #40
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…

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…

[dead]

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

#78

Post by Retr0id »

amenn wrote: post #70
Retr0id wrote: post #66

Earlier quoted context omitted.

I have a strong understanding of content addressing, memory allocation, data structures, and a superficial understanding of lattices. It is not clear how one has anything to do with the other. If there is any meaningful link or benefit, it has not been explained. Perhaps some magical insight is waiting for me if I understand the Leech lattice better, but given PhD category theorists are also scratching their heads I…

Still writing the docs. Content addressing is the mechanism, that is: same content lands in the same slot, equality is a handle compare. The allocator is provably extensional so distinct content never aliases even though the hash itself can collide. The Leech part: the heap is sized to the lattice's 196,560 minimal vectors, the coordinate-to-slot map is a collision-free perfect hash built from the Conway group's mm_o…

I understand that you can hash any object into a 196,560-slot space (that's how regular hash tables work), but I'm not sure why you'd want to do that. Regular hash tables can be resized when they get full (or less-full), yours cannot. How is this any different from a hash table with a fixed capacity of 196,560 entries?

"provably extensional" is not an established term in this context and communicates nothing about the design. I simply do not believe that this design doesn't have trivial collision issues, or that it makes efficient use of memory.

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

#79

Post by lambdas »

amenn wrote: post #69
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…

There's no wrong in vibe coding as long as you check what's the output. I can be wrong or missing the goal of course. But the work is in progress and I'm not writing a bash script for the theorem of pytagora. It's more complex and I'm studying as I go. You reviewed frontend/ast.ml, the small kernel, and concluded MLTT, but you missed frontend/cubical.ml. Thanks for the time you took to bring this critique, it will be…

Oooft, in cubical.ml why is your identity equivalence `CVar "__id"`? Surely this should be some fibration/reduction?

In fact, these weird string terms pop up pretty often, but surely you’d want to be using de Brujin indices lest you accidentally string match two different things (can’t believe I’m saying that for an implementation of a dependently typed language).

I started to wonder how your types were glued, as I would have thought Sigma types glued along identity equivalences would give me some insight on the odd behaviour.

`reduce_comp` seemed like the place it should be. There I realised your `CTGlue` case is wrong: it seems like `partial_pairs` is in the head but dropped from the body, so they’re never glued by any equivalence.

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

#80

Post by bitwalker »

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…

The benefit is that floats are allowed to be unboxed values - without NaN-boxing, you must heap-allocate them. The tradeoff is that immediate/unboxed integer values end up being smaller than the full machine word range (i.e. you have either a 24-bit or 48-bit mantissa you can use to hold data), but that's usually worthwhile because most integers are small anyway, so you box larger ones. Similarly, pointer values can't use the full address space, but that's also usually worth it since rarely do you actually need to do so in VMs where this technique is used.

Using unsigned integers is only a better choice if your VM doesn't need efficient floating-point operations.

Post reply on HN