Unfortunately you need to know type theory/logic notation in order to read this. Here's the English translation:
- There is a variable called `x` in scope.
- `x` is known to have type `A`.
- `B` is a function that, when given `x` as an argument, returns a type. If this seems weird, it's because you need dependent types to even be able to say this.
Honestly, this article is not written for programmers, and I don't know why it's on Hacker News right now. Most HN readers don't have the necessary background to follow it.
- There is a variable called `x` in scope.
- `x` is known to have type `A`.
- `B` is a function that, when given `x` as an argument, returns a type. If this seems weird, it's because you need dependent types to even be able to say this.
Honestly, this article is not written for programmers, and I don't know why it's on Hacker News right now. Most HN readers don't have the necessary background to follow it.