|
|
|
@ -30,7 +30,7 @@ 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 fpr |
|
|
|
|
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 |
|
|
|
@ -46,7 +46,7 @@ Our `Expr` data type, which allows ill-typed expressions, ends up as follows: |
|
|
|
|
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 vein, we extend our `SafeExpr` GADT: |
|
|
|
|
a similar manner, we extend our `SafeExpr` GADT: |
|
|
|
|
|
|
|
|
|
{{< codelines "Idris" "typesafe-interpreter/TypesafeIntrV3.idr" 41 49 "hl_lines=7 8 9" >}} |
|
|
|
|
|
|
|
|
@ -93,7 +93,7 @@ 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 false, and thus, this case |
|
|
|
|
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 |
|
|
|
@ -131,7 +131,7 @@ 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 lt2 replaced |
|
|
|
|
PairType lt1 lt2 = PairType rt1 lt2 -- Second lt1 replaced |
|
|
|
|
PairType rt1 lt2 = PairType rt1 lt2 -- Both replaced |
|
|
|
|
``` |
|
|
|
|
|
|
|
|
@ -147,7 +147,7 @@ t1 => PairType lt1 lt2 = PairType t1 lt2 |
|
|
|
|
t1 => PairType t1 lt2 = PairType t1 lt2 |
|
|
|
|
``` |
|
|
|
|
|
|
|
|
|
The highlighted function is the one we'll need to use to attain |
|
|
|
|
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: |
|
|
|
|