| 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/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). 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. |