15 ms·

Strong arrows: a new approach to gradual typing

200 points by ahamez 3y ago

benreesman 3y ago
Slightly OT (though I do really like Elixir: I used to work with José and he’s a goddamned visionary): TypeScript just hits it out of the park here. With arguably harder erasure constraints than either Java or C# the covariance and contravariance bounds and ergonomics are so much more intuitive than either. The MSR brain trust is clearly keeping their eye on the ball. Elixir looks to be one of few languages that is never going to sit still on absorbing the best ideas. At the risk of repetition, no one would expect less from the person who’s passion created it.
- weatherlight 3y ago
  > TypeScript just hits it out of the park here but the type system isn't sound :( whats the point of a type system? if it's not sound?
anonyfox 3y ago
I cannot support much in terms of money or time currently, but somehow I'd wish there are ways to speed this up. Sure, sponsoring from big corps comes with their own problems, but maybe that would be an option? There are quite some that use Elixir (or BEAM in general) out there... Idk what would be the best approach. But I am very convinced that Elixir and the wider ecosystem (not only phoenix liveview) is (or could be) the very best "default" web app stack we have right now in general. It solves _so many_ problems of other comparable tech stacks right out of the box, one way or the other, and is the only one I've noticed a sentiment of pure joy from seasoned devs that also lasts well after the novelty wears off. At this point it looks "only" like a number problem to become mainstream (again a number problem). No idea how to solve it, just felt I needed to share my thoughts as a data point here. Like the type system here: I'd _kill_ to have this exact implementation today rather than _maybe in a few years_. And yes, I can draw comparison to Typescript, Rust and Haskell which I used for projects in the past. Its like combining the very beast ideas (and adding some more) into one awesome thing.
- tempotemporary 3y ago
  > It solves _so many_ problems of other comparable tech stacks right out of the box Could you expand top 5(or more) major pain points that it solves?
  - anonyfox 3y ago
    I don't thinks that would be a helpful discussion right here. Any one point there might come someone who points at some external "solution" (package, tool, ...) that might also do the same feature in some way for X, ignoring the fact that there are lot of Y without that particular thing still, but leads into derailing the argument anyways. Elixir (and esp. Phoenix for web dev) is more like the culmination of the best ideas and heavily draws/depends on the last decades of real-world experience. Most stuff isn't (or shouldn't) be surprising, but the point is that everything you might need for the vast majority of projects is right there, nicely packaged up into a unified nice thingy. But to give you a few of _my_ top points: 1. Architecture and DX for complex interactions: there is no need to bring in supplemental infrastructure crutches (Redis, AWS whatever service, ...) in many cases to begin with. OTP, which is like a core library always available, already includes the building blocks for things like cache servers, application clustering and supervision strategies, ... . 2. Reliability and availability: this tech is the original one achieving the "nine-nines" of uptime record. To get an idea of how, https://www.youtube.com/watch?v=JvBT4XBdoUE https://www.youtube.com/watch?v=JvBT4XBdoUE this talked is packed and excellent, and also highlights a few things why it can achieve my point 1 above. 3. "SPA-like" interactivity with full server side rendering without all the pains of exposing/consuming a dedicated HTTP API in between, or overcomplicated nuances of rendering pipelines (also see react server components) to achieve SSR/CSR in a way that not sucks or is noticeably slow. Liveview is tried to be replicated in other stacks, but they don't come close in reality today or complicate the apps' infrastructure with additional crudges. And don't get me started on the integration testing story compared with SPA+Backend setups. 4. Agents/Message passing parallelism (not only concurrency, but also distributed!) at your fingertips, which makes modeling current "async problems" kinda trivial. OTOH, building something like a proper async-based web framework in rust is quite a pain in the ass, with lots of type fiddling needed, instead of doing the solution you actually want to deliver with it. 5. Some absolutely awesome takes on some typical libraries. Take the ORM options for javascript/typescript (all with severe tradeoffs, and analysis paralysis ontop). Take Rails' ActiveRecord with lots of magic and while great to get started becomes quickly bloated (iE fat models) in bigger projects. And then Ecto got it "just right" with slim schemas, changesets, and basically pure functions + pipelines. Any "model" can be used within new usecases by adding new changesets/validations explicitly and easily, there is no "general" validation right on the model level you have to tiptoe around, and starting If-cascades.
contravariant 3y ago
> If the function returns none() (i.e. it does not type check) or a type which is a subset of its codomain (i.e. its output), then it is a strong arrow. Unless I didn't understand correctly, surely 'none()' is also a subset of the codomain? Or is none() a type containing all errors? Anyway the concept of strong arrows is interesting. But does it also mean you can 'weaken' an arrow if you implement a more general version of a function? That would make it a bit odd because you can't know up front whether an arrow is strong or not. It makes code very non-local.
- josevalim 3y ago
  > Unless I didn't understand correctly, surely 'none()' is also a subset of the codomain? Correct. Both are included for clarity. > But does it also mean you can 'weaken' an arrow if you implement a more general version of a function? If you have a function that is a strong arrow because of other functions (i.e. the current function does not explicit guard its arguments) then that would be the case. However, we don't know yet how much of a big deal this is. Strong arrows is all about making static typing more useful to dynamic code. Dynamic code should not be relying on strong arrows for correctness, they are a nice to have. If you want guarantees, then you need static typing. It may be that, in practice, it is enough for Elixir standard library to be made of strong arrows and that will propagate enough type information to most dynamic programs. Otherwise, if more is needed, we will definitely need to add visibility and reflection APIs around strong arrows.
  - cryptonector 3y ago
    > Strong arrows is all about making static typing more useful to dynamic code. Where "more useful" == safer and faster [0] when you make use of static typing. [0] If the compiler and runtime take advantage of the optimization opportunities.
charcircuit 3y ago
This blog post makes this look like a type system for theoretical type theory people to play with than something designed to actually be practical and useful.
- hughw 3y ago
  I guess I'd be glad to have my type system designed by people well grounded in theory.
  - charcircuit 3y ago
    Not if it results in the type system being optimized for type theorists to play around with and not to assist developers in making real projects.
    - josevalim 3y ago
      This is a surprising assessment given most of the blog post is explaining how to build the type system in a way it can give feedback on all _existing real projects_ already written in Elixir. :) It is the opposite of optimizing for type theorists and rather exploring how to bring values to the existing millions of lines of code. Edit: I am the author.
      - charcircuit 3y ago
        It's about the way it is framed and that this is the main blog of the programming language, so the target demographic isn't people interested about how awesome a type theory based off of set theory is. My complaint was about the way the information was presented was in a way that I don't think properly motivates why this is being done and will be a good thing. For example the text about gradual typing should have been near the start to motivate why this was being done, but instead the blog post starts by trying to teach people the basics of using types + set theory.
        josevalim 3y ago
