->> 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".
"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.
Unmatchable 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.
