top | item 42613356

(no title)

herrington_d | 1 year 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

> If a type error appears _anywhere_, the program is formally meaningless _everywhere_

discuss

order

crowdhailer|1 year ago

The EYG type system does support recovery, so you will get multiple type errors if that's the case in the program.

herrington_d|1 year ago

My point is that type error recovery is the property of the type system. Not the property of structural code editor.