New blog post on strong arrows #1725
Conversation
|
|
||
| But at the end of the day it will simply expand to intersections. The important bit is that, at the semantic level, there is no need for additional constructs and representations. | ||
|
|
||
| > Note: for the type-curious readers, set-theoretic types implement a limited form of bounded quantification a-la kernel fun. In a nutshell, it means we can only compare functions if they have the same bounds. For example, our type system cannot answer if `a -> a when a: integer() or boolean()` is a subtype of `a -> a when a: integer()`. |
There was a problem hiding this comment.
I'm probably missing some context, but I didn't understand "a-la kernel fun" and failed to look it up. Maybe we could provide a link for further reading?
|
|
||
| > Note: for the type-curious readers, set-theoretic types implement a limited form of bounded quantification a-la kernel fun. In a nutshell, it means we can only compare functions if they have the same bounds. For example, our type system cannot answer if `a -> a when a: integer() or boolean()` is a subtype of `a -> a when a: integer()`. | ||
|
|
||
| Not only that, we get lower bounds for free. If intersections allow us to place an upper bound, a union is a lower bound, because it says a given type must always be considered: `a or atom()` means atoms and any other type (which may or may not be a subset of atoms). |
There was a problem hiding this comment.
This transition is a bit brutal, especially because this whole section is about intersections and constraints, except this block (which is followed by another sentence about intersections). Also, the use case isn't very clear.
Maybe developing a more concrete example could help?
For example, I could imagine a or nil as an equivalent of an option type? (don't know if my understanding is correct)
There was a problem hiding this comment.
There aren't many examples of lower bounds. Perhaps I should move it to a "note", like I did above? It is not really required for the understanding of the text.
| end | ||
| ``` | ||
|
|
||
| The function receives two dynamically typed arguments and computes the remainder of the numerator by the denominator incremented by one. The `rem/2` operation expects both sides to be integers and returns an integer. Therefore the type of `increment_and_remainder/2` would be `dynamic(), dynamic() -> integer()`. Let's also consider that this function is part of an existing codebase where all calls to `increment_and_remainder` pass two valid integers. |
There was a problem hiding this comment.
Sorry for this probably silly question, but why isn't the type of numerator dynamic() and integer() or even integer(), since anything else is bound to fail?
There was a problem hiding this comment.
You are thinking of typing inference: the ability to look at how something is used in the code to deduce its type. We are not doing inference though, we are doing type checking.
Co-authored-by: Jean Klingler <sabiwara@gmail.com>
|
💚 💙 💜 💛 ❤️ |
No description provided.