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

81–87 of 87 posts

Re: Strong arrows: a new approach to gradual typing

#81

Post by alphablended »

_a_a_a_ wrote: post #69
alphablended wrote: post #49

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.

You make a valid point: I used the word "bug" here without trying first to define it, and that led to confusion in my mind, and thus in my comment.

In that comment, I used the example of programs performing an ascending sort or a descending one. While both programs would be valid, one of them, at least, would not correspond to the intent of the programmer. From an engineering perspective, that would be considered a bug.

I guess an informal yet hopefully apt definition of the word bug could be "an error in the source code of a program leading to an incorrect behaviour of that program at runtime". That incorrect behaviour can take many forms: the most obvious one is the program breaking in the middle of a computation, without providing any result (a semantic bug). A second one is when the compiler will not accept the program as valid (a syntactic bug). A third one is the program producing the wrong result, as in my example (also a semantic bug).

In my mind, I only considered the first 2 kinds of errors as bugs, and qualified the last as something else, perhaps for the reason that only the programmer may really know the intent behind a program's implementation.

One of the goals when designing a programming language is to help reduce the occurrence of bugs. The main strategy is to turn bugs of the first kind (semantic) into bugs of the second kind (syntactic), or at least that is my understanding.

Concretely, with a powerful enough type system, one may express expected properties of a program using the provided syntax, and let the compiler validate these claims using only formal rules.

Re: Strong arrows: a new approach to gradual typing

#82

Post by josevalim »

charcircuit wrote: post #74
josevalim wrote: post #67

Earlier quoted context omitted.

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

It is impossible to ignore the set theoretic type aspects, because the whole foundation of strong arrows is based on being able to negate a type. If I don't explain the set theory bits, then the rest of the article falls apart.

I could perhaps rearrange some of those sections but that doesn't change my main argument: the type system is not being designed for type theoretic people. At best, you could say the _article_ focus too much on theory, rather than on the practical bits.

Re: Strong arrows: a new approach to gradual typing

#83

Post by ChrisRackauckas »

jovial_cavalier wrote: post #70
adgjlsfhk1 wrote: post #65

Earlier quoted context omitted.

It's worth noting that the benchmarkgame is including startup time. If you look at the execution time (which is what matters once you start doing more work) the speeds are equal. For example, https://arxiv.org/pdf/2207.12762.pdf shows Julia beating hand codes BLAS kernels for the 2nd fastest supercomputer in the world.

I agree that if you keep increasing n on any of these benchmarks, Julia and C should start to approach each other, but the JIT overhead is not meaningless. I think there’s a reason benchmarkgame includes it. It sounds, though, like they’ve started to seriously address this in versions more recent than what I’ve played with. I suppose I’ll check it out again.

I agree JIT overhead is not meaningless, but it's pretty odd that only some programming languages in the benchmark measure compilation time while others do not. If we really think it's not meaningless, then other languages (C, Fortran, etc.) should include that in the timing as well. Even better would be to have timings which include compilation and which do not. Then we would have a nice way of making a multi-dimensional comparison about the latency and runtime.

Currently, Julia's benchmarks add its compilation time while the building of the C binaries is not measured in its, so it's not a direct 1-1 comparison. And we don't have the numbers in there to really know how much of an effect it has either. More clarity would just be better for everyone.

Re: Strong arrows: a new approach to gradual typing

#84

Post by jovial_cavalier »

ChrisRackauckas wrote: post #83
jovial_cavalier wrote: post #70

Earlier quoted context omitted.

I agree that if you keep increasing n on any of these benchmarks, Julia and C should start to approach each other, but the JIT overhead is not meaningless. I think there’s a reason benchmarkgame includes it. It sounds, though, like they’ve started to seriously address this in versions more recent than what I’ve played with. I suppose I’ll check it out again.

I agree JIT overhead is not meaningless, but it's pretty odd that only some programming languages in the benchmark measure compilation time while others do not. If we really think it's not meaningless, then other languages (C, Fortran, etc.) should include that in the timing as well. Even better would be to have timings which include compilation and which do not. Then we would have a nice way of making a multi-dimens…

That's because, until recently, you compiled every time you ran with Julia. It's not the case with C.

Re: Strong arrows: a new approach to gradual typing

#85

Post by josevalim »

moljac024 wrote: post #72
josevalim wrote: post #32

Earlier quoted context omitted.

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?

If it comes to this, we will certainly need to have a discussion on the topic. So I am definitely open to discussing the idea!

Re: Strong arrows: a new approach to gradual typing

#86

Post by tjrgergw »

jovial_cavalier wrote: post #84
ChrisRackauckas wrote: post #83

Earlier quoted context omitted.

I agree JIT overhead is not meaningless, but it's pretty odd that only some programming languages in the benchmark measure compilation time while others do not. If we really think it's not meaningless, then other languages (C, Fortran, etc.) should include that in the timing as well. Even better would be to have timings which include compilation and which do not. Then we would have a nice way of making a multi-dimens…

That's because, until recently, you compiled every time you ran with Julia. It's not the case with C.

It has NEVER been the case that you have to compile a function every time you run it.

Re: Strong arrows: a new approach to gradual typing

#87

Post by OkayPhysicist »

Aerbil313 wrote: post #75
OkayPhysicist wrote: post #71

Earlier quoted context omitted.

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?

Definitely nothing in the mainstream. The closest you get is a couple of Actor-model libraries for Java and C#, but since languages weren't built from the ground up around it, you end up with a lot of jagged edges that simply don't exist in Erlang or Elixir. Outside of the functional paradigm, there are a lot of things you can express that simply cannot be translated into a distributed environment.

The other "in the same ballpark" thing that is much more mainstream is microservice architecture. They aim for the same goal, of achieving concurrency-modeled parallelism and fault tolerance by translating a system into a distributed one, but since microservices tend to be hacked together with a variety of languages with no intrinsic support for the paradigm, you end up with an "ad hoc informally-specified bug-ridden slow implementation of half of Erlang."

There's a few projects even further outside the mainstream than Erlang and Elixir that are taking a swing at it, but they're all extremely obscure, and IMO haven't yet demonstrated any novelty worth sacrificing the vast libraries available on the BEAM.

Post reply on HN