yon

xplicitly 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. 2. Normalization can fail in Yon. Yon's docs say that its universe of propositions has booleans (https://yon-lang.org/book/heyting-core?_highlight=prop). It also says its logic is intuitionistic (AKA, constructive). However, it also says the logical connectives on booleans are CLASSICAL. This implies law of excluded middle, which is NOT constructive without careful sandboxing (e.g., Linear logic). 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). 3. Yon's type definitional equality does not actually reduce types. See here. This is the function used by the type-checker to check if types are equal. https://github.com/yon-language/yon/blob/523e363a4a00e8da141... No reduction actually occurs, conveniently because none of the types actually contain terms (that is, it is simply typed). Yon claims to be dependently-typed. See this in the repo: https://github.com/yon-language/yon/blob/523e363a4a00e8da1410a2521b1d7d1309d360ce/… > 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: > world W { Code is X } > 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.