From 1df315612a2fb3847de394987884f540a3e96df7 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Mon, 13 May 2024 19:08:17 -0700 Subject: [PATCH] Update "typesafe interpreter" article to new math delimiters Signed-off-by: Danila Fedorin --- content/blog/typesafe_interpreter_revisited.md | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/content/blog/typesafe_interpreter_revisited.md b/content/blog/typesafe_interpreter_revisited.md index dc5a50d..30da782 100644 --- a/content/blog/typesafe_interpreter_revisited.md +++ b/content/blog/typesafe_interpreter_revisited.md @@ -130,16 +130,16 @@ to values of the types. 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 -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 -\\(A\\) and \\(B\\). +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 +\(A\) and \(B\). * `Either A B`, which contains one of `A` or `B`, is equivalent -to the proposition \\(A \lor B\\), which means \\(A\\) or \\(B\\). -Intuitively, to provide a proof that either \\(A\\) or \\(B\\) +to the proposition \(A \lor B\), which means \(A\) or \(B\). +Intuitively, to provide a proof that either \(A\) or \(B\) is true, we need to provide one of them. * `A -> B`, the type of a function from `A` to `B`, is equivalent -to the proposition \\(A \rightarrow B\\), which reads \\(A\\) -implies \\(B\\). We can think of a function `A -> B` as creating +to the proposition \(A \rightarrow B\), which reads \(A\) +implies \(B\). We can think of a function `A -> B` as creating a proof of `B` given a proof of `A`. Now, consider Idris' unit type `()`: @@ -150,7 +150,7 @@ data () = () 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 `()`. -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. 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 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` -is equivalent to \\(\\text{false}\\). +is equivalent to \(\text{false}\). Finally, we get to a more complicated example: