omegafixedpoint

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

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

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.

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.

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 opaque axiom.
  
  Pi types are mentioned, but Yon does not have dependent types. From what I can tell, they are polymorphic, 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, it is not dependent. Terms cannot appear in types. Pi is explicitly indexed by a type defining its domain and codomain. A pi type is not a pi type if its codomain cannot depend on its domain.

  Yon dangerously allows propositions to be lifted to booleans. If I am interpreting correctly (docs are very vague), this means propositions can be lifted to terms. This causes an obvious failure of normalization due to assumed proof irrelevance (otherwise Prop would not be distinguished) (also see Coquand's paper on this https://arxiv.org/abs/1911.08174).

  Yon claims to be dependently-typed. See this in the repo: https://github.com/yon-language/yon/blob/523e363a4a00e8da1410a2521b1d7d1309d360ce/frontend/ast.ml#L21
  > Types in Yon Core kernel — the small dependent type theory used for the operational semantics.

  Suppose I'm reading the source code wrong. Conveniently, the comment one line below reveals, once again, that the "type theory" is simply-typed:

  >  *   T, U ::= Type_n                            universe of level n
  >  *         |  Pi(x:T). U                         dependent function

  Pi types eliminate into a FIXED type that does not depend on x. This means there is also no purpose for having a universe hierarchy.

  To confirm, I scoured the docs a bit for any examples using Pi types or Sigma types. I searched the docs, and could not find any, besides this example:

place Account in W { balance number }

fun takes_sub(s: { a : Account where Pi(x: Account). Pi(y: Account). Id(Account, x, y) }): number { return 0 }

fun main(): number { return 0 }

Notably, the identity is the only constructor for Ty indexed by a term. That is, Pi types can ONLY eliminate into the identity. What if I want my Pi type to eliminate into anything else living in Prop? e.g., an existential like \forall (x : Nat), \exists (y : Nat), x < y. Unfortunately impossible in Yon.

This project is clearly produced by AI, and clearly dangerously incorrect. Do not use this for anything serious.