yawboakye 3y ago
the arc of progress in software engineering bends towards static typing. in the future, our type systems will be so powerful they'll be able to do more inference so that we have to be less explicit. then people who have come to hate static type because of these explicit type declarations will know they hated the costume after all, not the person in it.
- sodapopcan 3y ago
  OCaml had this figured out many years ago. Elixir/Erlang's dynamism can be particularly good compared to other dynamic languages if you lean into it properly. But yes, the world is loving static typing right now, and I'm actually a bit excited myself with their ideas for Elixir's type system.
  - pxeger1 3y ago
    What exactly do you mean that OCaml has figured out?
    - sodapopcan 3y ago
      It's a statically typed language that doesn't require explicit type declarations (in most cases, at least).
      - sodapopcan 3y ago
        Er, to clarify, I mean it has very strong type inference. If you're making a record or complex type then yes, you still need to define the type, so maybe that is what OP was actually talking about?
- raphlinus 3y ago
  Yeah, Rich Feldman has a good talk on this, entitled Why Static Typing Came Back[1]. It makes a good argument that static typing can recover most of the advantages traditionally accounted to dynamic typing. Rapid iteration you can get from incremental compilers, being concise you can get from powerful type inference, etc. Conversely, the advantages of static typing (largely boiling down to increased reliability) cannot easily be captured by dynamically typed languages. Gradual typing, particularly successful by TypeScript, might be an interesting middle ground, or it might just be a reflection of the dynamic history of JS. [1]: https://www.youtube.com/watch?v=Tml94je2edk https://www.youtube.com/watch?v=Tml94je2edk
