Live data from Hacker News

Elixir v1.20: Now a gradually typed language

elixir-lang.org

381–390 of 426 posts

Re: Elixir v1.20: Now a gradually typed language

#381

Earlier quoted context omitted.

For my $0.02 - it depends where you want to put the onus Statically typed languages put the onus on the caller to transform the data into the shape(s) required. Dynamically typed languages put the onus on the called to handle anything. That is, in a dynamically typed environment your function has to defensively code for every possible type it could be handed.

Nobody writes dynamically typed functions that can be called with any possible type. It's not about that at all. Static types give you errors reliably at compile time instead of randomly at runtime, better documentation of what the code expects (people writing dynamically typed languages eventually resort to type comments), working IDE support, reliable refactoring and better code, all of which results in faster deve…

> (people writing dynamically typed languages eventually resort to type comments)

This has never been an issue in Elixir, because instead of a comment, you'd just improve the pattern matching in the function definition.

    def blah(%{students: [%{firstname: firstname, lastname: lastname}|[]], count: cnt}) when is_int(cnt):
      fullname = firstname  lastname
Is a valid function declaration, which specifies that blah takes a dictionary that contains at least 2 keys, :count, who's value is an integer, and :students, who's value is a length-1 list who's first element is a dictionary that contains the keys :firstname and :lastname

Re: Elixir v1.20: Now a gradually typed language

#382
post #376

I wanted to use functional programming in actual projects and Elixir's lack of static types almost stopped me from picking it up initially. I tried it out and, although I do miss static types sometimes, immutability and not having to deal with inheritance and other OO abstractions has made the trade-off worth it for me. Yes some people do claim that pattern matching makes up for the lack of static types. I don't agre…

Statically typing the underlying message passing model used in Erlang is pretty hard, because the mailbox of a process can accept any type of message. And so, it cannot be statically typed in general, since anyone who holds a process id can shove a message into that mailbox. In contrast, Go's message passing model works on typed channels. A channel has a type, and only accepts messages of the given type. The `receive…

Why, consider: mailbox → pattern matching → fully statically typed code.

It's not unlike the standard HTTP-based API → routing and parsing → fully statically typed code.

Re: Elixir v1.20: Now a gradually typed language

#383

I wanted to use functional programming in actual projects and Elixir's lack of static types almost stopped me from picking it up initially. I tried it out and, although I do miss static types sometimes, immutability and not having to deal with inheritance and other OO abstractions has made the trade-off worth it for me. Yes some people do claim that pattern matching makes up for the lack of static types. I don't agre…

I've been writing Elixir for ~12 years now, and I also don't think pattern matching is what prevents types errors, I believe it's more foundational than that.

The biggest advantage in this regard is that Elixir (and Erlang) only has ~13 data types: atoms, booleans, strings (binaries/bistrings), floats, functions, integers, lists, maps, pids, ports, refs, maps, records, structs, tuples.

Combine the limited data types with the fact that those data types are pure data and not coupled to behavior (like OOP languages)-- it creates an environment where type errors are extremely easy to identify, correct, and limited in scope. The syntax also makes this easy, because they're generally visually distinct, it's obvious what something is and in practice 90%+ of the code written involves: string, floats, integers, lists, maps, structs, and tuples.

The only real source of type errors I encounter are between the types that become visually difficult to distinguish from: maps and structs (with a shoutout to keyword lists which are a special variant of a list). And the "type errors" are almost always due to 'Access' not being implemented on structs.

When I first started programming in Elixir, I was a huge fan of static types having enjoyed the pure madness that is Scala. All these years later, I find myself questioning my sanity back then. It really feels like a lot of the love static typing gets is due to fundamental issues with larger paradigm issues cough OOP cough than static types being a necessary feature to write good error-free code.

Re: Elixir v1.20: Now a gradually typed language

#384

Earlier quoted context omitted.

That’s very exciting! Is there anywhere I could follow you for updates? If you don’t want to share it publicly, and is ok with sharing it privately, my email is my username on gmail. Thank you!!

We're hoping to have a preprint ready at the end of the month, I'll send it to you then!

I'd like to see this paper too! Email in my profile.

Recently I came across this paper that explores the "Design by Contract" technique for LLMs: https://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=112...

Re: Elixir v1.20: Now a gradually typed language

#385
post #376

