A bidirectional typechecking puzzle in the Grace programming language
4 hours ago
- #bidirectional-typechecking
- #type-inference
- #programming-language-design
- Grace's bidirectional typechecking had limitations leading to a bug in list type inference.
- The bug caused incorrect list element types due to using the first element's type as the list's element type.
- Grace's typechecker elaborates expressions, inserting coercions like some tags for Optional types.
- The solution introduced a 'most-specific supertype' operation for inferring correct list element types.
- Record coercion is necessary for soundness and handling real-world JSON data.