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

41–50 of 87 posts

Re: Strong arrows: a new approach to gradual typing

#41

Post by pxeger1 »

sodapopcan wrote: post #28
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.

What exactly do you mean that OCaml has figured out?

Re: Strong arrows: a new approach to gradual typing

#42

Post by dylanowen »

charcircuit wrote: post #7

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.

This is how type systems work, you ground them in a strong theoretical foundation then build on top of that for actual consumption.

Re: Strong arrows: a new approach to gradual typing

#43

Post by jovial_cavalier »

adgjlsfhk1 wrote: post #35
jovial_cavalier wrote: post #22

Earlier quoted context omitted.

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…

This is not true https://benchmarksgame-team.pages.debian.net/benchmarksgame/... shows the middle of the pack julia implementations being over 10x faster than the fastest python implementations including startup and compile time.

On contrived benchmarks, sure. What if I want to, say, parse a json file and print something from it?

I understand that Julia is scientific computing oriented, and is probably faster than Python for those applications, but the fact is that Python is no slouch when it comes to scientific computing. And it can do a lot more, including simple but powerful scripts, which is what I mean when I say "most applications."

Re: Strong arrows: a new approach to gradual typing

#44

Post by anonyfox »

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

I have listed a few points here in the other comment: https://news.ycombinator.com/item?id=37596258

as a more general/subjective/emotional note:

The very pragmatic take on FP makes code in most cases so much easier to reason about. Immutability, no magic coming from some dark corner of the codebase unexpectedly, thinking in steps of data transformation from the get go, piping operator to make this visually pleasant, handling edge cases with pattern matches right at the function head level explicitly, ... and to have stateful stuff, there is OTP right on your fingertips with GenServer/Actor/ETS/... .

And a genserver basically is only just another module that implements certain callbacks and then gets spawned. Modelling some scenarios are are breeze with that. And when I feel like I need some better syntax for some exotic problem I am dealing with, I can bend and stretch my language constructs via hygienic macros right away.

And the whole experience is _extremely_ polished in terms of DX. docs, tests, doctests, interactive shell, a AOT-compiler, a JIT-runtime, and some very high-quality ecosystem bangers, like phoenix/livebook/membrane/boradway/Nx/Axon/... . Its like best of all worlds, and definitively the _very best_ choice for orchestrating stuff, which is a boon when you run into a problem you'd rather not use elixir for. Like building a native extension in rust/zig for some raw CPU task is a breeze.

Its not so much the individual feature (no matter which one) but the overall package.

Re: Strong arrows: a new approach to gradual typing

#45

Post by indigo0086 »

WJW wrote: post #16
daxfohl wrote: 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.

Do you reject learning any language that has been migrated away from by any company? Why not make up your own mind about whether it is nice instead of depending on rumours about other companies? In any case you could have easily googled "brex elixir" and have found their blog explaining their reasoning as the first result: https://medium.com/brexeng/building-backend-services-with-ko...

"Development speed: The future will be great and we want to get there fast. Our choice needs to help us move with urgency and focus. A type-system was a non-negotiable choice here."

While Jose Valim did a good job in his talk about dispelling the idea of type system offering all these promises that may or may not be true, the idea will never die. This could mean that it is the right idea, but it could also mean that now's the time to look into a way to offer it in away it attracts people who have that perception while offering a type system of value.

Re: Strong arrows: a new approach to gradual typing

#46

Post by sodapopcan »

pxeger1 wrote: post #41
sodapopcan wrote: post #28

Earlier quoted context omitted.

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.

What exactly do you mean that OCaml has figured out?

It's a statically typed language that doesn't require explicit type declarations (in most cases, at least).

Re: Strong arrows: a new approach to gradual typing

#47

Post by sodapopcan »

sodapopcan wrote: post #46
pxeger1 wrote: post #41

Earlier quoted context omitted.

What exactly do you mean that OCaml has figured out?

It's a statically typed language that doesn't require explicit type declarations (in most cases, at least).

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?

Re: Strong arrows: a new approach to gradual typing

#48

Post by reuben364 »

tutfbhuf wrote: post #13

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

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.

Re: Strong arrows: a new approach to gradual typing

#49

Post by alphablended »

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…

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 languages, type systems are used to ensure that programs are bug free, following the adage : "if it compiles, it works". The issue of having a proper implementation is not a concern of researchers in their papers, it's purely an engineering problem, so there is no interest for them in using the word correct in that sense.

Also, with type inference, one often does not have to mind too much about types, and instead gradually introduce type annotations to lift disagreements between the compiler and its user.

Gradual typing is yet another tool to achieve a similar result.

Re: Strong arrows: a new approach to gradual typing

#50

Post by tjrgergw »

jovial_cavalier wrote: post #43
adgjlsfhk1 wrote: post #35

Earlier quoted context omitted.

This is not true https://benchmarksgame-team.pages.debian.net/benchmarksgame/... shows the middle of the pack julia implementations being over 10x faster than the fastest python implementations including startup and compile time.

On contrived benchmarks, sure. What if I want to, say, parse a json file and print something from it? I understand that Julia is scientific computing oriented, and is probably faster than Python for those applications, but the fact is that Python is no slouch when it comes to scientific computing. And it can do a lot more, including simple but powerful scripts, which is what I mean when I say "most applications."

> contrived benchmarks

Why is doing actual science more of a contrived benchmark than parsing and printing a json? I think this says more about what you personally do than anything else.

Post reply on HN