Skip to content

Commit 9dfe28a

Browse files
soimortsoimort
committed
plt/subtyping: new page (Subtyping)
1 parent 9248030 commit 9dfe28a

File tree

2 files changed

+186
-0
lines changed

2 files changed

+186
-0
lines changed

‎plt/subtyping/index.html‎

Lines changed: 123 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,123 @@
1+
<!DOCTYPE html>
2+
<!-- Academia (pandoc HTML5 template)
3+
designer: soimort
4+
last updated: 2016-05-07
5+
last adapted: 2017-09-25 -->
6+
<html>
7+
<head>
8+
<meta charset="utf-8">
9+
<meta name="generator" content="pandoc">
10+
<meta name="viewport" content="width=device-width, initial-scale=1.0, user-scalable=yes">
11+
<meta name="author" content="Mort Yao">
12+
<meta name="dcterms.date" content="2018-02-08">
13+
<title>Subtyping</title>
14+
<link rel="canonical" href="https://wiki.soimort.org/plt/subtyping">
15+
<style type="text/css">code { white-space: pre; }</style>
16+
<link rel="stylesheet" href="//cdn.soimort.org/normalize/5.0.0/normalize.min.css">
17+
<link rel="stylesheet" href="//cdn.soimort.org/mathsvg/latest/mathsvg.min.css">
18+
<link rel="stylesheet" href="//cdn.soimort.org/fonts/latest/Latin-Modern-Roman.css">
19+
<link rel="stylesheet" href="//cdn.soimort.org/fonts/latest/Latin-Modern-Mono.css">
20+
<link rel="stylesheet" href="//cdnjs.cloudflare.com/ajax/libs/font-awesome/4.7.0/css/font-awesome.min.css">
21+
<link rel="stylesheet" href="/__/css/style.css">
22+
<link rel="stylesheet" href="/__/css/pygments.css">
23+
<script src="https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.2/MathJax.js?config=TeX-AMS_CHTML-full" type="text/javascript"></script>
24+
<!--[if lt IE 9]>
25+
<script src="//cdnjs.cloudflare.com/ajax/libs/html5shiv/3.7.3/html5shiv-printshiv.min.js"></script>
26+
<![endif]-->
27+
<script src="//cdn.soimort.org/jk/20160504/jk.min.js"></script>
28+
<script src="//cdn.soimort.org/mathsvg/latest/mathsvg.min.js"></script>
29+
<script src="/__/js/jk-minibar.js"></script>
30+
<link rel="icon" href="/favicon.png">
31+
<link rel="apple-touch-icon" href="/favicon.png">
32+
</head>
33+
<body>
34+
<p hidden>
35+
<span class="math display">\[\def\textsc#1{\textsf{#1}}\]</span>
36+
</p>
37+
<main><article>
38+
<header>
39+
<h1 class="title">Subtyping</h1>
40+
<!-- h3 class="date">2018-02-08</h3 -->
41+
</header>
42+
<div id="content">
43+
<p><em>Subtyping</em> is a form of type polymorphism, represented as a preorder on types: <span class="math display">\[\tau&#39; \preceq \tau\]</span> we say that <span class="math inline">\(\tau&#39;\)</span> is a <em>subtype</em> of <span class="math inline">\(\tau\)</span>, and that <span class="math inline">\(\tau\)</span> is a <em>supertype</em> of <span class="math inline">\(\tau&#39;\)</span>. (Note that <span class="math inline">\(\preceq\)</span> need not be a partial order, as no antisymmetry is assumed, i.e., it may be the case that both <span class="math inline">\(\tau&#39; \preceq \tau\)</span> and <span class="math inline">\(\tau \preceq \tau&#39;\)</span> but not <span class="math inline">\(\tau&#39; = \tau\)</span>.)</p>
44+
<p>As a preorder, the subtyping relation satisfies reflexivity: <span class="math display">\[\frac{}{
45+
\tau \preceq \tau
46+
}\qquad\textsc{ST-Refl}\]</span> and transitivity: <span class="math display">\[\frac{
47+
\tau&#39; \preceq \tau&#39;&#39; \qquad
48+
\tau&#39;&#39; \preceq \tau
49+
}{
50+
\tau&#39; \preceq \tau
51+
}\qquad\textsc{ST-Trans}\]</span></p>
52+
<p>On function types, the following rule applies: <span class="math display">\[\frac{
53+
\tau_1 \preceq \tau_1&#39; \qquad
54+
\tau_2&#39; \preceq \tau_2
55+
}{
56+
\tau_1&#39; \to \tau_2&#39; \preceq \tau_1 \to \tau_2
57+
}\qquad\textsc{ST-Fun}\]</span> The <span class="math inline">\(\to\)</span> type constructor is said to be <em>contravariant</em> in the argument type and <em>covariant</em> in the return type.</p>
58+
<p>The typing rule of <em>subsumption</em> applies: <span class="math display">\[\frac{
59+
\Gamma \vdash t : \tau&#39;
60+
\qquad \tau&#39; \preceq \tau
61+
}{
62+
\Gamma \vdash t : \tau
63+
}\qquad\textsc{T-Sub}\]</span></p>
64+
<p><strong>Nominal vs. structural subtyping.</strong> <em>Nominal subtyping</em> requires an explicit declaration of the subtype/supertype relation. In contrast, in <em>structural subtyping</em>, the structure of two types determines the subtype/supertype relation.</p>
65+
<p><strong>Inclusive vs. coercive subtyping.</strong> Given <span class="math inline">\(\tau&#39; \preceq \tau\)</span>. In an <em>inclusive</em> implementation of subtyping, a term <span class="math inline">\(t&#39; : \tau&#39;\)</span> is just the same value (of type <span class="math inline">\(\tau\)</span>) <span class="math inline">\(t&#39; : \tau\)</span>. In a <em>coercive</em> implementation of subtyping, a term <span class="math inline">\(t&#39; : \tau&#39;\)</span> must be converted to another value (of type <span class="math inline">\(\tau\)</span>) <span class="math inline">\(t : \tau\)</span>, using an implicit type conversion function <span class="math inline">\(coerce: \tau&#39; \to \tau\)</span> from subtype to supertype (e.g., from an integer to a floating-point number).</p>
66+
<p><strong>Mutable references.</strong> Write-only references (i.e., <em>sinks</em>) are contravariant, and read-only references (i.e., <em>sources</em>) are covariant. Mutable references which act as both sources and sinks are invariant.</p>
67+
<p><strong>Behavioral subtyping in OOP.</strong> In the scope of object-oriented programming where side effects are allowed, the notion of <em>behavioral subtyping</em> and the <em>Liskov substitution principle</em> apply, which are stronger than the above (sub)typing rules. Behavioral subtyping requires that subtypes preserve all invariants guaranteed by the supertypes in some contract; this problem is generally undecidable thus cannot be guaranteed by a type checker.</p>
68+
<p><strong>Subtyping and FP.</strong></p>
69+
<p>Conventionally, functional languages like ML and Haskell provide no direct support for subtype polymorphism. Subtyping raises difficulty for type inference; moreover, it is problematic in the presence of mutability. See:</p>
70+
<ul>
71+
<li><a href="https://redd.it/423o0c" class="uri">https://redd.it/423o0c</a></li>
72+
</ul>
73+
<p>Standard ML’s parametric polymorphism may be used to encode the subtyping hierarchy. See:</p>
74+
<ul>
75+
<li><a href="http://mlton.org/ObjectOrientedProgramming" class="uri">http://mlton.org/ObjectOrientedProgramming</a></li>
76+
<li>Matthew Fluet and Riccardo Pucella, “Phantom Types and Subtyping.” [<a href="https://www.cs.rit.edu/~mtf/research/phantom-subtyping/jfp06/jfp06.pdf">PDF</a>]</li>
77+
</ul>
78+
<p>Type inference has been implemented on MLsub, a superset of the core ML language. See:</p>
79+
<ul>
80+
<li>Stephen Dolan and Alan Mycroft, “Polymorphism, Subtyping, and Type Inference in MLsub.” [<a href="https://www.cl.cam.ac.uk/~sd601/papers/mlsub-preprint.pdf">PDF</a>] [<a href="https://github.com/stedolan/mlsub">Code</a>]</li>
81+
</ul>
82+
</div>
83+
<footer>
84+
<!-- TO BE MODIFIED BY NEED -->
85+
<a title="Keyboard shortcut: q"
86+
href="..">
87+
<i class="fa fa-angle-double-left" aria-hidden="true"></i>
88+
<code>Parent</code>
89+
</a> |
90+
<a class="raw" accesskey="r"
91+
title="Keyboard shortcut: R"
92+
href="https://wiki.soimort.org/plt/subtyping/src.md">
93+
<i class="fa fa-code" aria-hidden="true"></i>
94+
<code>Raw</code>
95+
</a> |
96+
<a class="history" accesskey="h"
97+
title="Keyboard shortcut: H"
98+
href="https://github.com/soimort/wiki/commits/gh-pages/plt/subtyping/src.md">
99+
<i class="fa fa-history" aria-hidden="true"></i>
100+
<code>History</code>
101+
</a> |
102+
<a class="edit" accesskey="e"
103+
title="Keyboard shortcut: E"
104+
href="https://github.com/soimort/wiki/edit/gh-pages/plt/subtyping/src.md">
105+
<i class="fa fa-code-fork" aria-hidden="true"></i>
106+
<code>Edit</code>
107+
</a> |
108+
<a title="Keyboard shortcut: p"
109+
href="javascript:window.print();">
110+
<i class="fa fa-print" aria-hidden="true"></i>
111+
<code>Print</code>
112+
</a> |
113+
<a title="Keyboard shortcut: ."
114+
href="https://wiki.soimort.org/plt/subtyping">
115+
<i class="fa fa-anchor" aria-hidden="true"></i>
116+
<code>Permalink</code>
117+
</a> |
118+
Last updated: <span id="update-time">2018-02-08</span>
119+
<address class="author">Mort Yao</address>
120+
</footer>
121+
</article></main>
122+
</body>
123+
</html>

‎plt/subtyping/src.md‎

Lines changed: 63 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,63 @@
1+
% Subtyping
2+
% Mort Yao
3+
% 2018-02-08
4+
5+
*Subtyping* is a form of type polymorphism, represented as a preorder on types:
6+
$$\tau' \preceq \tau$$
7+
we say that $\tau'$ is a *subtype* of $\tau$, and that $\tau$ is a *supertype* of $\tau'$. (Note that $\preceq$ need not be a partial order, as no antisymmetry is assumed, i.e., it may be the case that both $\tau' \preceq \tau$ and $\tau \preceq \tau'$ but not $\tau' = \tau$.)
8+
9+
As a preorder, the subtyping relation satisfies reflexivity:
10+
$$\frac{}{
11+
\tau \preceq \tau
12+
}\qquad\textsc{ST-Refl}$$
13+
and transitivity:
14+
$$\frac{
15+
\tau' \preceq \tau'' \qquad
16+
\tau'' \preceq \tau
17+
}{
18+
\tau' \preceq \tau
19+
}\qquad\textsc{ST-Trans}$$
20+
21+
On function types, the following rule applies:
22+
$$\frac{
23+
\tau_1 \preceq \tau_1' \qquad
24+
\tau_2' \preceq \tau_2
25+
}{
26+
\tau_1' \to \tau_2' \preceq \tau_1 \to \tau_2
27+
}\qquad\textsc{ST-Fun}$$
28+
The $\to$ type constructor is said to be *contravariant* in the argument type and *covariant* in the return type.
29+
30+
The typing rule of *subsumption* applies:
31+
$$\frac{
32+
\Gamma \vdash t : \tau'
33+
\qquad \tau' \preceq \tau
34+
}{
35+
\Gamma \vdash t : \tau
36+
}\qquad\textsc{T-Sub}$$
37+
38+
**Nominal vs. structural subtyping.** *Nominal subtyping* requires an explicit declaration of the subtype/supertype relation. In contrast, in *structural subtyping*, the structure of two types determines the subtype/supertype relation.
39+
40+
**Inclusive vs. coercive subtyping.** Given $\tau' \preceq \tau$. In an *inclusive* implementation of subtyping, a term $t' : \tau'$ is just the same value (of type $\tau$) $t' : \tau$. In a *coercive* implementation of subtyping, a term $t' : \tau'$ must be converted to another value (of type $\tau$) $t : \tau$, using an implicit type conversion function $coerce: \tau' \to \tau$ from subtype to supertype (e.g., from an integer to a floating-point number).
41+
42+
**Mutable references.** Write-only references (i.e., *sinks*) are contravariant, and read-only references (i.e., *sources*) are covariant. Mutable references which act as both sources and sinks are invariant.
43+
44+
**Behavioral subtyping in OOP.**
45+
In the scope of object-oriented programming where side effects are allowed, the notion of *behavioral subtyping* and the *Liskov substitution principle* apply, which are stronger than the above (sub)typing rules. Behavioral subtyping requires that subtypes preserve all invariants guaranteed by the supertypes in some contract; this problem is generally undecidable thus cannot be guaranteed by a type checker.
46+
47+
**Subtyping and FP.**
48+
49+
Conventionally, functional languages like ML and Haskell provide no direct support for subtype polymorphism. Subtyping raises difficulty for type inference; moreover, it is problematic in the presence of mutability. See:
50+
51+
* <https://redd.it/423o0c>
52+
53+
Standard ML's parametric polymorphism may be used to encode the subtyping hierarchy. See:
54+
55+
* <http://mlton.org/ObjectOrientedProgramming>
56+
* Matthew Fluet and Riccardo Pucella, "Phantom Types and Subtyping."
57+
[[PDF](https://www.cs.rit.edu/~mtf/research/phantom-subtyping/jfp06/jfp06.pdf)]
58+
59+
Type inference has been implemented on MLsub, a superset of the core ML language. See:
60+
61+
* Stephen Dolan and Alan Mycroft, "Polymorphism, Subtyping, and Type Inference in MLsub."
62+
[[PDF](https://www.cl.cam.ac.uk/~sd601/papers/mlsub-preprint.pdf)]
63+
[[Code](https://github.com/stedolan/mlsub)]

0 commit comments

Comments
 (0)