Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Strong arrows: a new approach to gradual typing

elixir-lang.org

Post reply on HN
Print view View original

21–30 of 87 posts

Re: Strong arrows: a new approach to gradual typing

#21

Post by josevalim »

daxfohl wrote: post #12
anonyfox wrote: post #3

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…

I read that Brex moved away from Elixir to Kotlin. If Elixir was really that great then why would a company put such a big effort to ditch it? That killed off my interest in learning it, but maybe their reasons were invalid? Genuinely curious.

You will find examples from companies moving away from Elixir, Python, JavaScript, Scala, Java, etc. I don't think there is any programming language that is "unditchable". So I'd suggest to analyze the reasons that made a company move away from X, check if they are still relevant, if they'd apply to you, and, if yes, if they are a deal breaker or something you can work around.

For the Brex case, if I remember correctly, lack of static typing and early-development of gRPC tools were the reasons back then. How much this impacts your needs is up to you.

Re: Strong arrows: a new approach to gradual typing

#22

Post by jovial_cavalier »

tjrgergw wrote: post #18

"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 perfo…

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?"

Re: Strong arrows: a new approach to gradual typing

#23

Post by losvedir »

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

Re: Strong arrows: a new approach to gradual typing

#24

Post by tjrgergw »

jovial_cavalier wrote: post #22
tjrgergw wrote: post #18

"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 perfo…

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 Pyth…

You compile your code every time you run it? Yikes. Sorry to hear that.

Re: Strong arrows: a new approach to gradual typing

#25

Post by johnbcoughlin »

jovial_cavalier wrote: post #22
tjrgergw wrote: post #18

"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 perfo…

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 Pyth…

What does "most applications" mean?

Re: Strong arrows: a new approach to gradual typing

#26

Post by sodapopcan »

daxfohl wrote: post #12
anonyfox wrote: post #3

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…

I read that Brex moved away from Elixir to Kotlin. If Elixir was really that great then why would a company put such a big effort to ditch it? That killed off my interest in learning it, but maybe their reasons were invalid? Genuinely curious.

Too bad, you're missing out. Did you look into companies that have not ditched it?

People don't tend to write articles titled, "We've been using the same tech for 10 years and have had no major issues with it so we are still using it." It's always the "we ditched x for y" ones that get traction and the actions of ONE company can seemingly have a far-reaching impression for people who otherwise know nothing about the technology in question.

Re: Strong arrows: a new approach to gradual typing

#27

Post by josevalim »

contravariant wrote: post #6

> 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 vers…

> 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.

Re: Strong arrows: a new approach to gradual typing

#28

Post by sodapopcan »

yawboakye wrote: post #10

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.

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.

Re: Strong arrows: a new approach to gradual typing

#29

Post by eigenspace »

jovial_cavalier wrote: post #22
tjrgergw wrote: post #18

"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 perfo…

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 Pyth…

Maybe if your program is just println("hello world!")

Julia also has done a lot lately[1] to cache the results of JIT compilation from packages and re-use it later. So if you're doing a lot of println("hello world!") or whatever, you can make that faster by bundling it in a package and adding a precompile workflow. This will also be improving more with upcoming releases.

[1] https://julialang.org/blog/2023/04/julia-1.9-highlights/#cac...

Re: Strong arrows: a new approach to gradual typing

#30

Post by josevalim »

losvedir wrote: post #23

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, ty…

> 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.

Post reply on HN