tutfbhuf 3y ago
When we talk about arrows in terms of functional programming, we really mean Hughes’ Arrows (or Freyd-categories) a generalization of monads. The term arrow represents a level of abstraction over computations, essentially modeling them as objects with inputs and outputs. Hughes' Arrows extend beyond the traditional notion of functors and monads in handling side effects and common computational patterns in a more structured manner. Arrows are useful because they provide a computation model that can implicitly make use of state without ever exposing that state to the programmer. The programmer can use arrowized computations and combine them to create sophisticated systems. A strong arrow is an arrow A having an extra structure known as strength. The strength for A is a natural transformation, generally denoted by t, which consumes a pair of objects (X,Y) and gives back an arrow in the category. In a concrete manner, the strength has this form: t_X,Y: X x AY -> A(X x Y), called tensorial strength. The strength obeys some particular coherence conditions. A deeper explanation involves the monoidal structure of a category and how the 'strength' aids in elaborating the combination of values in the arrow context.
- tomberek 3y ago
  This was my first thought, but this connection was not made clear in the article - or if it was a naming coincidence.
- aatd86 3y ago
  And here I thought it was just about functions (arrow type) ;p
- reuben364 3y ago
  My understanding here for Elixir is that you have dynamic() as a universe U and an error set E. All functions f are from U to E + U. f is an arrow A -> B iff f[A] subset B + E. f is a strong arrow iff it is an arrow and f(U\A) subset E. I'm not sure how this connects to strength in the category theoretic sense.
tjrgergw 3y ago
"gradual typing" is exactly how I code Julia. Disclaimer: this is not how to the strengths of Julia are normally described by most people, it's just how I think about it. You might have heard that Julia solves the two language problem (easy as python, fast as C++). But exactly how does it do that? In python you don't have to care about types, but even if you were willing to care about types you wouldn't get any performance benefit. In C++ you have to care about types, you don't have the option not to, even when you don't care about performance. In Julia you don't have to care about types. You can code it exactly as python. But if you are willing to you can care about types, and you'll get a huge performance benefit. So, the way I code Julia is on a first pass I code it like python. I don't care about types, I just care that it's correct. Then, after it's correct, and if performance is critical, I start thinking about types. So Julia very much lends itself to "make it work, make it right, make it fast", by allowing you to gradually introducing types into the parts of your code that matter.
- jovial_cavalier 3y ago
  Julia is slower than Python for most applications if you include the compile time (which is every time you run your program, because it's "just in time"). edit: I want to be clear - I like Julia, and I have long wanted a scripting language that was gramatically simple like python but had support for strong typing, etc. But the TTFX problem, for me, muddies the waters on the question of "which is faster, Julia or Python?"
  - tjrgergw 3y ago
    You compile your code every time you run it? Yikes. Sorry to hear that.
    - jovial_cavalier 3y ago
      Is there a way to get around that in Julia? I tried to find a way to compile programs directly, and was disappointed with what was on offer.
      - 3y ago
losvedir 3y ago
This is great! I've been an Elixir developer professionally for many years now, and I love it. (I took my current job in large part for the opportunity to use it some more.) But this scratches the one last itch I have with it. After having a taste of types from Rust and Typescript, I do miss them from time to time. One thing I really like about a strong type system is it makes VSCode feel like it has super powers, type-checking in line and improving suggestions and all that. Given that this seems to be a somewhat novel type system, what are the implications for editor integration? Will it still do all the cool things that Language Servers support? In other words, is the "set theoretic type system" an implementation detail which doesn't affect the language server API? The post is great, and I'm still digesting it, but this one part caught my eye: > In a nutshell, it means we can only compare functions if they have the same bounds. For example, our type system states a -> a when a: integer() or boolean() is not a subtype of a -> a when a: integer(). It's not a subtype right? If a function could safely accept some function `f` as a parameter, then if that function were able to return more than expected, it wouldn't be safe to drop it in. I think the return values have to be more restricted. On the other hand, the input can be more general. This is "covariance" and "contravariance" in types, I think? But regardless, this is one of my main hangups with dialyzer: its `underspecs` and `overspecs` design gets it wrong. I mentioned in once a while ago in this comment[0] with more examples. But, if you typed it like this: @type direction :: east | north | west | south @spec common_wind() :: direction def common_winds(), do: :east dialyzer will complain because it infers `common_winds/0` can only return one of the values that it's spec'ed for. (If you have `overspecs` or `underspecs` - I forget which - enabled, which you need, if you want to restrict input types.) So I guess my question with this approach, is whether you can explicitly spec "larger" sets than is inferred? And if so, whether the given specs overrule the inferred ones elsewhere. [0] https://news.ycombinator.com/item?id=31568098 https://news.ycombinator.com/item?id=31568098
- josevalim 3y ago
  > In other words, is the "set theoretic type system" an implementation detail which doesn't affect the language server API? This should be the case. Type violations would automatically appear on your IDEs when you update Elixir. However, if you need additional metadata/features, then we need to expose them from Elixir and Language Servers need to consume it. But that's implementation work and not "type system" work. :) > But regardless, this is one of my main hangups with dialyzer: its `underspecs` and `overspecs` design gets it wrong. I believe recent Erlang/OTP versions changed this to give you more fine grained control for the precise reasons you mentioned. > So I guess my question with this approach, is whether you can explicitly spec "larger" sets than is inferred? And if so, whether the given specs overrule the inferred ones elsewhere. I am 99% sure the theory allows both options, so we will pick one based on patterns and community needs.
