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, #Coq'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

Welcome to your niu world ! We are a cute and loving international community O(≧▽≦)O !