3 ms·
-> could be read as type arrow and ->> as unmatchable type arrow?
by ximeng 8y ago
-> could be read as type arrow and ->> as unmatchable type arrow?
- ggm 8y agocan you "speak" a sentence either here written or in your head, using those words, which feels like it makes sense?
- sitkack 8y agoI appreciate your meta-level.
- 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.
- danidiaz 8y ago->> is a function at the type level without extra properties like matchability, so it can be simply read as "to" or "into" -> is used with type constructors like Maybe or Either, and arguments passed to it can still be "read" in the result (for example, a -> Maybe a, or a -> b -> Either a b). I would call it a "slotting" arrow to connote that the argument will be fitted into a hole of a type constructor. So I would read a -> Maybe a as "slotting a into Maybe".