Web-Projects/blog-static
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Update "typesafe interpreter" article to new math delimiters

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-05-13 19:08:17 -07:00
parent 15beddf96b
commit 1df315612a
1 changed files with 9 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
content/blog/typesafe_interpreter_revisited.md
View File

@ -130,16 +130,16 @@ to values of the types.
To get settled into this idea, let's look at a few 'well-known' examples: To get settled into this idea, let's look at a few 'well-known' examples:
* `(A,B)`, the tuple of two types `A` and `B` is equivalent to the * `(A,B)`, the tuple of two types `A` and `B` is equivalent to the
proposition \\(A \land B\\), which means \\(A\\) and \\(B\\). Intuitively, proposition \(A \land B\), which means \(A\) and \(B\). Intuitively,
to provide a proof of \\(A \land B\\), we have to provide the proofs of to provide a proof of \(A \land B\), we have to provide the proofs of
\\(A\\) and \\(B\\). \(A\) and \(B\).
* `Either A B`, which contains one of `A` or `B`, is equivalent * `Either A B`, which contains one of `A` or `B`, is equivalent
to the proposition \\(A \lor B\\), which means \\(A\\) or \\(B\\). to the proposition \(A \lor B\), which means \(A\) or \(B\).
Intuitively, to provide a proof that either \\(A\\) or \\(B\\) Intuitively, to provide a proof that either \(A\) or \(B\)
is true, we need to provide one of them. is true, we need to provide one of them.
* `A -> B`, the type of a function from `A` to `B`, is equivalent * `A -> B`, the type of a function from `A` to `B`, is equivalent
to the proposition \\(A \rightarrow B\\), which reads \\(A\\) to the proposition \(A \rightarrow B\), which reads \(A\)
implies \\(B\\). We can think of a function `A -> B` as creating implies \(B\). We can think of a function `A -> B` as creating
a proof of `B` given a proof of `A`. a proof of `B` given a proof of `A`.
Now, consider Idris' unit type `()`: Now, consider Idris' unit type `()`:
@ -150,7 +150,7 @@ data () = ()
This type takes no arguments, and there's only one way to construct This type takes no arguments, and there's only one way to construct
it. We can create a value of type `()` at any time, by just writing `()`. it. We can create a value of type `()` at any time, by just writing `()`.
This type is equivalent to \\(\\text{true}\\): only one proof of it exists, This type is equivalent to \(\text{true}\): only one proof of it exists,
and it requires no premises. It just is. and it requires no premises. It just is.
Consider also the type `Void`, which too is present in Idris: Consider also the type `Void`, which too is present in Idris:
@ -163,7 +163,7 @@ data Void = -- Nothing
The type `Void` has no constructors: it's impossible The type `Void` has no constructors: it's impossible
to create a value of this type, and therefore, it's to create a value of this type, and therefore, it's
impossible to create a proof of `Void`. Thus, as you may have guessed, `Void` impossible to create a proof of `Void`. Thus, as you may have guessed, `Void`
is equivalent to \\(\\text{false}\\). is equivalent to \(\text{false}\).
Finally, we get to a more complicated example: Finally, we get to a more complicated example: