[HN Gopher] Type system updates: moving from research into devel...
___________________________________________________________________
Type system updates: moving from research into development
Author : weatherlight
Score : 109 points
Date : 2023-07-04 19:11 UTC (3 hours ago)
(HTM) web link (elixir-lang.org)
(TXT) w3m dump (elixir-lang.org)
| Pannoniae wrote:
| There seems to be a pattern of introducing static types into
| previously weakly typed or dynamically typed languages. I think
| this is because people have written many large projects in them,
| and without types, it's quite hard to enforce an API or document
| what to pass into it if there are no types.
|
| The drawbacks to statically typed languages have become way less
| significant since most of them have "var" or an equivalent which
| saves on typing.
| slondr wrote:
| Elixir never really didn't have a static type system, this is
| just improving it.
| mvdtnz wrote:
| "var" does not "save on typing", at least not in C#. A variable
| declared with var is still statically typed. Its type is just
| inferred from context. The compiler will assign it the most
| specific type possible from that context. That's the important
| point - this occurs at compile time, not runtime.
| tialaramex wrote:
| You have perhaps misconstrued what your parent was saying.
|
| Typing has two meanings, the one intended here wasn't about
| types - it was about keyboards. The var keyword and similar
| syntax in modern languages is less typing where "typing"
| means pushing the little buttons on the keyboard, and the
| associated squiggles appearing on a display.
| weatherlight wrote:
| It's also not your "standard static" type system. It's a new
| type system that novel using Set Theoretical Types. Which is
| kind of interesting. because if Elixir can get this working
| properly, it would also probably work for other Strong
| Dynamically Typed languages.
|
| Imagine if Typescript's type system if it were actually sound.
|
| The research paper is here if anyone wants to read it.
| https://www.irif.fr/_media/users/gduboc/elixir-types.pdf
| srgpqt wrote:
| Indeed, even C has caught up!
|
| #define let __auto_type
| yewenjie wrote:
| Is this type-system guaranteed to be sound? (Does type checking
| ensure no runtime type bugs?). Also, can it infer all the types
| if none of the types are actually annotated?
|
| Also, what is the novelty about this new type system?
| weatherlight wrote:
| Yes. it's guaranteed to be sound. As per what makes it unique,
| from the paper: We present a gradual type
| system for Elixir, based on the framework of semantic subtyping
| [10, 19]. This framework, developed for and implemented by the
| CDuce programming language [3, 15], provides a type system
| centered on the use of settheoretic types (unions,
| intersections, negations) that satisfy the commutativity and
| distributivity properties of the corresponding set-theoretic
| operations [19]. The system is a polymorphic type system with
| local type inference, that is, functions are explicitly
| annotated with types that may contain type variables, but their
| applications do not require explicit instantiations: the system
| deduces the right instantiations of every type variable. It
| also features precise typing of pattern matching combined with
| type narrowing: the types of the capture variables of the
| pattern and of some variables of the matched expression are
| refined in the branches to take into account the results of
| pattern matching
|
| CDuce programming language: https://www.cduce.org
| tannhaeuser wrote:
| I had to double-check that, knowing CDuce as an XML-oriented
| language from when XML was hip around almost twenty years ago
| - and indeed it's that language for manipulating XML. It's
| been a while but I thought the point was to experiment with
| static typing of XML transformations, but ultimately type
| inference complexity results hit a wall and weren't
| convincing from a practical PoV. But what do I know - after
| all, adding types on top of a language that isn't statically
| typed seems like a pointless exercise to me when there are
| plenty statically typed languages. I guess it might make
| sense for a Python code base that's gotten out control maybe?
| bcrosby95 wrote:
| It doesn't make sense for certain kinds of languages. But
| Elixir and Erlang unique in a way that languages like
| Python, Ruby, etc. are not.
|
| A semi-mainstream BEAM language with static typing would be
| a huge boon.
| daxfohl wrote:
| Nothing can infer _all_ types. Or even much of a subset:
| https://stackoverflow.com/a/74869648/171121
| losvedir wrote:
| I've used Elixir professionally for 6 years and have been very
| impressed with how it's been managed. All additions seem very
| careful and deliberate. I can't think of any regression or issue
| I've had as the language and tooling and standard library have
| improved.
|
| Given that, I'm excited to see how this works out. Adding static
| types has the potential to be very disruptive but I trust the
| team to do it in a way that will work very well with existing
| Elixir apps and the BEAM VM.
| daxfohl wrote:
| Is set theory more useful than category theory for dynamic types?
| Seems like set theory is less constrained, like a set can be part
| of itself by nature, whereas category theory generally doesn't
| allow mixing containers and elements like that out of the box
| IIUC. Seems like category theory best suits Haskell and such
| where types are more precisely defined (something that could be
| an int or a bool needs an ADT wrapper), whereas set theory might
| make sense for completely dynamic types, where something could be
| an int or a bool or whatever else by nature.
|
| But I'm entirely unsure. Maybe it is completely unrelated to why
| set theory is used as a basis here. Just wondering.
| ccday wrote:
| Very excited to hear about this. Elixir is a fantastic language
| but tooling lags behind some other options, a type system should
| help with that.
| weatherlight wrote:
| > tooling lags behind some other options.
|
| Just out of curiosity. What other options?
| totallywrong wrote:
| Elixir leverages Erlang/OTP and the BEAM which is basically a
| whole platform for applications. Probably only the Java / JVM
| ecosystem is on par.
| weatherlight wrote:
| The tooling in the elixir ecosystem is excelent. The only
| lang/ecosystem that I think does a better job is maybe
| Rust.
| answiftydev wrote:
| The command line tooling is pretty good, the elixirls/ide
| integration is pretty poor compared to other languages I
| have worked with. Some trivial examples while learning
| live view. Using : in pattern matching brings up erlang
| modules, instead of the atom I used elsewhere in the
| file. html.heex and the ~H sigil can't seem to support
| both html and elixir syntax intellsense at the same time.
| I also somehow got def in intellsense to not make a new
| function but instead autocomplete to def(). Finally,
| after hearing how great Ecto was I was hoping it could
| provide some sort of hints based on the names of
| tables/rows I had provided in the migrations.
| dns_snek wrote:
| I love Elixir, I use it daily, but I have to disagree.
| Elixir tooling is in my opinion one of the only sore
| spots of the ecosystem and its quality is seriously
| lagging behind the vast majority of other languages. When
| I say "tooling", I'm talking about language servers and
| overall editor support.
|
| As much as I appreciate the work the team has done, I
| think we have to be honest about the good and bad parts.
| ElixirLS has never worked quite right for me, or most
| other Elixir developers I know. It's often painfully slow
| to respond even in small project, it often gets stuck in
| obscure failures that require an editor reload to get it
| fully working again. If you run into any kind of issue
| with it, the boilerplate response it always: Try running
| `rm -rf .elixir_ls _build` which sometimes works, but
| usually not.
|
| Javascript, Typescript have immaculate tooling in this
| regard, same goes for Java, C#, Go, even Python (on IDE
| side, the package management situation is of course a
| dumpster fire). I'd go as far as to say that any language
| supported by Jetbrains has better tooling than Elixir
| does.
| weatherlight wrote:
| https://github.com/elixir-tools
|
| Check out next-ls aims to replace ElixirLS.
|
| https://www.elixir-tools.dev/next-ls/
|
| There's a podcast/interview from its creator below.
|
| https://podcast.thinkingelixir.com/153
| losvedir wrote:
| I use VSCode at work on our Elixir codebases so I feel
| your pain trying to get ElixirLS working, though when it
| does work it's pretty good. However, on my personal
| laptop I've been trying out the Zed editor which has
| Elixir language server capabilities out of the box (not a
| user installed plugin) and haven't had any issues at all.
| ccday wrote:
| I use IDEA and most typed languages I write (eg Java, Go,
| Python with annotations) have better support for things like
| automated refactoring, bug detection via static analysis, etc
| weatherlight wrote:
| Dialyzer gets you pretty far, Especially since Elixir is
| dynamically typed.
| wofo wrote:
| After spending 6 months working on an Elixir codebase,
| and spoiled by languages with proper IDE support, I'd say
| Dialyzer is nice... But doesn't get even close to what
| I'm used to. Sometimes the benefits of the BEAM and the
| OTP outweight these drawbacks, of course, but to me it
| sucked the joy out of programming (I'm very type oriented
| when writing and, more importantly, reading code).
| doctorpangloss wrote:
| Personally I am most affected by language features that
| didn't exist before September, 2021.
| ljlolel wrote:
| Are you an AI?
| CoastalCoder wrote:
| > (I'm very type oriented when writing and, more
| importantly, reading code).
|
| Me too!
|
| Have you learned any tricks for getting up to speed on
| large code bases with very limited static typing?
|
| In recent years I've mostly worked on large, complex
| Python systems. The consequences of (undisciplined)
| dynamic typing not only sapped my joy in programming, it
| really burned me out.
|
| Some people are really good at living with code bases
| like that. I'm not one of them, but I'm still hoping to
| find some way to bridge the mental gap.
| weatherlight wrote:
| Proposed type system described in more detail here.
| https://www.irif.fr/_media/users/gduboc/elixir-types.pdf
| DonaldPShimoda wrote:
| Ah, thanks for that, I was wondering where the details were!
| Adding this to my pile...
| rocketbop wrote:
| Discussed yesterday also.
|
| https://news.ycombinator.com/item?id=36576352
___________________________________________________________________
(page generated 2023-07-04 23:00 UTC)