Live data from Hacker News

Strong arrows: a new approach to gradual typing

elixir-lang.org

71–80 of 87 posts

Re: Strong arrows: a new approach to gradual typing

#71
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’m curious. What exactly is Elixir good for? What do you find in it more appealing than other languages?

It's a functional, concurrent-first language. People have talked about the upsides of functional programming to death, either you prefer it or you don't. The concurrency story, though, is a significant advantage exclusive to the BEAM languages. They utilize green threads with message passing queues that we call "processes" (not to be confused with OS-level processes).

A good almost-toy level project I built in Elixir was a Minecraft server proxy. At the top level, you've got a listener process, that waits for an incoming TCP connection, and a Supervisor process, who's responsible for the existing connections. When the listener receives a new TCP connection, it spawns a process under the Supervisor to handle that incoming connection, and goes back to listening. That's about 10 lines for code: 4 in the initiation (function declaration, start Supervisor, start Listener, end), and 6 in the Listener (function declaration, get new TCP connection, spawn process as a child of the Supervisor, assign TCP connection, recurse, end)

The child processes are running a little state machine to do some parsing of the TCP stream. They receive TCP packets as a series of messages, and based on those messages they do various things. Unimportant for the purposes of explanation, except to say that the built-in gen-statem state machine handler simplifies it down to a series of functions that match a message, and produce a new state.

But what if I receive a packet that I don't have a defined response to? Well, I don't need to write any extra code for that. When it fails to pattern match any of my states, the process is going to crash. Then it's children will crash (including the tcp connection, which will be closed by this operation), then it'll tell it's Supervisor "Alas, I am slain". By default, the Supervisor would replace it with a clone, passed the same initial arguments. But that's not the behavior we want here, we want it to just accept that the process has died, and maybe pass an alert to some process for logging or monitoring purposes. That's a built-in option, so it was just an argument in our declaration of the Supervisor in the first place.

The key thing to notice there is that anything that causes that child to crash will resolve the same, safe, way, from unpredicted packets, to the processor core it's running in being struck by a meteor. The other, perfectly fine child processes will keep chugging along, doing their own thing. Likewise, the Supervisor and Listener are protected from each other's failings. If the Listener fails, the top-level application supervisor will replace it, and likewise for the Supervisor for all the connection handlers.

This synnergy of fault tolerance and concurrency is the key idea of Erlang, and by extension Elixir. It lets you code the pretty path, and accept that there are failure modes you can't or don't want to bother anticipating.

Re: Strong arrows: a new approach to gradual typing

#72
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 understand many would love to have this yesterday but I strongly believe we should not speed it up. :) This is potentially the largest change the language will ever go through and we are being very intentional and deliberate on every step and decision we make. Once we start collecting feedback from the community, it may speed up or slow down the process, but I want to make sure everyone gets plenty of time to exper…

I would like to add that for what it's worth, I wouldn't mind slower compilation times if it means we get the type system as described. If it really does end up having a significant impact on performance, would you be open to making compile-time type-checking optional instead of scrapping the whole thing?

Re: Strong arrows: a new approach to gradual typing

#73
post #69

Earlier quoted context omitted.

The way you use the word "correct" is interesting: in PL theory circles, it usually means : "bug free", but it appears that you use it to mean: "produces the results I'm looking for". Indeed, one may write a program which is bug free, yet does not implement the algorithm that produces the expected result (for instance, a program sorting data in ascending order, when a descending order is needed). In strongly typed la…

> In strongly typed languages, type systems are used to ensure that programs are bug free, following the adage : "if it compiles, it works". (chokes on his latte) - could you elaborate on this, cos, much as I love strong typing, it surely don't mean 'bug free' at the end, not in any way useful sense.

This is a slightly above my pay grade, so take it with a bit salt.

Type systems in general reject some programs as invalid, but this claim is usually made with powerful type systems in mind; think Haskell, Idris, Rust. I only played with these casually, but it is true that you can write some code, and then let yourself be guided by compiler in fixing all the errors. It's often the case that the resulting program just works.

Rust's borrow checker is a part of its type system, based on some flavor of linear types if I remember correctly. Think about it: the type system can protect you from double frees. This is powerful.

In Haskell, for starters, you can't do any side effects outside of IO monad. You can express precisely what a given function is allowed to do.

In dependently-typed languages you can express that, for example, a function concatenating lists of length n and m returns a list of length n + m.

And aside from these above there is a lot of other, less magical things: no nulls, exhaustiveness checks for ADTs, some focus on immutability, lack of exceptions, and so on.

Now, I doubt we are all going to write Idris in five years, and even there bugs do happen obviously. But the idea compiles==works is not entirely out of this world.

Re: Strong arrows: a new approach to gradual typing

#74

Earlier quoted context omitted.

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.

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.

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.

Re: Strong arrows: a new approach to gradual typing

#75

Earlier quoted context omitted.

I’m curious. What exactly is Elixir good for? What do you find in it more appealing than other languages?

It's a functional, concurrent-first language. People have talked about the upsides of functional programming to death, either you prefer it or you don't. The concurrency story, though, is a significant advantage exclusive to the BEAM languages. They utilize green threads with message passing queues that we call "processes" (not to be confused with OS-level processes). A good almost-toy level project I built in Elixir…

Thanks for the detailed response. There’s no other mainstream language which has this fault tolerance built-in, right?

Re: Strong arrows: a new approach to gradual typing

#76

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

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

Re: Strong arrows: a new approach to gradual typing

#77
post #73
post #69

Earlier quoted context omitted.

> In strongly typed languages, type systems are used to ensure that programs are bug free, following the adage : "if it compiles, it works". (chokes on his latte) - could you elaborate on this, cos, much as I love strong typing, it surely don't mean 'bug free' at the end, not in any way useful sense.

This is a slightly above my pay grade, so take it with a bit salt. Type systems in general reject some programs as invalid, but this claim is usually made with powerful type systems in mind; think Haskell, Idris, Rust. I only played with these casually, but it is true that you can write some code, and then let yourself be guided by compiler in fixing all the errors. It's often the case that the resulting program just…

Thank you, that's exactly what I had in mind when speaking about strongly typed languages. I don't think I could have presented it in a better way.

Re: Strong arrows: a new approach to gradual typing

#78

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

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

Re: Strong arrows: a new approach to gradual typing

#79
post #12

Earlier quoted context omitted.

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.

I hear new Cto came in, got nervous about hiring. They are still hiring for elixir positions, though?

i heard basically the same and also (the new CTO just really like kotlin and knew a bunch of people who know kotlin and wanted to bring them over. )

again, take the above with a grain of salt.

Re: Strong arrows: a new approach to gradual typing

#80

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.

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) cann…

it's a good talk.

the static typing (of the future) at the end of the video isn't, say, the static typing of C# or Java.

Static typing should be more like OCaml, Elm, Rust, Haskell (and ideally Roc)

Post reply on HN