Makes me think of another mnemonic for subtyping: S <: T when id : S -> T is well-typed.

"Our language comes with a subtyping relation T <: S that tells when it is safe to use elements of T in a context that expects elements of S."


@lyxia It's always safe to use elements of one type in contexts that expect elements of another one… except when it's not…

Seriously, though, 's :> offers to save a few keystrokes, by not specifying the field of the structure, at the expense of harder debugging, when the types aren't quite coercible…

Sure I can get the aesthetics of identifying an algebraic structure with it's carrier, as is commonly done in informal math, but still, it's a fragile mechanism, IMO.

This is talking about the theory of subtyping though, not Coq coercions.

Sign in to participate in the conversation
Functional Café

The social network of the future: No ads, no corporate surveillance, ethical design, and decentralization! Own your data with Mastodon!