How does `refl` work if its not even dependently typed?
\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.
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.