# Is a reference on T a subtype of T?

If I take the book Practical Foundations for Programming Languages by Robert Harper, the following definition is given for subtyping:

A subtype relation is a pre-order on types that validates the subsumption principle: if $$\tau'$$ is a subtype of $$\tau$$, then a value of type $$\tau'$$ may be provided when a value of type $$\tau$$ is required.

I was wondering whether we can say that a reference on $$T$$, denoted by $$\text{Ref }T$$ is a subtype of $$T$$. If not, why?

• This is not research level, but the answer is no because this doesn't satisfy the Liskov substitution principle. – xrq Dec 18 '18 at 10:51
• @xuq01 Could you provide an example of that as an answer? – Vincent Dec 21 '18 at 4:51
• I don't really want to right now, because I think this question is off topic here, but I think it could be migrated to CS.SE. If the admins do that I will add an answer. – xrq Dec 21 '18 at 5:52

No, Ref T is not a subtype of T. In typical sub-typing rules, a term of type Ref T is not substitutable for a term of type T. A Ref T has the value of a pointer to a location in memory of an T, whereas T has the value of an T. More concretely, in ML-based languages, in order to pass the value from a Ref T to a function that takes the enclosed type T, you need to dereference the argument first. Typically that will involve using a unary operator like !.

So, while it is possible that a coercion could make the Ref T appear to be a subtype, I think it's better to think of Ref as a container type, rather than a more specific kind of T.

An example from OCaml:

# let t = ref 2 ;;
val t : int ref = {contents = 2}
# let q : int = t ;;
Error: This expression has type int ref
but an expression was expected of type int
# let r : int = !t ;;
val r : int = 2


A possible workaround for this would be to look into some form of implicit coercions, which are available in certain languages. See more on coercion here.