Compare commits
No commits in common. "b0e501f08652de10d1e91d02151328f8568b46eb" and "068d0218b0fbbbfc6cd200fd0c268b9cdab1e15f" have entirely different histories.
b0e501f086
...
068d0218b0
|
@ -3,7 +3,7 @@ languageCode = "en-us"
|
||||||
title = "Daniel's Blog"
|
title = "Daniel's Blog"
|
||||||
theme = "vanilla"
|
theme = "vanilla"
|
||||||
pygmentsCodeFences = true
|
pygmentsCodeFences = true
|
||||||
pygmentsUseClasses = true
|
pygmentsStyle = "github"
|
||||||
summaryLength = 20
|
summaryLength = 20
|
||||||
|
|
||||||
[markup]
|
[markup]
|
||||||
|
|
|
@ -1,216 +0,0 @@
|
||||||
---
|
|
||||||
title: Meaningfully Typechecking a Language in Idris, With Tuples
|
|
||||||
date: 2020-08-12T15:48:04-07:00
|
|
||||||
tags: ["Idris"]
|
|
||||||
---
|
|
||||||
|
|
||||||
Some time ago, I wrote a post titled
|
|
||||||
[Meaningfully Typechecking a Language in Idris]({{< relref "typesafe_interpreter.md" >}}).
|
|
||||||
I then followed it up with
|
|
||||||
[Meaningfully Typechecking a Language in Idris, Revisited]({{< relref "typesafe_interpreter_revisited.md" >}}).
|
|
||||||
In these posts, I described a hypothetical
|
|
||||||
way of 'typechecking' an expression data type `Expr` into a typesafe form `SafeExpr`.
|
|
||||||
A `SafeExpr` can be evaluated without any code to handle type errors,
|
|
||||||
since it's by definition impossible to construct ill-typed expressions using
|
|
||||||
it. In the first post, we implemented the method only for simple arithmetic
|
|
||||||
expressions; in my latter post, we extended this to support `if`-expressions.
|
|
||||||
Near the end of the post, I made the following comment:
|
|
||||||
|
|
||||||
> When we add polymorphic tuples and lists, we start being able to construct an
|
|
||||||
arbitrary number of types: `[a]`. `[[a]]`, and so on. Then, we cease to be able t
|
|
||||||
enumerate all possible pairs of types, and require a recursive solution. I think
|
|
||||||
that this leads us back to [our method].
|
|
||||||
|
|
||||||
Recently, I thought about this some more, and decided that it's rather simple
|
|
||||||
to add tuples into our little language. The addition of tuples mean that our
|
|
||||||
language will have an infinite number of possible types. We would have
|
|
||||||
`Int`, `(Int, Int)`, `((Int, Int), Int)`, and so on. This would make it
|
|
||||||
impossible to manually test every possible case in our typechecker,
|
|
||||||
but our approach of returning `Dec (a = b)` will work just fine.
|
|
||||||
|
|
||||||
### Extending The Syntax
|
|
||||||
First, let's extend our existing language with expressions for
|
|
||||||
tuples. For simplicity, let's use pairs `(a,b)` instead of general
|
|
||||||
`n`-element tuples. This would make typechecking less cumbersome while still
|
|
||||||
having the interesting effect of making the number of types in our language
|
|
||||||
infinite. We can always represent the 3-element tuple `(a,b,c)` as `((a,b), c)`,
|
|
||||||
after all. To be able to extract values from our pairs, we'll add the `fst` and
|
|
||||||
`snd` functions into our language, which accept a tuple and return its
|
|
||||||
first or second element, respectively.
|
|
||||||
|
|
||||||
Our `Expr` data type, which allows ill-typed expressions, ends up as follows:
|
|
||||||
|
|
||||||
{{< codelines "Idris" "typesafe-interpreter/TypesafeIntrV3.idr" 31 39 "hl_lines=7 8 9" >}}
|
|
||||||
|
|
||||||
I've highlighted the new lines. The additions consist of the `Pair` constructor, which
|
|
||||||
represents the tuple expression `(a, b)`, and the `Fst` and `Snd` constructors,
|
|
||||||
which represent the `fst e` and `snd e` expressions, respectively. In
|
|
||||||
a similar manner, we extend our `SafeExpr` GADT:
|
|
||||||
|
|
||||||
{{< codelines "Idris" "typesafe-interpreter/TypesafeIntrV3.idr" 41 49 "hl_lines=7 8 9" >}}
|
|
||||||
|
|
||||||
Finally, to provide the `PairType` constructor, we extend the `ExprType` and `repr` functions:
|
|
||||||
|
|
||||||
{{< codelines "Idris" "typesafe-interpreter/TypesafeIntrV3.idr" 1 11 "hl_lines=5 11" >}}
|
|
||||||
|
|
||||||
### Implementing Equality
|
|
||||||
An important part of this change is the extension of the `decEq` function,
|
|
||||||
which compares two types for equality. The kind folks over at `#idris` previously
|
|
||||||
recommended the use of the `Dec` data type for this purpose. A value of
|
|
||||||
type `Dec P`
|
|
||||||
{{< sidenote "right" "decideable-note" "is either a proof that \(P\) is true, or a proof that \(P\) is false." >}}
|
|
||||||
It's possible that a proposition \(P\) is not provable, and neither is \(\lnot P\).
|
|
||||||
It is therefore not possible to construct a value of type <code>Dec P</code> for
|
|
||||||
any proposition <code>P</code>. Having a value of type <code>Dec P</code>, then,
|
|
||||||
provides us nontrivial information.
|
|
||||||
{{< /sidenote >}} Our `decEq` function, given two types `a` and `b`, returns
|
|
||||||
`Dec (a = b)`. Thus, it will return either a proof that `a = b` (which we can
|
|
||||||
then use to convince the Idris type system that two `SafeExpr` values are,
|
|
||||||
in fact, of the same type), or a proof of `a = b -> Void` (which tells
|
|
||||||
us that `a` and `b` are definitely not equal). If you're not sure what the deal with `(=)`
|
|
||||||
and `Void` is, check out
|
|
||||||
[this section]({{< relref "typesafe_interpreter_revisited.md" >}}#curry-howard-correspondence)
|
|
||||||
of the previous article.
|
|
||||||
|
|
||||||
A lot of the work in implementing `decEq` went into constructing proofs of falsity.
|
|
||||||
That is, we needed to explicitly list every case like `decEq IntType BoolType`, and create
|
|
||||||
a proof that `IntType` cannot equal `BoolType`. However, here's how we use `decEq` in
|
|
||||||
the typechecking function:
|
|
||||||
|
|
||||||
{{< codelines "Idris" "typesafe-interpreter/TypesafeIntrV2.idr" 76 78 >}}
|
|
||||||
|
|
||||||
We always throw away the proof inequality! So, rather than spending the time
|
|
||||||
constructing useless proofs like this, we can just switch `decEq` to return
|
|
||||||
a `Maybe (a = b)`. The `Just` case will tell us that the two types are equal
|
|
||||||
(and, as before, provide a proof); the `Nothing` case will tell us that
|
|
||||||
the two types are _not_ equal, and provide no further information. Let's
|
|
||||||
see the implementation of `decEq` now:
|
|
||||||
|
|
||||||
{{< codelines "Idris" "typesafe-interpreter/TypesafeIntrV3.idr" 13 23 >}}
|
|
||||||
|
|
||||||
Lines 14 through 16 are pretty simple; in this case, we can tell at a glance
|
|
||||||
that the two types are equal, and Idris can infer an equality proof in
|
|
||||||
the form of `Refl`. We return this proof by writing it in a `Just`.
|
|
||||||
Line 23 is the catch-all case for any combination of types we didn't handle.
|
|
||||||
Any combination of types we don't handle is invalid, and thus, this case
|
|
||||||
returns `Nothing`.
|
|
||||||
|
|
||||||
What about lines 17 through 22? This is the case for handling the equality
|
|
||||||
of two pair types, `(lt1, lt2)` and `(rt1, rt2)`. The equality of the two
|
|
||||||
types depends on the equality of their constituents. That is, if we
|
|
||||||
know that `lt1 = rt1` and `lt2 = rt2`, we know that the two pair types
|
|
||||||
are also equal. If one of the two equalities doesn't hold, the two
|
|
||||||
pairs obviously aren't equal, and thus, we should return `Nothing`.
|
|
||||||
This should remind us of `Maybe`'s monadic nature: we can first compute
|
|
||||||
`decEq lt1 rt1`, and then, if it succeeds, compute `decEq lt2 rt2`.
|
|
||||||
If both succeed, we will have in hand the two proofs, `lt1 = rt1`
|
|
||||||
and `lt2 = rt2`. We achieve this effect using `do`-notation,
|
|
||||||
storing the sub-proofs into `subEq1` and `subEq2`.
|
|
||||||
|
|
||||||
What now? Once again, we have to use `replace`. Recall its type:
|
|
||||||
|
|
||||||
```Idris
|
|
||||||
replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Type} -> x = y -> P x -> P y
|
|
||||||
```
|
|
||||||
|
|
||||||
Given some proposition in terms of `a`, and knowing that `a = b`, `replace`
|
|
||||||
returns the original proposition, but now in terms of `b`. We know for sure
|
|
||||||
that:
|
|
||||||
|
|
||||||
```Idris
|
|
||||||
PairType lt1 lt2 = PairType lt1 lt2
|
|
||||||
```
|
|
||||||
|
|
||||||
We can start from there. Let's handle one thing at a time, and try
|
|
||||||
to replace the second `lt1` with `rt1`. Then, we can replace the second
|
|
||||||
`lt2` with `rt2`, and we'll have our equality!
|
|
||||||
|
|
||||||
Easier said than done, though. How do we tell Idris which `lt1`
|
|
||||||
we want to substitute? After all, of the following are possible:
|
|
||||||
|
|
||||||
```Idris
|
|
||||||
PairType rt1 lt2 = PairType lt1 lt2 -- First lt1 replaced
|
|
||||||
PairType lt1 lt2 = PairType rt1 lt2 -- Second lt1 replaced
|
|
||||||
PairType rt1 lt2 = PairType rt1 lt2 -- Both replaced
|
|
||||||
```
|
|
||||||
|
|
||||||
The key is in the signature, specifically the expressions `P x` and `P y`.
|
|
||||||
We can think of `P` as a function, and of `replace` as creating a value
|
|
||||||
of `P` applied to another argument. Thus, the substitution will occur
|
|
||||||
exactly where the argument of `P` is used. Then, to achieve each
|
|
||||||
of the above substitution, we can write `P` as follows:
|
|
||||||
|
|
||||||
```Idris {linenos=table, hl_lines=[2]}
|
|
||||||
t1 => PairType t1 lt2 = PairType lt1 lt2
|
|
||||||
t1 => PairType lt1 lt2 = PairType t1 lt2
|
|
||||||
t1 => PairType t1 lt2 = PairType t1 lt2
|
|
||||||
```
|
|
||||||
|
|
||||||
The second function (highlighted) is the one we'll need to use to attain
|
|
||||||
the desired result. Since `P` is an implicit argument to `replace`,
|
|
||||||
we can explicitly provide it with `{P=...}`, leading to the following
|
|
||||||
line:
|
|
||||||
|
|
||||||
{{< codelines "Idris" "typesafe-interpreter/TypesafeIntrV3.idr" 20 20>}}
|
|
||||||
|
|
||||||
We now have a proof of the following proposition:
|
|
||||||
|
|
||||||
```Idris
|
|
||||||
PairType lt1 lt2 = PairType rt1 lt2
|
|
||||||
```
|
|
||||||
|
|
||||||
We want to replace the second `lt2` with `rt2`, which means that we
|
|
||||||
write our `P` as follows:
|
|
||||||
|
|
||||||
```Idris
|
|
||||||
t2 => PairType lt1 lt2 = PairType rt1 t2
|
|
||||||
```
|
|
||||||
|
|
||||||
Finally, we perform the second replacement, and return the result:
|
|
||||||
|
|
||||||
{{< codelines "Idris" "typesafe-interpreter/TypesafeIntrV3.idr" 21 22 >}}
|
|
||||||
|
|
||||||
Great! We have finished implement `decEq`.
|
|
||||||
|
|
||||||
### Adjusting The Typechecker
|
|
||||||
It's time to make our typechecker work with tuples.
|
|
||||||
First, we need to fix the `IfElse` case to accept `Maybe (a=b)` instead
|
|
||||||
of `Dec (a=b)`:
|
|
||||||
|
|
||||||
{{< codelines "Idris" "typesafe-interpreter/TypesafeIntrV3.idr" 71 78 "hl_lines=7 8" >}}
|
|
||||||
|
|
||||||
Note that the only change is from `Dec` to `Maybe`; we didn't need to add new cases
|
|
||||||
or even to know what sort of types are available in the language.
|
|
||||||
|
|
||||||
Next, we can write the cases for the new expressions in our language. We can
|
|
||||||
start with `Pair`, which, given expressions of types `a` and `b`, creates
|
|
||||||
an expression of type `(a,b)`. As long as the arguments to `Pair` are well-typed,
|
|
||||||
so is the `Pair` expression itself; thus, there are no errors to handle.
|
|
||||||
|
|
||||||
{{< codelines "Idris" "typesafe-interpreter/TypesafeIntrV3.idr" 79 83 >}}
|
|
||||||
|
|
||||||
The case for `Fst` is more complicated. If the argument to `Fst` is a tuple
|
|
||||||
of type `(a, b)`, then `Fst` constructs from it an expression
|
|
||||||
of type `a`. Otherwise, the expression is ill-typed, and we return an error.
|
|
||||||
|
|
||||||
{{< codelines "Idris" "typesafe-interpreter/TypesafeIntrV3.idr" 84 89 >}}
|
|
||||||
|
|
||||||
The case for `Snd` is very similar:
|
|
||||||
|
|
||||||
{{< codelines "Idris" "typesafe-interpreter/TypesafeIntrV3.idr" 90 96 >}}
|
|
||||||
|
|
||||||
### Evaluation Function and Conclusion
|
|
||||||
We conclude with our final `eval` and `resultStr` functions,
|
|
||||||
which now look as follows.
|
|
||||||
|
|
||||||
{{< codelines "Idris" "typesafe-interpreter/TypesafeIntrV3.idr" 97 111 "hl_lines=7-9 13-15" >}}
|
|
||||||
|
|
||||||
As you can see, we require no error handling in `eval`; the expressions returned by
|
|
||||||
`typecheck` are guaranteed to evaluate to valid Idris values. We have achieved our goal,
|
|
||||||
with very little changes to `typecheck` other than the addition of new language
|
|
||||||
constructs. In my opinion, this is a win!
|
|
||||||
|
|
||||||
As always, you can see the code on my Git server. Here's
|
|
||||||
[the latest Idris file,](https://dev.danilafe.com/Web-Projects/blog-static/src/branch/master/code/typesafe-interpreter/TypesafeIntrV3.idr)
|
|
||||||
if you want to check it out (and maybe verify that it compiles). I hope you found
|
|
||||||
this interesting!
|
|
|
@ -1,78 +0,0 @@
|
||||||
@import "variables.scss";
|
|
||||||
|
|
||||||
$code-color-lineno: grey;
|
|
||||||
$code-color-keyword: black;
|
|
||||||
$code-color-type: black;
|
|
||||||
$code-color-comment: grey;
|
|
||||||
|
|
||||||
code {
|
|
||||||
font-family: $font-code;
|
|
||||||
background-color: $code-color;
|
|
||||||
border: $code-border;
|
|
||||||
padding: 0 0.25rem 0 0.25rem;
|
|
||||||
}
|
|
||||||
|
|
||||||
pre code {
|
|
||||||
display: block;
|
|
||||||
box-sizing: border-box;
|
|
||||||
padding: 0.5rem;
|
|
||||||
overflow: auto;
|
|
||||||
}
|
|
||||||
|
|
||||||
.chroma {
|
|
||||||
.lntable {
|
|
||||||
border-spacing: 0;
|
|
||||||
padding: 0.5rem 0 0.5rem 0;
|
|
||||||
background-color: $code-color;
|
|
||||||
border-radius: 0;
|
|
||||||
border: $code-border;
|
|
||||||
display: block;
|
|
||||||
overflow: auto;
|
|
||||||
|
|
||||||
td {
|
|
||||||
padding: 0;
|
|
||||||
}
|
|
||||||
|
|
||||||
code {
|
|
||||||
border: none;
|
|
||||||
padding: 0;
|
|
||||||
}
|
|
||||||
|
|
||||||
pre {
|
|
||||||
margin: 0;
|
|
||||||
}
|
|
||||||
|
|
||||||
.lntd:last-child {
|
|
||||||
width: 100%;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
.lntr {
|
|
||||||
display: table-row;
|
|
||||||
}
|
|
||||||
|
|
||||||
.lnt {
|
|
||||||
display: block;
|
|
||||||
padding: 0 1rem 0 1rem;
|
|
||||||
color: $code-color-lineno;
|
|
||||||
}
|
|
||||||
|
|
||||||
.hl {
|
|
||||||
display: block;
|
|
||||||
background-color: #fffd99;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
.kr, .k {
|
|
||||||
font-weight: bold;
|
|
||||||
color: $code-color-keyword;
|
|
||||||
}
|
|
||||||
|
|
||||||
.kt {
|
|
||||||
font-weight: bold;
|
|
||||||
color: $code-color-type;
|
|
||||||
}
|
|
||||||
|
|
||||||
.c, .c1 {
|
|
||||||
color: $code-color-comment;
|
|
||||||
}
|
|
|
@ -31,6 +31,35 @@ h1, h2, h3, h4, h5, h6 {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
code {
|
||||||
|
font-family: $font-code;
|
||||||
|
background-color: $code-color;
|
||||||
|
}
|
||||||
|
|
||||||
|
pre code {
|
||||||
|
display: block;
|
||||||
|
padding: 0.5rem;
|
||||||
|
overflow-x: auto;
|
||||||
|
border: $code-border;
|
||||||
|
}
|
||||||
|
|
||||||
|
div.highlight table {
|
||||||
|
border: $code-border !important;
|
||||||
|
border-radius: 0px;
|
||||||
|
|
||||||
|
pre {
|
||||||
|
margin: 0;
|
||||||
|
}
|
||||||
|
|
||||||
|
code {
|
||||||
|
border: none;
|
||||||
|
}
|
||||||
|
|
||||||
|
span {
|
||||||
|
margin: 0 !important;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
.container {
|
.container {
|
||||||
position: relative;
|
position: relative;
|
||||||
margin: auto;
|
margin: auto;
|
||||||
|
|
|
@ -6,16 +6,14 @@
|
||||||
<meta name="description" content="{{ .Description }}">
|
<meta name="description" content="{{ .Description }}">
|
||||||
{{ end }}
|
{{ end }}
|
||||||
|
|
||||||
<link rel="stylesheet" href="https://fonts.googleapis.com/css2?family=Inconsolata:wght@400;700&family=Raleway&family=Lora&display=block" media="screen">
|
<link rel="stylesheet" href="https://fonts.googleapis.com/css2?family=Inconsolata&family=Raleway&family=Lora&display=block" media="screen">
|
||||||
<link rel="stylesheet" href="//cdnjs.cloudflare.com/ajax/libs/normalize/5.0.0/normalize.min.css" media="screen">
|
<link rel="stylesheet" href="//cdnjs.cloudflare.com/ajax/libs/normalize/5.0.0/normalize.min.css" media="screen">
|
||||||
{{ $style := resources.Get "scss/style.scss" | resources.ToCSS | resources.Minify }}
|
{{ $style := resources.Get "scss/style.scss" | resources.ToCSS | resources.Minify }}
|
||||||
{{ $sidenotes := resources.Get "scss/sidenotes.scss" | resources.ToCSS | resources.Minify }}
|
{{ $sidenotes := resources.Get "scss/sidenotes.scss" | resources.ToCSS | resources.Minify }}
|
||||||
{{ $code := resources.Get "scss/code.scss" | resources.ToCSS | resources.Minify }}
|
|
||||||
{{ $icon := resources.Get "img/favicon.png" }}
|
{{ $icon := resources.Get "img/favicon.png" }}
|
||||||
{{- partial "sidenotes.html" . -}}
|
{{- partial "sidenotes.html" . -}}
|
||||||
<link rel="stylesheet" href="{{ $style.Permalink }}" media="screen">
|
<link rel="stylesheet" href="{{ $style.Permalink }}" media="screen">
|
||||||
<link rel="stylesheet" href="{{ $sidenotes.Permalink }}" media="screen">
|
<link rel="stylesheet" href="{{ $sidenotes.Permalink }}" media="screen">
|
||||||
<link rel="stylesheet" href="{{ $code.Permalink }}" media="screen">
|
|
||||||
<link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/katex@0.11.1/dist/katex.min.css" integrity="sha384-zB1R0rpPzHqg7Kpt0Aljp8JPLqbXI3bhnPWROx27a9N0Ll6ZP/+DiW/UqRcLbRjq" crossorigin="anonymous" media="screen">
|
<link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/katex@0.11.1/dist/katex.min.css" integrity="sha384-zB1R0rpPzHqg7Kpt0Aljp8JPLqbXI3bhnPWROx27a9N0Ll6ZP/+DiW/UqRcLbRjq" crossorigin="anonymous" media="screen">
|
||||||
<link rel="icon" type="image/png" href="{{ $icon.Permalink }}">
|
<link rel="icon" type="image/png" href="{{ $icon.Permalink }}">
|
||||||
|
|
||||||
|
|
|
@ -6,9 +6,4 @@
|
||||||
{{ .Scratch.Set "u" $t }}
|
{{ .Scratch.Set "u" $t }}
|
||||||
{{ end }}
|
{{ end }}
|
||||||
{{ $v := first (add (sub (int (.Get 3)) (int (.Get 2))) 1) (.Scratch.Get "u") }}
|
{{ $v := first (add (sub (int (.Get 3)) (int (.Get 2))) 1) (.Scratch.Get "u") }}
|
||||||
{{ if (.Get 4) }}
|
{{ highlight (delimit $v "\n") (.Get 0) (printf "linenos=table,linenostart=%d" (.Get 2)) }}
|
||||||
{{ .Scratch.Set "opts" (printf ",%s" (.Get 4)) }}
|
|
||||||
{{ else }}
|
|
||||||
{{ .Scratch.Set "opts" "" }}
|
|
||||||
{{ end }}
|
|
||||||
{{ highlight (delimit $v "\n") (.Get 0) (printf "linenos=table,linenostart=%d%s" (.Get 2) (.Scratch.Get "opts")) }}
|
|
||||||
|
|
Loading…
Reference in New Issue
Block a user