4 ms·

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 4mo 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.

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.