3 ms·
"As an example, the kind of Maybe remains ⋆ → ⋆, but DbType now has kind ⋆ ↠ ⋆" - the kind of Maybe remains star type arrow star, but DbType now has kind star u
by ximeng 8y ago
"As an example, the kind of Maybe remains ⋆ → ⋆, but DbType now has kind ⋆ ↠ ⋆" - the kind of Maybe remains star type arrow star, but DbType now has kind star unmatchable type arrow star.
- ggm 8y agounmatchable type or not yet matched type? dangling type? provisional type? unconfirmed type?
- ximeng 8y agoUnmatchable type, following terminology from the paper. This is contrasted with a matchable type which is "injective" and "generative". Basically these unmatchable types are potentially ambiguous under certain operations, so it indicates to the type system limits to the transformations which can be done. So Maybe is * -> * means that if Maybe a is f a, then f is Maybe, and if Maybe a is Maybe b then a is b. If another type t is * ->> *, then the type checker can't make these assumptions.