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

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

<p>An example from OCaml:</p>

<pre><code># 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
</code></pre>

<p>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 <a href="https://en.wikibooks.org/wiki/Introduction_to_Programming_Languages/Coercion" rel="nofollow noreferrer">here</a>.</p>

CC BY-SA 4.0
2018-12-15T05:52:13.470Z
2018-12-15T05:52:13.470Z
Will Bradley
<p>If I take the book <em>Practical Foundations for Programming Languages</em> by Robert Harper, the following definition is given for subtyping:</p>

<blockquote>
  <p>A subtype relation is a pre-order on types that validates the subsumption principle: if <span class="math-container">$\tau'$</span> is a subtype of <span class="math-container">$\tau$</span>, then a value of type <span class="math-container">$\tau'$</span> may be provided when a value of type <span class="math-container">$\tau$</span> is required.</p>
</blockquote>

<p>I was wondering whether we can say that a reference on <span class="math-container">$T$</span>, denoted by <span class="math-container">$\text{Ref }T$</span> is a subtype of <span class="math-container">$T$</span>. If not, why? </p>

CC BY-SA 4.0
2018-12-18T10:51:09.600Z
This is not research level, but the answer is no because this doesn't satisfy the Liskov substitution principle.
xrq
CC BY-SA 4.0
2018-12-21T04:51:17.597Z
@xuq01 Could you provide an example of that as an answer?
Vincent
CC BY-SA 4.0
2018-12-21T05:52:38.343Z
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
<type-theory><type-systems>
Is a reference on T a subtype of T?
Vincent
# Is a reference on T a subtype of T?

(Asked by: username_0 on 2018-12-14)

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?

**Tags:** type-theory, type-systems
> **Comments:**
> **username_1**: This is not research level, but the answer is no because this doesn't satisfy the Liskov substitution principle.  
> **username_0**: @xuq01 Could you provide an example of that as an answer?  
> **username_1**: 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.  

---

## 1 answers

### Answer by username_2 on 2018-12-15. Score: 4 | Accepted answer

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.


---