glonq 3y ago
Please tell me that I'm not the only one who thought that this was a story about learning how to touch-type better. I guess we peaked at Mavis Beacon then?

200 points by ahamez 3y ago

Slightly OT (though I do really like Elixir: I used to work with José and he’s a goddamned visionary): TypeScript just hits it out of the park here. With arguably harder erasure constraints than either Java or C# the covariance and contravariance bounds and ergonomics are so much more intuitive than either. The MSR brain trust is clearly keeping their eye on the ball. Elixir looks to be one of few languages that is never going to sit still on absorbing the best ideas. At the risk of repetition, no one would expect less from the person who’s passion created it.

weatherlight 3y ago
> TypeScript just hits it out of the park here but the type system isn't sound :( whats the point of a type system? if it's not sound?

anonyfox 3y ago

I cannot support much in terms of money or time currently, but somehow I'd wish there are ways to speed this up. Sure, sponsoring from big corps comes with their own problems, but maybe that would be an option? There are quite some that use Elixir (or BEAM in general) out there... Idk what would be the best approach. But I am very convinced that Elixir and the wider ecosystem (not only phoenix liveview) is (or could be) the very best "default" web app stack we have right now in general. It solves _so many_ problems of other comparable tech stacks right out of the box, one way or the other, and is the only one I've noticed a sentiment of pure joy from seasoned devs that also lasts well after the novelty wears off. At this point it looks "only" like a number problem to become mainstream (again a number problem). No idea how to solve it, just felt I needed to share my thoughts as a data point here. Like the type system here: I'd _kill_ to have this exact implementation today rather than _maybe in a few years_. And yes, I can draw comparison to Typescript, Rust and Haskell which I used for projects in the past. Its like combining the very beast ideas (and adding some more) into one awesome thing.