I wanted to use functional programming in actual projects and Elixir's lack of static types almost stopped me from picking it up initially. I tried it out and, although I do miss static types sometimes, immutability and not having to deal with inheritance and other OO abstractions has made the trade-off worth it for me. Yes some people do claim that pattern matching makes up for the lack of static types. I don't agre…

Statically typing the underlying message passing model used in Erlang is pretty hard, because the mailbox of a process can accept any type of message. And so, it cannot be statically typed in general, since anyone who holds a process id can shove a message into that mailbox. In contrast, Go's message passing model works on typed channels. A channel has a type, and only accepts messages of the given type. The `receive…

[deleted]

Re: Elixir v1.20: Now a gradually typed language

#386
post #376

I wanted to use functional programming in actual projects and Elixir's lack of static types almost stopped me from picking it up initially. I tried it out and, although I do miss static types sometimes, immutability and not having to deal with inheritance and other OO abstractions has made the trade-off worth it for me. Yes some people do claim that pattern matching makes up for the lack of static types. I don't agre…

Statically typing the underlying message passing model used in Erlang is pretty hard, because the mailbox of a process can accept any type of message. And so, it cannot be statically typed in general, since anyone who holds a process id can shove a message into that mailbox. In contrast, Go's message passing model works on typed channels. A channel has a type, and only accepts messages of the given type. The `receive…

Maybe you’re implying that message passing makes compile-time validation of messages difficult? The types themselves are a solved problem, as long as you allow actors to fail when they receive a message they can’t handle.

Re: Elixir v1.20: Now a gradually typed language

#387

I wanted to use functional programming in actual projects and Elixir's lack of static types almost stopped me from picking it up initially. I tried it out and, although I do miss static types sometimes, immutability and not having to deal with inheritance and other OO abstractions has made the trade-off worth it for me. Yes some people do claim that pattern matching makes up for the lack of static types. I don't agre…

I've been writing Elixir for ~12 years now, and I also don't think pattern matching is what prevents types errors, I believe it's more foundational than that. The biggest advantage in this regard is that Elixir (and Erlang) only has ~13 data types: atoms, booleans, strings (binaries/bistrings), floats, functions, integers, lists, maps, pids, ports, refs, maps, records, structs, tuples. Combine the limited data types…

Sounds very similar to my experience with Clojure. I think Elixir and Clojure are alike in that regard.

Re: Elixir v1.20: Now a gradually typed language

#388

Theres is also gleam that did this "upfront", and actully has a decent type system, im not sure if this effort is that relevant. On the flipside this is a good effort nontheless. For go there is also lisette ( https://github.com/ivov/lisette/ ) that has a very similar dev-exp to gleam. As a bonus you get all the goodies if go and a static binary. Lots of stuff happening in the language space at the moment.

Lisette actually looks really nice! I huge improvement over Go (even i am really fond of the go runtime)

Re: Elixir v1.20: Now a gradually typed language

#389

Earlier quoted context omitted.

I don’t know if it satisfies “already convenient to use”, but IMO ocaml fits “adds great features reliably and safely”. They merged their multicore compiler ~4 years ago, which was a pretty huge change that added parallelism through domains. Notably, they had a working version ~10 years ago, but refused to merge it until they sorted out some performance issues that would have affected existing single-threaded code. I…

IMO OCaml is mind-bending (e.g. go figure out the 'in' keyword, I still don't understand it), F# is much easier/simpler.

Ocaml is just an ML in the traditional sense. It keep scope without curlies. There is really not much else to it.

Re: Elixir v1.20: Now a gradually typed language

#390
post #373

Earlier quoted context omitted.

Types do not inherently have any such restrictions. A value can belong to several types. In fact, if you posit types to have union, that necessarily follows.

I think they do, and as you mentioned you can explicitly remove such a restriction. Sets and types are once again two different kinds of objects in mathematical theory, and a set-theoretic type doesn’t seem to be based either on set theory or type theory.

If types have unions/intersections/negations, as you originally seemed to imply, then “a value belongs to just one type” is false (if x is of type A then it’s also of type A ∪ B for any B).

If they don’t unless you add them to “explicitly remove such a restriction”, then that means you’re making types more set-like (set-theoretic).

In strict “type theory”, it’s the latter: types don’t have unions (in the sense that set-theoretic types do). There are sum types, which are different.

Post reply on HN