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

81–90 of 93 posts

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

#81

Post by jrmg »

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…

Are you saying that two distinct pieces of content can never collide? That seems obviously incorrect.

For example, take the integers 0 - 196,561, and put them into your lattice-based map. Something’s got to give. There are only 196,560 containers in the map (right?)

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

#82

Post by Retr0id »

jrmg wrote: post #81
amenn wrote: post #70

Earlier quoted context omitted.

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…

Are you saying that two distinct pieces of content can never collide? That seems obviously incorrect. For example, take the integers 0 - 196,561, and put them into your lattice-based map. Something’s got to give. There are only 196,560 containers in the map (right?)

It's just a regular hash table with linear probing https://github.com/yon-language/yon/blob/aa4617ced3abc92ac53...

The only relation to the Leech group appears to be the number of slots.

When a table gets full they allocate a second one, and so on, up until 256 tables when allocations start silently failing (after exactly 50319104 allocations).

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

#83

Post by jrmg »

Retr0id wrote: post #82
jrmg wrote: post #81

Earlier quoted context omitted.

Are you saying that two distinct pieces of content can never collide? That seems obviously incorrect. For example, take the integers 0 - 196,561, and put them into your lattice-based map. Something’s got to give. There are only 196,560 containers in the map (right?)

It's just a regular hash table with linear probing https://github.com/yon-language/yon/blob/aa4617ced3abc92ac53... The only relation to the Leech group appears to be the number of slots. When a table gets full they allocate a second one, and so on, up until 256 tables when allocations start silently failing (after exactly 50319104 allocations).

Ha! Well that answers my question.

I hope OP is seriously considering what’s actually been built here, and how their interactions with whatever LLM they’ve been using really reflects that. I’m genuinely a bit concerned for them.

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

#84

Post by jrmg »

danieltanfh95 wrote: post #59
ModernMech wrote: post #41

Earlier quoted context omitted.

"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.

I indeed was insinuating that OP may be in the early stages of AI psychosis - or, if you don’t believe that’s a thing, at least in a mildly delusional or hyperactive state.

If I’m wrong, I don’t think any of the advice I gave was harmful. Really it’s good advice for anyone sunk deep into a problem to periodically take space, relax and recharge - and potentially allow their brain to work on it in the background while they do.

My questions came from a genuine place of wanting to understand the system though.

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

#85

Post by omegafixedpoint »

solomonb wrote: post #64
omegafixedpoint wrote: post #58

Earlier quoted context omitted.

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 const…

I respect you for taking the time to review this codebase. Personally I don't want to do that. It sounds like a mess.

Yeah it really is a mess. One of the most egregious things I noticed was that variables under lambdas are STRINGS: https://github.com/yon-language/yon/blob/aa4617ced3abc92ac53...

This is extremely dangerous and error prone. The classic example is: (fun (x : number) (y : number) => x) y once y is substituted for x, x now refers to y, which is bound later.

This is usually avoided with Debruijn indices (https://en.wikipedia.org/wiki/De_Bruijn_index). That function becomes:

(fun (_ : number) => (_ : number) => 2) y

Lambda binders refer to variables via an offset relative to the position of the variable. However, Yon doesn't do this. It uses strings. The usual approach to make this sound is alpha renaming (which is by default very easy to mess up and introduce bugs). However, Yon's alpha renaming algorithm has a critical error:

https://github.com/yon-language/yon/blob/aa4617ced3abc92ac53...

Notice that substitution under lambdas checks that the "fresh" name for the bound variable does not appear in the free variables under the lambda body (https://github.com/yon-language/yon/blob/aa4617ced3abc92ac53...). However, scopes don't check this at all. https://github.com/yon-language/yon/blob/aa4617ced3abc92ac53...

This is a critical, foundational bug that is easily avoided with DeBruijn indices. DeBruijn indices are widely used across all proof assistants. This oversight is absolutely due to a lack of understanding of type theory.

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

#86

Post by omegafixedpoint »

lambdas wrote: post #79
amenn wrote: post #69

Earlier quoted context omitted.

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 w…

Seconding Debruijn indices. See here: https://github.com/yon-language/yon/blob/aa4617ced3abc92ac53...

The alpha renaming algorithm does not run under scopes, only lambdas.

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

#87

Post by [deleted] »

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…

[deleted]

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

#88

Post by danieltanfh95 »

jrmg wrote: post #84
danieltanfh95 wrote: post #59

Earlier quoted context omitted.

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

I indeed was insinuating that OP may be in the early stages of AI psychosis - or, if you don’t believe that’s a thing, at least in a mildly delusional or hyperactive state. If I’m wrong, I don’t think any of the advice I gave was harmful. Really it’s good advice for anyone sunk deep into a problem to periodically take space, relax and recharge - and potentially allow their brain to work on it in the background while…

Thanks for being honest, at least.

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

#89

Post by dkersten »

mccoyb wrote: post #3

I'm not sure where or how to convey this, because I've seen several of these languages designed with AI, documentation created using AI, etc -- posted on Hacker News in the last months or so, and I've responded to each one with roughly the same feedback (and I'm assuming good faith: that the intent is that the poster wishes to grow as a language designer). Your audience, or whoever you aim your work at, should be tre…

> You've gone too fast, too much is vague, nothing is clear.

Contrast to when Clojure was released: Rich Hickey had spent years thinking about, researching, and refining the concepts. It was easy to understand what the language is. And it shows in the design quality as even now, almost two decades later, the language has changed surprisingly little and is still really good.

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

#90

Post by canyp »

bitwalker wrote: post #80
canyp wrote: post #55

Earlier quoted context omitted.

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'…

Makes sense, thank you.
Post reply on HN