Skip to content

Commit

Permalink
Fix potential typos in readme.md
Browse files Browse the repository at this point in the history
In the first change, `y` was defined but not subsequently used.

In the second change, the `else` branch was missing.
  • Loading branch information
bmwalters committed Jan 20, 2021
1 parent 4b99ec7 commit b68b18d
Showing 1 changed file with 4 additions and 4 deletions.
8 changes: 4 additions & 4 deletions readme.md
Expand Up @@ -1722,14 +1722,14 @@ Here is an example that demonstrates what I got hung up on in pseudo-code. Imagi

```fs
let (y : (if x < 10 then int else string)) = if x < 10 then 0 else "asd"
if x < 10 then x + 10 else x + "qwe"
if x < 10 then y + 10 else y + "qwe"
```

In Spiral, F# and other statically typed languages with strong, but not dependent type systems, the types actually do have a 1:1 correspondence with their underlying representation.

How exactly the type `if x < 10 then int else string` be compiled? Is it some kind of union type? That seems to be a reasonable avenue to go down on at first, but the difficulties of that become apparent very quickly.

In the branches of `if x < 10 then x + 10 else x + "qwe"` how should `x` be destructured if it is a union type under the hood? Thinking about it logically, we know that `x` is an `int` in the *then* branch, and a `string` in the *else* branch, but where is the hook to actually unbox the union? This kind of thinking does not really make sense to me.
In the branches of `if x < 10 then y + 10 else y + "qwe"` how should `y` be destructured if it is a union type under the hood? Thinking about it logically, we know that `y` is an `int` in the *then* branch, and a `string` in the *else* branch, but where is the hook to actually unbox the union? This kind of thinking does not really make sense to me.

As if it were a force of nature, there is an inexorable pull towards admitting that despite being statically typed, the types in dependently typed languages are unmoored from their underlying representation. Much like in dynamically typed languages. And the most natural way of compiling the above fragment would be to forget the type signatures and just execute it in a computational context that has uniform representation for all its datatypes.

Expand Down Expand Up @@ -1962,7 +1962,7 @@ It is not just the shape of the data that can be matched on. As long as the valu
open real_core
inl main () =
inl x = 1
if x < 10 then x + 10
if x < 10 then x + 10 else "asd"
```
```fs
11
Expand Down Expand Up @@ -4144,4 +4144,4 @@ I don't have intention of working on these for the time being. I do not know how

* The mapping from the files on the hard drive, to the editor, to the language server is not perfect. For example opening a file first, and then having a new project file usurp ownership from another project file will not be reacted to by the language server unless it is done from the editor.

* There is a name collision between Spiral and a [DSL](https://www.spiral.net/) by the same name. This is purely coincidental and there is no association between the two.
* There is a name collision between Spiral and a [DSL](https://www.spiral.net/) by the same name. This is purely coincidental and there is no association between the two.

0 comments on commit b68b18d

Please sign in to comment.