Live data from Hacker News

Strong arrows: a new approach to gradual typing

elixir-lang.org

51–60 of 87 posts

Re: Strong arrows: a new approach to gradual typing

#51

Earlier quoted context omitted.

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

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.

https://github.com/JuliaLang/PackageCompiler.jl

https://julialang.github.io/PrecompileTools.jl

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

Re: Strong arrows: a new approach to gradual typing

#52

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.

> 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

And in the past too!

In my Haskell workflow I constantly use the _ (typed hole) keyword. When the compiler hits that expression, it tells me what type I have to put there.

If I were using Idris, it can oftentimes provide and implementation too!

Two caveats about what you said though:

- More power is not always better (depending on how you define power). Structured programming removes the power of goto. Functional programming removes the power of mutation.

- There are limitations to what can be inferred. The more your type system can do, the harder it is for type inference to do its thing.

Re: Strong arrows: a new approach to gradual typing

#53

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…

This talk is so good!

Re: Strong arrows: a new approach to gradual typing

#54

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.

Do you have an example of a practical and useful type system? One that's not "for type theory people" ?

Re: Strong arrows: a new approach to gradual typing

#55

Earlier quoted context omitted.

I would add some more points. 6. Livebook, Jupyter notebook are amazing in Python, Livebook is the same but for Elixir. Also you can connect to your running environment and interact with it. 7. The Nx ecosystem, ML is not only a Python thing now, Elixir is completely usable for ML now. 8. Ash framework, this is not a web framework but a framework for your domain, it's amazing

absolutelt hard agree on livebook, but I think thats not an immediate thing every webdev needs. but speaking from recent practice, it is laughably simple and kinda mindblowing for non-experts in this stuff. Like, I klick me a few smart cells to interact with external data and get a connection/data, write a few straightforward logic modules to do something, and a super simple form for users of this thing (like two inp…

I've replaced postman (and postman likes) with a liveview notebook. It's absolutely great. No need to mess with weird plugins or mentally have to parse responses, you can just use cells that use real elixir to do that.

It's really nice

Re: Strong arrows: a new approach to gradual typing

#56
post #9

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.

I guess I'd be glad to have my type system designed by people well grounded in theory.

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.

Re: Strong arrows: a new approach to gradual typing

#57
post #54

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.

Do you have an example of a practical and useful type system? One that's not "for type theory people" ?

Java

Re: Strong arrows: a new approach to gradual typing

#58

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.

I'm not saying that having a foundation in bad, but you need the right foundation. If a foundation results in compile times ballooning people writing 100 line toy programs won't care, but people writing millions of lines will.

Re: Strong arrows: a new approach to gradual typing

#59

Earlier quoted context omitted.

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.

Most code is that. N-body problems and computing the julia set are cool and beautiful and important. But most code is plumbing scripts that get run for .5s 10,000,000 times a day.

Re: Strong arrows: a new approach to gradual typing

#60

Earlier quoted context omitted.

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

Most code is that. N-body problems and computing the julia set are cool and beautiful and important. But most code is plumbing scripts that get run for .5s 10,000,000 times a day.

Sure, if you're solving easy problems python will be fine.
Post reply on HN