We need to add sugar conversion between a formal representation and user representation of type.
let's say we have a type forall a. (a, a). Its formal rep is forall a (b ~ (a, a)). b. The second rep is confusing and not intuitive and user will be forced to fully understand MLF to understand formal rep of type. To avoid this, we need to add sugar transformation between Graphic type and Syntactic type.
We need to add sugar conversion between a formal representation and user representation of type.
let's say we have a type
forall a. (a, a)
. Its formal rep isforall a (b ~ (a, a)). b
. The second rep is confusing and not intuitive and user will be forced to fully understand MLF to understand formal rep of type. To avoid this, we need to add sugar transformation between Graphic type and Syntactic type.