tempotemporary 3y ago
> It solves _so many_ problems of other comparable tech stacks right out of the box Could you expand top 5(or more) major pain points that it solves?
- anonyfox 3y ago
  I don't thinks that would be a helpful discussion right here. Any one point there might come someone who points at some external "solution" (package, tool, ...) that might also do the same feature in some way for X, ignoring the fact that there are lot of Y without that particular thing still, but leads into derailing the argument anyways. Elixir (and esp. Phoenix for web dev) is more like the culmination of the best ideas and heavily draws/depends on the last decades of real-world experience. Most stuff isn't (or shouldn't) be surprising, but the point is that everything you might need for the vast majority of projects is right there, nicely packaged up into a unified nice thingy. But to give you a few of _my_ top points: 1. Architecture and DX for complex interactions: there is no need to bring in supplemental infrastructure crutches (Redis, AWS whatever service, ...) in many cases to begin with. OTP, which is like a core library always available, already includes the building blocks for things like cache servers, application clustering and supervision strategies, ... . 2. Reliability and availability: this tech is the original one achieving the "nine-nines" of uptime record. To get an idea of how, https://www.youtube.com/watch?v=JvBT4XBdoUE https://www.youtube.com/watch?v=JvBT4XBdoUE this talked is packed and excellent, and also highlights a few things why it can achieve my point 1 above. 3. "SPA-like" interactivity with full server side rendering without all the pains of exposing/consuming a dedicated HTTP API in between, or overcomplicated nuances of rendering pipelines (also see react server components) to achieve SSR/CSR in a way that not sucks or is noticeably slow. Liveview is tried to be replicated in other stacks, but they don't come close in reality today or complicate the apps' infrastructure with additional crudges. And don't get me started on the integration testing story compared with SPA+Backend setups. 4. Agents/Message passing parallelism (not only concurrency, but also distributed!) at your fingertips, which makes modeling current "async problems" kinda trivial. OTOH, building something like a proper async-based web framework in rust is quite a pain in the ass, with lots of type fiddling needed, instead of doing the solution you actually want to deliver with it. 5. Some absolutely awesome takes on some typical libraries. Take the ORM options for javascript/typescript (all with severe tradeoffs, and analysis paralysis ontop). Take Rails' ActiveRecord with lots of magic and while great to get started becomes quickly bloated (iE fat models) in bigger projects. And then Ecto got it "just right" with slim schemas, changesets, and basically pure functions + pipelines. Any "model" can be used within new usecases by adding new changesets/validations explicitly and easily, there is no "general" validation right on the model level you have to tiptoe around, and starting If-cascades.

contravariant 3y ago

> If the function returns none() (i.e. it does not type check) or a type which is a subset of its codomain (i.e. its output), then it is a strong arrow. Unless I didn't understand correctly, surely 'none()' is also a subset of the codomain? Or is none() a type containing all errors? Anyway the concept of strong arrows is interesting. But does it also mean you can 'weaken' an arrow if you implement a more general version of a function? That would make it a bit odd because you can't know up front whether an arrow is strong or not. It makes code very non-local.

josevalim 3y ago
> Unless I didn't understand correctly, surely 'none()' is also a subset of the codomain? Correct. Both are included for clarity. > But does it also mean you can 'weaken' an arrow if you implement a more general version of a function? If you have a function that is a strong arrow because of other functions (i.e. the current function does not explicit guard its arguments) then that would be the case. However, we don't know yet how much of a big deal this is. Strong arrows is all about making static typing more useful to dynamic code. Dynamic code should not be relying on strong arrows for correctness, they are a nice to have. If you want guarantees, then you need static typing. It may be that, in practice, it is enough for Elixir standard library to be made of strong arrows and that will propagate enough type information to most dynamic programs. Otherwise, if more is needed, we will definitely need to add visibility and reflection APIs around strong arrows.
- cryptonector 3y ago
  > Strong arrows is all about making static typing more useful to dynamic code. Where "more useful" == safer and faster [0] when you make use of static typing. [0] If the compiler and runtime take advantage of the optimization opportunities.

charcircuit 3y ago

This blog post makes this look like a type system for theoretical type theory people to play with than something designed to actually be practical and useful.

hughw 3y ago
I guess I'd be glad to have my type system designed by people well grounded in theory.
- charcircuit 3y ago
  Not if it results in the type system being optimized for type theorists to play around with and not to assist developers in making real projects.
  - josevalim 3y ago
    This is a surprising assessment given most of the blog post is explaining how to build the type system in a way it can give feedback on all _existing real projects_ already written in Elixir. :) It is the opposite of optimizing for type theorists and rather exploring how to bring values to the existing millions of lines of code. Edit: I am the author.
    - charcircuit 3y ago
      It's about the way it is framed and that this is the main blog of the programming language, so the target demographic isn't people interested about how awesome a type theory based off of set theory is. My complaint was about the way the information was presented was in a way that I don't think properly motivates why this is being done and will be a good thing. For example the text about gradual typing should have been near the start to motivate why this was being done, but instead the blog post starts by trying to teach people the basics of using types + set theory.
      - josevalim 3y ago

