yon-language/yon
View on GitHub ↗ ★ 27 C
An experimental language whose object system is a topos: places are pre-sheaves, values are content-addressed on the Leech lattice, and the type checker refuses to compile a false proof.
6 mentions on Hacker News by 3 people: 1 story, 5 comments · first 2026-06-05 · latest 2026-06-08
20082026
-
Seconding Debruijn indices. See here: https://github.com/yon-language/yon/blob/aa4617ced3abc92ac53... The alpha renaming algorithm does not run under scopes, only lambdas.
comment by omegafixedpoint · 2026-06-08 · in Yon – a topos-oriented language with a content-addressed lattice heap -
…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…
comment by omegafixedpoint · 2026-06-08 · in Yon – a topos-oriented language with a content-addressed lattice heap -
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,…
comment by Retr0id · 2026-06-08 · in Yon – a topos-oriented language with a content-addressed lattice heap -
…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…
comment by omegafixedpoint · 2026-06-07 · in Yon – a topos-oriented language with a content-addressed lattice heap -
…maybe even just simply-typed (except for identity types under Pi). See here in the repo: https://github.com/yon-language/yon/blob/523e363a4a00e8da1410a2521b1d7d1309d360ce/frontend/ast.ml#L37 The datatype Ty only refers to other Ty's. Thus,…
comment by omegafixedpoint · 2026-06-07 · in Yon – a topos-oriented language with a content-addressed lattice heap