mirror
/
rustc-dev-guide
mirror of https://github.com/rust-lang/rustc-dev-guide.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity
rustc-dev-guide/traits/lowering-to-logic.html

376 lines
19 KiB
HTML
Raw Permalink Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

<!DOCTYPE HTML>
<html lang="en" class="light sidebar-visible" dir="ltr">
<head>
<!-- Book generated using mdBook -->
<meta charset="UTF-8">
<title>Lowering to logic - Rust Compiler Development Guide</title>
<!-- Custom HTML head -->
<meta name="description" content="A guide to developing the Rust compiler (rustc)">
<meta name="viewport" content="width=device-width, initial-scale=1">
<meta name="theme-color" content="#ffffff">
<link rel="icon" href="../favicon.svg">
<link rel="shortcut icon" href="../favicon.png">
<link rel="stylesheet" href="../css/variables.css">
<link rel="stylesheet" href="../css/general.css">
<link rel="stylesheet" href="../css/chrome.css">
<link rel="stylesheet" href="../css/print.css" media="print">
<!-- Fonts -->
<link rel="stylesheet" href="../FontAwesome/css/font-awesome.css">
<link rel="stylesheet" href="../fonts/fonts.css">
<!-- Highlight.js Stylesheets -->
<link rel="stylesheet" id="highlight-css" href="../highlight.css">
<link rel="stylesheet" id="tomorrow-night-css" href="../tomorrow-night.css">
<link rel="stylesheet" id="ayu-highlight-css" href="../ayu-highlight.css">
<!-- Custom theme stylesheets -->
<!-- Provide site root and default themes to javascript -->
<script>
const path_to_root = "../";
const default_light_theme = "light";
const default_dark_theme = "navy";
</script>
<!-- Start loading toc.js asap -->
<script src="../toc.js"></script>
</head>
<body>
<div id="body-container">
<!-- Work around some values being stored in localStorage wrapped in quotes -->
<script>
try {
let theme = localStorage.getItem('mdbook-theme');
let sidebar = localStorage.getItem('mdbook-sidebar');
if (theme.startsWith('"') && theme.endsWith('"')) {
localStorage.setItem('mdbook-theme', theme.slice(1, theme.length - 1));
}
if (sidebar.startsWith('"') && sidebar.endsWith('"')) {
localStorage.setItem('mdbook-sidebar', sidebar.slice(1, sidebar.length - 1));
}
} catch (e) { }
</script>
<!-- Set the theme before any content is loaded, prevents flash -->
<script>
const default_theme = window.matchMedia("(prefers-color-scheme: dark)").matches ? default_dark_theme : default_light_theme;
let theme;
try { theme = localStorage.getItem('mdbook-theme'); } catch(e) { }
if (theme === null || theme === undefined) { theme = default_theme; }
const html = document.documentElement;
html.classList.remove('light')
html.classList.add(theme);
html.classList.add("js");
</script>
<input type="checkbox" id="sidebar-toggle-anchor" class="hidden">
<!-- Hide / unhide sidebar before it is displayed -->
<script>
let sidebar = null;
const sidebar_toggle = document.getElementById("sidebar-toggle-anchor");
if (document.body.clientWidth >= 1080) {
try { sidebar = localStorage.getItem('mdbook-sidebar'); } catch(e) { }
sidebar = sidebar || 'visible';
} else {
sidebar = 'hidden';
}
sidebar_toggle.checked = sidebar === 'visible';
html.classList.remove('sidebar-visible');
html.classList.add("sidebar-" + sidebar);
</script>
<nav id="sidebar" class="sidebar" aria-label="Table of contents">
<!-- populated by js -->
<mdbook-sidebar-scrollbox class="sidebar-scrollbox"></mdbook-sidebar-scrollbox>
<noscript>
<iframe class="sidebar-iframe-outer" src="../toc.html"></iframe>
</noscript>
<div id="sidebar-resize-handle" class="sidebar-resize-handle">
<div class="sidebar-resize-indicator"></div>
</div>
</nav>
<div id="page-wrapper" class="page-wrapper">
<div class="page">
<div id="menu-bar-hover-placeholder"></div>
<div id="menu-bar" class="menu-bar sticky">
<div class="left-buttons">
<label id="sidebar-toggle" class="icon-button" for="sidebar-toggle-anchor" title="Toggle Table of Contents" aria-label="Toggle Table of Contents" aria-controls="sidebar">
<i class="fa fa-bars"></i>
</label>
<button id="theme-toggle" class="icon-button" type="button" title="Change theme" aria-label="Change theme" aria-haspopup="true" aria-expanded="false" aria-controls="theme-list">
<i class="fa fa-paint-brush"></i>
</button>
<ul id="theme-list" class="theme-popup" aria-label="Themes" role="menu">
<li role="none"><button role="menuitem" class="theme" id="default_theme">Auto</button></li>
<li role="none"><button role="menuitem" class="theme" id="light">Light</button></li>
<li role="none"><button role="menuitem" class="theme" id="rust">Rust</button></li>
<li role="none"><button role="menuitem" class="theme" id="coal">Coal</button></li>
<li role="none"><button role="menuitem" class="theme" id="navy">Navy</button></li>
<li role="none"><button role="menuitem" class="theme" id="ayu">Ayu</button></li>
</ul>
<button id="search-toggle" class="icon-button" type="button" title="Search. (Shortkey: s)" aria-label="Toggle Searchbar" aria-expanded="false" aria-keyshortcuts="S" aria-controls="searchbar">
<i class="fa fa-search"></i>
</button>
</div>
<h1 class="menu-title">Rust Compiler Development Guide</h1>
<div class="right-buttons">
<a href="../print.html" title="Print this book" aria-label="Print this book">
<i id="print-button" class="fa fa-print"></i>
</a>
<a href="https://github.com/rust-lang/rustc-dev-guide" title="Git repository" aria-label="Git repository">
<i id="git-repository-button" class="fa fa-github"></i>
</a>
<a href="https://github.com/rust-lang/rustc-dev-guide/edit/master/src/traits/lowering-to-logic.md" title="Suggest an edit" aria-label="Suggest an edit">
<i id="git-edit-button" class="fa fa-edit"></i>
</a>
</div>
</div>
<div id="search-wrapper" class="hidden">
<form id="searchbar-outer" class="searchbar-outer">
<input type="search" id="searchbar" name="searchbar" placeholder="Search this book ..." aria-controls="searchresults-outer" aria-describedby="searchresults-header">
</form>
<div id="searchresults-outer" class="searchresults-outer hidden">
<div id="searchresults-header" class="searchresults-header"></div>
<ul id="searchresults">
</ul>
</div>
</div>
<!-- Apply ARIA attributes after the sidebar and the sidebar toggle button are added to the DOM -->
<script>
document.getElementById('sidebar-toggle').setAttribute('aria-expanded', sidebar === 'visible');
document.getElementById('sidebar').setAttribute('aria-hidden', sidebar !== 'visible');
Array.from(document.querySelectorAll('#sidebar a')).forEach(function(link) {
link.setAttribute('tabIndex', sidebar === 'visible' ? 0 : -1);
});
</script>
<div id="content" class="content">
<main>
<h1 id="lowering-to-logic"><a class="header" href="#lowering-to-logic">Lowering to logic</a></h1>
<ul>
<li><a href="#rust-traits-and-logic">Rust traits and logic</a></li>
<li><a href="#type-checking-normal-functions">Type-checking normal functions</a></li>
<li><a href="#type-checking-generic-functions-beyond-horn-clauses">Type-checking generic functions: beyond Horn clauses</a></li>
<li><a href="#source">Source</a></li>
</ul>
<p>The key observation here is that the Rust trait system is basically a
kind of logic, and it can be mapped onto standard logical inference
rules. We can then look for solutions to those inference rules in a
very similar fashion to how e.g. a <a href="https://en.wikipedia.org/wiki/Prolog">Prolog</a> solver works. It turns out
that we can't <em>quite</em> use Prolog rules (also called Horn clauses) but
rather need a somewhat more expressive variant.</p>
<h2 id="rust-traits-and-logic"><a class="header" href="#rust-traits-and-logic">Rust traits and logic</a></h2>
<p>One of the first observations is that the Rust trait system is
basically a kind of logic. As such, we can map our struct, trait, and
impl declarations into logical inference rules. For the most part,
these are basically Horn clauses, though we'll see that to capture the
full richness of Rust – and in particular to support generic
programming – we have to go a bit further than standard Horn clauses.</p>
<p>To see how this mapping works, let's start with an example. Imagine
we declare a trait and a few impls, like so:</p>
<pre><pre class="playground"><code class="language-rust"><span class="boring">#![allow(unused)]
</span><span class="boring">fn main() {
</span>trait Clone { }
impl Clone for usize { }
impl&lt;T&gt; Clone for Vec&lt;T&gt; where T: Clone { }
<span class="boring">}</span></code></pre></pre>
<p>We could map these declarations to some Horn clauses, written in a
Prolog-like notation, as follows:</p>
<pre><code class="language-text">Clone(usize).
Clone(Vec&lt;?T&gt;) :- Clone(?T).
// The notation `A :- B` means "A is true if B is true".
// Or, put another way, B implies A.
</code></pre>
<p>In Prolog terms, we might say that <code>Clone(Foo)</code> – where <code>Foo</code> is some
Rust type – is a <em>predicate</em> that represents the idea that the type
<code>Foo</code> implements <code>Clone</code>. These rules are <strong>program clauses</strong>; they
state the conditions under which that predicate can be proven (i.e.,
considered true). So the first rule just says "Clone is implemented
for <code>usize</code>". The next rule says "for any type <code>?T</code>, Clone is
implemented for <code>Vec&lt;?T&gt;</code> if clone is implemented for <code>?T</code>". So
e.g. if we wanted to prove that <code>Clone(Vec&lt;Vec&lt;usize&gt;&gt;)</code>, we would do
so by applying the rules recursively:</p>
<ul>
<li><code>Clone(Vec&lt;Vec&lt;usize&gt;&gt;)</code> is provable if:
<ul>
<li><code>Clone(Vec&lt;usize&gt;)</code> is provable if:
<ul>
<li><code>Clone(usize)</code> is provable. (Which it is, so we're all good.)</li>
</ul>
</li>
</ul>
</li>
</ul>
<p>But now suppose we tried to prove that <code>Clone(Vec&lt;Bar&gt;)</code>. This would
fail (after all, I didn't give an impl of <code>Clone</code> for <code>Bar</code>):</p>
<ul>
<li><code>Clone(Vec&lt;Bar&gt;)</code> is provable if:
<ul>
<li><code>Clone(Bar)</code> is provable. (But it is not, as there are no applicable rules.)</li>
</ul>
</li>
</ul>
<p>We can easily extend the example above to cover generic traits with
more than one input type. So imagine the <code>Eq&lt;T&gt;</code> trait, which declares
that <code>Self</code> is equatable with a value of type <code>T</code>:</p>
<pre><code class="language-rust ignore">trait Eq&lt;T&gt; { ... }
impl Eq&lt;usize&gt; for usize { }
impl&lt;T: Eq&lt;U&gt;&gt; Eq&lt;Vec&lt;U&gt;&gt; for Vec&lt;T&gt; { }</code></pre>
<p>That could be mapped as follows:</p>
<pre><code class="language-text">Eq(usize, usize).
Eq(Vec&lt;?T&gt;, Vec&lt;?U&gt;) :- Eq(?T, ?U).
</code></pre>
<p>So far so good.</p>
<h2 id="type-checking-normal-functions"><a class="header" href="#type-checking-normal-functions">Type-checking normal functions</a></h2>
<p>OK, now that we have defined some logical rules that are able to
express when traits are implemented and to handle associated types,
let's turn our focus a bit towards <strong>type-checking</strong>. Type-checking is
interesting because it is what gives us the goals that we need to
prove. That is, everything we've seen so far has been about how we
derive the rules by which we can prove goals from the traits and impls
in the program; but we are also interested in how to derive the goals
that we need to prove, and those come from type-checking.</p>
<p>Consider type-checking the function <code>foo()</code> here:</p>
<pre><code class="language-rust ignore">fn foo() { bar::&lt;usize&gt;() }
fn bar&lt;U: Eq&lt;U&gt;&gt;() { }</code></pre>
<p>This function is very simple, of course: all it does is to call
<code>bar::&lt;usize&gt;()</code>. Now, looking at the definition of <code>bar()</code>, we can see
that it has one where-clause <code>U: Eq&lt;U&gt;</code>. So, that means that <code>foo()</code> will
have to prove that <code>usize: Eq&lt;usize&gt;</code> in order to show that it can call <code>bar()</code>
with <code>usize</code> as the type argument.</p>
<p>If we wanted, we could write a Prolog predicate that defines the
conditions under which <code>bar()</code> can be called. We'll say that those
conditions are called being "well-formed":</p>
<pre><code class="language-text">barWellFormed(?U) :- Eq(?U, ?U).
</code></pre>
<p>Then we can say that <code>foo()</code> type-checks if the reference to
<code>bar::&lt;usize&gt;</code> (that is, <code>bar()</code> applied to the type <code>usize</code>) is
well-formed:</p>
<pre><code class="language-text">fooTypeChecks :- barWellFormed(usize).
</code></pre>
<p>If we try to prove the goal <code>fooTypeChecks</code>, it will succeed:</p>
<ul>
<li><code>fooTypeChecks</code> is provable if:
<ul>
<li><code>barWellFormed(usize)</code>, which is provable if:
<ul>
<li><code>Eq(usize, usize)</code>, which is provable because of an impl.</li>
</ul>
</li>
</ul>
</li>
</ul>
<p>Ok, so far so good. Let's move on to type-checking a more complex function.</p>
<h2 id="type-checking-generic-functions-beyond-horn-clauses"><a class="header" href="#type-checking-generic-functions-beyond-horn-clauses">Type-checking generic functions: beyond Horn clauses</a></h2>
<p>In the last section, we used standard Prolog horn-clauses (augmented with Rust's
notion of type equality) to type-check some simple Rust functions. But that only
works when we are type-checking non-generic functions. If we want to type-check
a generic function, it turns out we need a stronger notion of goal than what Prolog
can provide. To see what I'm talking about, let's revamp our previous
example to make <code>foo</code> generic:</p>
<pre><code class="language-rust ignore">fn foo&lt;T: Eq&lt;T&gt;&gt;() { bar::&lt;T&gt;() }
fn bar&lt;U: Eq&lt;U&gt;&gt;() { }</code></pre>
<p>To type-check the body of <code>foo</code>, we need to be able to hold the type
<code>T</code> "abstract". That is, we need to check that the body of <code>foo</code> is
type-safe <em>for all types <code>T</code></em>, not just for some specific type. We might express
this like so:</p>
<pre><code class="language-text">fooTypeChecks :-
// for all types T...
forall&lt;T&gt; {
// ...if we assume that Eq(T, T) is provable...
if (Eq(T, T)) {
// ...then we can prove that `barWellFormed(T)` holds.
barWellFormed(T)
}
}.
</code></pre>
<p>This notation I'm using here is the notation I've been using in my
prototype implementation; it's similar to standard mathematical
notation but a bit Rustified. Anyway, the problem is that standard
Horn clauses don't allow universal quantification (<code>forall</code>) or
implication (<code>if</code>) in goals (though many Prolog engines do support
them, as an extension). For this reason, we need to accept something
called "first-order hereditary harrop" (FOHH) clauses – this long
name basically means "standard Horn clauses with <code>forall</code> and <code>if</code> in
the body". But it's nice to know the proper name, because there is a
lot of work describing how to efficiently handle FOHH clauses; see for
example Gopalan Nadathur's excellent
<a href="https://rust-lang.github.io/chalk/book/bibliography.html#pphhf">"A Proof Procedure for the Logic of Hereditary Harrop Formulas"</a>
in <a href="https://rust-lang.github.io/chalk/book/bibliography.html">the bibliography of Chalk Book</a>.</p>
<p>It turns out that supporting FOHH is not really all that hard. And
once we are able to do that, we can easily describe the type-checking
rule for generic functions like <code>foo</code> in our logic.</p>
<h2 id="source"><a class="header" href="#source">Source</a></h2>
<p>This page is a lightly adapted version of a
<a href="http://smallcultfollowing.com/babysteps/blog/2017/01/26/lowering-rust-traits-to-logic/">blog post by Nicholas Matsakis</a>.</p>
</main>
<nav class="nav-wrapper" aria-label="Page navigation">
<!-- Mobile navigation buttons -->
<a rel="prev" href="../traits/chalk.html" class="mobile-nav-chapters previous" title="Previous chapter" aria-label="Previous chapter" aria-keyshortcuts="Left">
<i class="fa fa-angle-left"></i>
</a>
<a rel="next prefetch" href="../traits/goals-and-clauses.html" class="mobile-nav-chapters next" title="Next chapter" aria-label="Next chapter" aria-keyshortcuts="Right">
<i class="fa fa-angle-right"></i>
</a>
<div style="clear: both"></div>
</nav>
</div>
</div>
<nav class="nav-wide-wrapper" aria-label="Page navigation">
<a rel="prev" href="../traits/chalk.html" class="nav-chapters previous" title="Previous chapter" aria-label="Previous chapter" aria-keyshortcuts="Left">
<i class="fa fa-angle-left"></i>
</a>
<a rel="next prefetch" href="../traits/goals-and-clauses.html" class="nav-chapters next" title="Next chapter" aria-label="Next chapter" aria-keyshortcuts="Right">
<i class="fa fa-angle-right"></i>
</a>
</nav>
</div>
<script>
window.playground_copyable = true;
</script>
<script src="../elasticlunr.min.js"></script>
<script src="../mark.min.js"></script>
<script src="../searcher.js"></script>
<script src="../clipboard.min.js"></script>
<script src="../highlight.js"></script>
<script src="../book.js"></script>
<!-- Custom JS scripts -->
<script src="../mermaid.min.js"></script>
<script src="../mermaid-init.js"></script>
</div>
</body>
</html>
Reference in New Issue View Git Blame Copy Permalink