7 ms·

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,

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/aa4617ced3abc92ac53afb4d49b258df52e84e24/frontend/ast.ml#L37 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.

solomonb 3mo ago
I respect you for taking the time to review this codebase. Personally I don't want to do that. It sounds like a mess.
- omegafixedpoint 3mo ago
  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/aa4617ced3abc92ac53afb4d49b258df52e84e24/frontend/catt_r_yon.ml#L45 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 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/aa4617ced3abc92ac53afb4d49b258df52e84e24/frontend/subst.ml#L38 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/aa4617ced3abc92ac53afb4d49b258df52e84e24/frontend/subst.ml#L28 https://github.com/yon-language/yon/blob/aa4617ced3abc92ac53...). However, scopes don't check this at all. https://github.com/yon-language/yon/blob/aa4617ced3abc92ac53afb4d49b258df52e84e24/frontend/subst.ml#L38 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.

solomonb 3mo ago

I respect you for taking the time to review this codebase. Personally I don't want to do that. It sounds like a mess.

omegafixedpoint 3mo ago
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/aa4617ced3abc92ac53afb4d49b258df52e84e24/frontend/catt_r_yon.ml#L45 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 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/aa4617ced3abc92ac53afb4d49b258df52e84e24/frontend/subst.ml#L38 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/aa4617ced3abc92ac53afb4d49b258df52e84e24/frontend/subst.ml#L28 https://github.com/yon-language/yon/blob/aa4617ced3abc92ac53...). However, scopes don't check this at all. https://github.com/yon-language/yon/blob/aa4617ced3abc92ac53afb4d49b258df52e84e24/frontend/subst.ml#L38 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.