yawboakye 3y ago

the arc of progress in software engineering bends towards static typing. in the future, our type systems will be so powerful they'll be able to do more inference so that we have to be less explicit. then people who have come to hate static type because of these explicit type declarations will know they hated the costume after all, not the person in it.

sodapopcan 3y ago
OCaml had this figured out many years ago. Elixir/Erlang's dynamism can be particularly good compared to other dynamic languages if you lean into it properly. But yes, the world is loving static typing right now, and I'm actually a bit excited myself with their ideas for Elixir's type system.
- pxeger1 3y ago
  What exactly do you mean that OCaml has figured out?
  - sodapopcan 3y ago
    It's a statically typed language that doesn't require explicit type declarations (in most cases, at least).
    - sodapopcan 3y ago
      Er, to clarify, I mean it has very strong type inference. If you're making a record or complex type then yes, you still need to define the type, so maybe that is what OP was actually talking about?
raphlinus 3y ago
Yeah, Rich Feldman has a good talk on this, entitled Why Static Typing Came Back[1]. It makes a good argument that static typing can recover most of the advantages traditionally accounted to dynamic typing. Rapid iteration you can get from incremental compilers, being concise you can get from powerful type inference, etc. Conversely, the advantages of static typing (largely boiling down to increased reliability) cannot easily be captured by dynamically typed languages. Gradual typing, particularly successful by TypeScript, might be an interesting middle ground, or it might just be a reflection of the dynamic history of JS. [1]: https://www.youtube.com/watch?v=Tml94je2edk https://www.youtube.com/watch?v=Tml94je2edk

tutfbhuf 3y ago

When we talk about arrows in terms of functional programming, we really mean Hughes’ Arrows (or Freyd-categories) a generalization of monads. The term arrow represents a level of abstraction over computations, essentially modeling them as objects with inputs and outputs. Hughes' Arrows extend beyond the traditional notion of functors and monads in handling side effects and common computational patterns in a more structured manner. Arrows are useful because they provide a computation model that can implicitly make use of state without ever exposing that state to the programmer. The programmer can use arrowized computations and combine them to create sophisticated systems. A strong arrow is an arrow A having an extra structure known as strength. The strength for A is a natural transformation, generally denoted by t, which consumes a pair of objects (X,Y) and gives back an arrow in the category. In a concrete manner, the strength has this form: t_X,Y: X x AY -> A(X x Y), called tensorial strength. The strength obeys some particular coherence conditions. A deeper explanation involves the monoidal structure of a category and how the 'strength' aids in elaborating the combination of values in the arrow context.

tomberek 3y ago
This was my first thought, but this connection was not made clear in the article - or if it was a naming coincidence.
aatd86 3y ago
And here I thought it was just about functions (arrow type) ;p
reuben364 3y ago
My understanding here for Elixir is that you have dynamic() as a universe U and an error set E. All functions f are from U to E + U. f is an arrow A -> B iff f[A] subset B + E. f is a strong arrow iff it is an arrow and f(U\A) subset E. I'm not sure how this connects to strength in the category theoretic sense.

tjrgergw 3y ago

