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
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
|
<!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">Home</a>
<span>/</span>
<a href="/posts" class="post-end-link">Posts</a>
<span>/</span>
<a class="post-end-link">Turing Complete Type Systems</a>
<a class="stats post-end-link" href="https://git.peppe.rs/web/site/plain/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.19
</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>
</div>
<p>I'm Akshay, programmer and pixel-artist.</p>
<p>
I write <a href="https://git.peppe.rs">open-source stuff</a> to pass time.
I also design fonts:
<a href="https://git.peppe.rs/fonts/scientifica/about">scientifica</a>,
<a href="https://git.peppe.rs/fonts/curie/about">curie</a>.
</p>
<p>Send me a mail at [email protected] or a message at [email protected].</p>
</div>
<a href="/" class="post-end-link">Home</a>
<span>/</span>
<a href="/posts" class="post-end-link">Posts</a>
<span>/</span>
<a class="post-end-link">Turing Complete Type Systems</a>
<a class="stats post-end-link" href="https://git.peppe.rs/web/site/plain/posts/turing_complete_type_systems.md
">View Raw</a>
</div>
</div>
</body>
</html>
|
