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:
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.
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.
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:
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.
\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.