1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
|
<!DOCTYPE html>
<html lang="en">
<head>
<link rel="stylesheet" href="/style.css">
<link rel="stylesheet" href="/syntax.css">
<meta charset="UTF-8">
<meta name="viewport" content="initial-scale=1">
<meta content="#ffffff" name="theme-color">
<meta name="HandheldFriendly" content="true">
<meta property="og:title" content="Turing Complete Type Systems">
<meta property="og:type" content="website">
<meta property="og:description" content="a static site {for, by, about} me ">
<meta property="og:url" content="https://peppe.rs">
<link rel="icon" type="image/x-icon" href="/favicon.png">
<title>Turing Complete Type Systems · peppe.rs</title>
<body>
<div class="posts">
<div class="post">
<a href="/" class="post-end-link">⟵ Back</a>
<a class="stats post-end-link" href="https://raw.githubusercontent.com/nerdypepper/site/master/posts/turing_complete_type_systems.md
">View Raw</a>
<div class="separator"></div>
<div class="date">
18/06 — 2020
<div class="stats">
<span class="stats-number">
9.18
</span>
<span class="stats-unit">cm</span>
 
<span class="stats-number">
0.9
</span>
<span class="stats-unit">min</span>
</div>
</div>
<h1>
Turing Complete Type Systems
</h1>
<div class="post-text">
<p>Rust’s type system is Turing complete:</p>
<ul>
<li><a href="https://github.com/doctorn/trait-eval/">FizzBuzz with Rust Traits</a></li>
<li><a href="https://github.com/Ashymad/fortraith">A Forth implementation with Rust Traits</a></li>
</ul>
<p>It is impossible to determine if a program written in a generally Turing complete system will ever stop. That is, it is impossible to write a program <code>f</code> that determines if a program <code>g</code>, where <code>g</code> is written in a Turing complete programming language, will ever halt. The <a href="https://en.wikipedia.org/wiki/Halting_problem">Halting Problem</a> is in fact, an <a href="https://en.wikipedia.org/wiki/Undecidable_problem">undecidable problem</a>.</p>
<p><em>How is any of this relevant?</em></p>
<p>Rust performs compile-time type inference. The type checker, in turn, compiles and infers types, I would describe it as a compiler inside a compiler. It is possible that <code>rustc</code> may never finish compiling your Rust program! I lied, <code>rustc</code> stops after a while, after hitting the recursion limit.</p>
<p>I understand that this post lacks content.</p>
</div>
<div class=intro>
Hi.
<div class=hot-links>
<a href=https://peppe.rs/index.xml class=feed-button>Subscribe</a>
<a href=https://liberapay.com/nerdypepper/donate class=donate-button>Donate</a>
</div>
<p>I'm Akshay, I go by nerd or nerdypepper on the internet.</p>
<p>
I am a compsci undergrad, Rust programmer and an enthusiastic Vimmer.
I write open-source stuff to pass time. I also design fonts: scientifica, curie.
</p>
<p>Send me a mail at [email protected] or a message at [email protected].</p>
</div>
<a href="/" class="post-end-link">⟵ Back</a>
<a class="stats post-end-link" href="https://raw.githubusercontent.com/nerdypepper/site/master/posts/turing_complete_type_systems.md
">View Raw</a>
</div>
</div>
</body>
</html>
|