traits/lowering-to-logic.html - rust-lang/rustc-dev-guide - Git at Google

 <!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 -->
         <link rel="stylesheet" href="../pagetoc.css">


         <!-- Provide site root and default themes to javascript -->
         <script>
             const path_to_root = "../";
             const default_light_theme = "light";
             const default_dark_theme = "navy";
             window.path_to_searchindex_js = "../searchindex.js";
         </script>
         <!-- Start loading toc.js asap -->
         <script src="../toc.js"></script>
     </head>
     <body>
     <div id="mdbook-help-container">
         <div id="mdbook-help-popup">
             <h2 class="mdbook-help-title">Keyboard shortcuts</h2>
             <div>
                 <p>Press <kbd>←</kbd> or <kbd>→</kbd> to navigate between chapters</p>
                 <p>Press <kbd>S</kbd> or <kbd>/</kbd> to search in the book</p>
                 <p>Press <kbd>?</kbd> to show this help</p>
                 <p>Press <kbd>Esc</kbd> to hide this help</p>
             </div>
         </div>
     </div>
     <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 = false;
             }
             if (sidebar === 'visible') {
                 sidebar_toggle.checked = true;
             } else {
                 html.classList.remove('sidebar-visible');
             }
         </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 (`/`)" 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/main/src/traits/lowering-to-logic.md" title="Suggest an edit" aria-label="Suggest an edit" rel="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">
                         <div class="search-wrapper">
                             <input type="search" id="searchbar" name="searchbar" placeholder="Search this book ..." aria-controls="searchresults-outer" aria-describedby="searchresults-header">
                             <div class="spinner-wrapper">
                                 <i class="fa fa-spinner fa-spin"></i>
                             </div>
                         </div>
                     </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>
 <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>
         <script src="../pagetoc.js"></script>


     </div>
     </body>
 </html>
	<!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 -->
	<link rel="stylesheet" href="../pagetoc.css">


	<!-- Provide site root and default themes to javascript -->
	<script>
	const path_to_root = "../";
	const default_light_theme = "light";
	const default_dark_theme = "navy";
	window.path_to_searchindex_js = "../searchindex.js";
	</script>
	<!-- Start loading toc.js asap -->
	<script src="../toc.js"></script>
	</head>
	<body>
	<div id="mdbook-help-container">
	<div id="mdbook-help-popup">
	<h2 class="mdbook-help-title">Keyboard shortcuts</h2>
	<div>
	<p>Press <kbd>←</kbd> or <kbd>→</kbd> to navigate between chapters</p>
	<p>Press <kbd>S</kbd> or <kbd>/</kbd> to search in the book</p>
	<p>Press <kbd>?</kbd> to show this help</p>
	<p>Press <kbd>Esc</kbd> to hide this help</p>
	</div>
	</div>
	</div>
	<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 = false;
	}
	if (sidebar === 'visible') {
	sidebar_toggle.checked = true;
	} else {
	html.classList.remove('sidebar-visible');
	}
	</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 (`/`)" 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/main/src/traits/lowering-to-logic.md" title="Suggest an edit" aria-label="Suggest an edit" rel="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">
	<div class="search-wrapper">
	<input type="search" id="searchbar" name="searchbar" placeholder="Search this book ..." aria-controls="searchresults-outer" aria-describedby="searchresults-header">
	<div class="spinner-wrapper">
	<i class="fa fa-spinner fa-spin"></i>
	</div>
	</div>
	</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>
	<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<T> Clone for Vec<T> 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<?T>) :- 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<?T></code> if clone is implemented for <code>?T</code>". So
	e.g. if we wanted to prove that <code>Clone(Vec<Vec<usize>>)</code>, we would do
	so by applying the rules recursively:</p>
	<ul>
	<li><code>Clone(Vec<Vec<usize>>)</code> is provable if:
	<ul>
	<li><code>Clone(Vec<usize>)</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<Bar>)</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<Bar>)</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<T></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<T> { ... }
	impl Eq<usize> for usize { }
	impl<T: Eq<U>> Eq<Vec<U>> for Vec<T> { }</code></pre>
	<p>That could be mapped as follows:</p>
	<pre><code class="language-text">Eq(usize, usize).
	Eq(Vec<?T>, Vec<?U>) :- 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::<usize>() }
	fn bar<U: Eq<U>>() { }</code></pre>
	<p>This function is very simple, of course: all it does is to call
	<code>bar::<usize>()</code>. Now, looking at the definition of <code>bar()</code>, we can see
	that it has one where-clause <code>U: Eq<U></code>. So, that means that <code>foo()</code> will
	have to prove that <code>usize: Eq<usize></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::<usize></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<T: Eq<T>>() { bar::<T>() }
	fn bar<U: Eq<U>>() { }</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<T> {
	// ...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>
	<script src="../pagetoc.js"></script>



	</div>
	</body>
	</html>