4 ms·
> Better type information. Because the program is always in a valid state the type checker can always run and give meaningful feedback. Note that programs can
by herrington_d 2y ago
> Better type information. Because the program is always in a valid state the type checker can always run and give meaningful feedback.
Note that programs can be syntactically well-formed but ill-typed. For example `let x = true + 1` has valid syntax but produces an "undefined" type for the variable `x`, if the type system does not support type error recovery.
A quote from the great paper from POPL 2024, https://hazel.org/papers/marking-popl24.pdf https://hazel.org/papers/marking-popl24.pdf
> If a type error appears _anywhere_, the program is formally meaningless _everywhere_
- crowdhailer 2y agoThe EYG type system does support recovery, so you will get multiple type errors if that's the case in the program.
- herrington_d 2y agoMy point is that type error recovery is the property of the type system. Not the property of structural code editor.