0
$\begingroup$

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?

$\endgroup$
  • $\begingroup$ This is not research level, but the answer is no because this doesn't satisfy the Liskov substitution principle. $\endgroup$ – xuq01 Dec 18 '18 at 10:51
  • $\begingroup$ @xuq01 Could you provide an example of that as an answer? $\endgroup$ – Vincent Dec 21 '18 at 4:51
  • $\begingroup$ 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. $\endgroup$ – xuq01 Dec 21 '18 at 5:52
4
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Not the answer you're looking for? Browse other questions tagged or ask your own question.