"gradual typing" is exactly how I code Julia. Disclaimer: this is not how to the strengths of Julia are normally described by most people, it's just how I think about it. You might have heard that Julia solves the two language problem (easy as python, fast as C++). But exactly how does it do that? In python you don't have to care about types, but even if you were willing to care about types you wouldn't get any performance benefit. In C++ you have to care about types, you don't have the option not to, even when you don't care about performance. In Julia you don't have to care about types. You can code it exactly as python. But if you are willing to you can care about types, and you'll get a huge performance benefit. So, the way I code Julia is on a first pass I code it like python. I don't care about types, I just care that it's correct. Then, after it's correct, and if performance is critical, I start thinking about types. So Julia very much lends itself to "make it work, make it right, make it fast", by allowing you to gradually introducing types into the parts of your code that matter.

jovial_cavalier 3y ago
Julia is slower than Python for most applications if you include the compile time (which is every time you run your program, because it's "just in time"). edit: I want to be clear - I like Julia, and I have long wanted a scripting language that was gramatically simple like python but had support for strong typing, etc. But the TTFX problem, for me, muddies the waters on the question of "which is faster, Julia or Python?"
- tjrgergw 3y ago
  You compile your code every time you run it? Yikes. Sorry to hear that.
  - jovial_cavalier 3y ago
    Is there a way to get around that in Julia? I tried to find a way to compile programs directly, and was disappointed with what was on offer.
    - 3y ago

losvedir 3y ago

This is great! I've been an Elixir developer professionally for many years now, and I love it. (I took my current job in large part for the opportunity to use it some more.) But this scratches the one last itch I have with it. After having a taste of types from Rust and Typescript, I do miss them from time to time. One thing I really like about a strong type system is it makes VSCode feel like it has super powers, type-checking in line and improving suggestions and all that. Given that this seems to be a somewhat novel type system, what are the implications for editor integration? Will it still do all the cool things that Language Servers support? In other words, is the "set theoretic type system" an implementation detail which doesn't affect the language server API? The post is great, and I'm still digesting it, but this one part caught my eye: > In a nutshell, it means we can only compare functions if they have the same bounds. For example, our type system states a -> a when a: integer() or boolean() is not a subtype of a -> a when a: integer(). It's not a subtype right? If a function could safely accept some function `f` as a parameter, then if that function were able to return more than expected, it wouldn't be safe to drop it in. I think the return values have to be more restricted. On the other hand, the input can be more general. This is "covariance" and "contravariance" in types, I think? But regardless, this is one of my main hangups with dialyzer: its `underspecs` and `overspecs` design gets it wrong. I mentioned in once a while ago in this comment[0] with more examples. But, if you typed it like this: @type direction :: east | north | west | south @spec common_wind() :: direction def common_winds(), do: :east dialyzer will complain because it infers `common_winds/0` can only return one of the values that it's spec'ed for. (If you have `overspecs` or `underspecs` - I forget which - enabled, which you need, if you want to restrict input types.) So I guess my question with this approach, is whether you can explicitly spec "larger" sets than is inferred? And if so, whether the given specs overrule the inferred ones elsewhere. [0] https://news.ycombinator.com/item?id=31568098 https://news.ycombinator.com/item?id=31568098

josevalim 3y ago
> In other words, is the "set theoretic type system" an implementation detail which doesn't affect the language server API? This should be the case. Type violations would automatically appear on your IDEs when you update Elixir. However, if you need additional metadata/features, then we need to expose them from Elixir and Language Servers need to consume it. But that's implementation work and not "type system" work. :) > But regardless, this is one of my main hangups with dialyzer: its `underspecs` and `overspecs` design gets it wrong. I believe recent Erlang/OTP versions changed this to give you more fine grained control for the precise reasons you mentioned. > So I guess my question with this approach, is whether you can explicitly spec "larger" sets than is inferred? And if so, whether the given specs overrule the inferred ones elsewhere. I am 99% sure the theory allows both options, so we will pick one based on patterns and community needs.

glonq 3y ago

Please tell me that I'm not the only one who thought that this was a story about learning how to touch-type better. I guess we peaked at Mavis Beacon then?