Beta release

[josefs]

Beta release

[josefs]

One thing I think we should wait with until after the beta is constraint solving.

One reason is that implementing constraint solving is going to take a bit of time. But it also doesn't hurt that much to not do constraint solving since we will just accept more programs. However, some error messages will look worse, but I think that's ok in a beta release.

[zuiderkwast]

Here's a list of OTP modules where we crash, by Josef and Pierre.

Jag fixade några av dessa igår kväll. Följande går igenom med ok: inet6_tcp, inet6_udp, inet_hosts, inet_tcp

Följande kraschar inte längre, men ger typfel: erl_epmd, erts_debug, inet_tcp_dist, io_lib_fread

Jag gick snabbt igenom de resterande och klassificerade med avseende på varför de kraschar:
Binary comprehensions: base64, gl, inet_res, lib, wxAcceleratorTable, wxCheckListBox, wxChoice, wxComboBox, wxControlWithItems, wxDC
Empty after-block: beam_lib, dets, dets_utils, erl_tar, gen_sctp, pg2, qlc, qlc_pt, xmerl_b64Bin, xmerl_xpath_parse, zip
unhandled type_error,record : dets_v9
unhandled arith_error: digraph
printing of function types: log_mf_h
unhandled undef usertype: rand

Flera av de här problemen är ganska lätta att fixa. Stöd för binary comprehesions är väl den mest komplicerade att lösa.

Det problemet som jag beskrivit som ”Empty after-block” är lite mystiskt. Det är något jag inte förstår om representationen av after-block i try-uttryck som jag behöver gräva lite i.

(...)

Av de moduler som vi får typfel i så beror flera på att vi inte hanterar import-statements just nu.

[zuiderkwast]

What were the crashes we got when checking OTP? @Zalastax you had a list I think. Binary comprehensions was one of them. What more?

[zuiderkwast]

Draft of summary of what we have achieved so far when releasing this beta:

FEEL FREE TO EDIT

• A bidirectional typechecker using a gradual type system; let's call it TYPED ERLANG! (The logo could have an italic all-caps typewriter font from the early computers.)
• Handling all of Erlang's expression syntax
• Handling all of Erlang's data types, with informal and carefully chosen but far from perfect typing rules
• Experimental extensions of Erlang's type language, by intersection types and generalized integer ranges
• Optional, experimental support for local type interference
• AST retrieval from .erl and .beam files, pretty-printing of types and error reporting
• Substitution of type aliases in specs and some handling of annotated types, with cycle detection
• Basic type refinement of patterns in clauses, not using guards
• Basic exhaustiveness-checking of clauses
• CLI interface and Erlang interface
• Basic documentation and comprehensive messages

Future work, not covered included in this beta release:

• Constraint solving for type variables
• Type refinement using guards (can be a fairly wide topic)
• Formal or at least somewhat carefully described typing rules
• Thorough documentation
• Reworked code, API, set of options and formatting of error messages
• Make it pass its own type checking of itself; self-gradualization

[josefs]

Excellent summary, @zuiderkwast! And sorry for being slow to reply.

There's one point that I'd like to change a bit. It's the one about local type inference. I don't think we need to explicitly state that it breaks the graduality property, in fact, after thinking about it some more I don't think it fails, or fails in a way that one can instead give a weaker property. Anyhow, I think we should just remove the theoretical aspects of this point.

It'd also be nice to say something about the Elixir support. Perhaps reach out to @OvermindDL1 about gradualixir on whether they want to be part of an announcement.

Personally I think it'd be good to get #217 done before we make a release as it is a rather fundamental change. I think we should just go ahead and make the change.

@zuiderkwast would you like to drive the process of releasing the beta? You seem to have a bit of momentum. I'll be traveling for the next week and a half so my availability might be spotty.

[zuiderkwast]

Fine, let's add #217 to the milestone!

Regarding gradualixir, sure! I don't know much about it, but a simple link at least, or what do you say @OvermindDL1?

I'm a litte worried about a pretty-printing callback for elixir because we have some extensions to the type syntax and custom pretty-printing for those cases (intersection and ranges and in some cases even a list instead of a type, which comes from a multi-clause spec but should probably be converted to an intersection of fun types).

We don't need to do much apart from tagging a version in git, right? I can do that.

Or do you want to announce it on erlang-questions? (Btw, there was someone else announcing a new type system on erlang-questions recently. He invented a new type syntax which is written in comments. I don't think it will be very successful. It seems simply overriding specs would solve his use cases.)

At some point, I'd like to write some introduction in the form of simple reasoning about the fundamental problems with set-based static types in an environment where types are unknown, e.g. passing the result from receive to a function like integer_to_list, just as a very easy to understand point of why a new type system is needed.

(Not related to this, but I'd also like to find some time to write down some thoughts from reading the paper, e.g. the concretization and the definition of gradual extrema (semantics of Int & ? and Int | ?) and how I think they should be interpreted for our practical needs. It's interesting that you're mentioning interference now, because I'm just now starting to grasp also the second part of the paper, the applicative concretization function, which is producing the discjuctive normal form for arrow types, which seems to be needed for inference.

[OvermindDL1]

I'm a litte worried about a pretty-printing callback for elixir because we have some extensions to the type syntax and custom pretty-printing for those cases (intersection and ranges and in some cases even a list instead of a type, which comes from a multi-clause spec but should probably be converted to an intersection of fun types).

As long as it's a term I could write a converter, if it's a string, well, it shouldn't be a string. ^.^

It'd also be nice to say something about the Elixir support. Perhaps reach out to @OvermindDL1 about gradualixir on whether they want to be part of an announcement.

Does Elixir code 'gradualize' better now? Have you included your own mix runner? The gradualixir is just a mix plugin that calls to gradualizer, nothing else, and if you include a mix plugin yourself then all the better. I can't really post it onto the hex package manager for mix plugins and tasks without gradualizer being on there yet (otherwise people need to use it from git, meaning that 'they' can't then be on hex and so forth), but if that's planned and gradualixir is still needed then tell me shortly before-hand and I'll catch it up to date (may have a question or two about the new interfaces, are you all on IRC somewhere?) then publish it as soon as gradualizer is on hex as well. If someone else wants to take and handle gradualixir as well then by all means, I highly encourage it. ^.^

Making a hex plugin and including it into gradualizer wouldn't be hard, it doesn't need to be written in elixir, erlang is fine (they all compile down to the same code), it just needs to be a specially named module and fulfill a specific behaviour.

[zuiderkwast]

As long as it's a term I could write a converter

OK, sounds good! A type error is still represented as a tuple, where some element is an expression or a type, which in most cases is the same as returned by erl_parse and used by the erlang compiler.

Does Elixir code 'gradualize' better now?

We still don't handle refinement of maps very well, which seems to be important for Elixir code, so maybe it's not yet ready for broader use on Elixir. It's up to you to judge.

Have you included your own mix runner?

I don't know what that is, but can't gradualixir do that an just have gradualizer as a dependency? I think it would be good to keep everything Elixir specific in a different repo.

I can't really post it onto the hex package manager for mix plugins and tasks without gradualizer being on there yet

That's a good point. I guess we want to put gradualizer will be on hex soon once we have a beta, so I realize there's no point to put gradualixir on hex until we have that.

are you all on IRC somewhere?

No, not regularily, but feel free to email me. I'm in the git log.

I agree, all this is not very hard, but it requires some checking, making a test repo to check that it works as a dependency and so forth. Non of us seem to having a lot of extra time to kill. But it makes sense to wait until we have it on hex then perhaps. It's good to know you're still around when the time comes!

[OvermindDL1]

We still don't handle refinement of maps very well, which seems to be important for Elixir code, so maybe it's not yet ready for broader use on Elixir. It's up to you to judge.

Yeah maps are used everywhere in Elixir, as a replacement of Records, so they are utterly everywhere, basically they are pretended to be a row-typed record instead of a structural record like erlang records.

I don't know what that is, but can't gradualixir do that an just have gradualizer as a dependency? I think it would be good to keep everything Elixir specific in a different repo.

Once it's on hex.pm yep. If you wanted to include the mix task straight in, it would just be a specially named erlang file with a specially named function in it.

That's a good point. I guess we want to put gradualizer will be on hex soon once we have a beta, so I realize there's no point to put gradualixir on hex until we have that.

It won't even let me yet due to having a non-hex dependency. ^.^;

Non of us seem to having a lot of extra time to kill.

Quite relate...

It's good to know you're still around when the time comes!

Yep, just ping me, I'm open to being pinged. ^.^

[erszcz]

We still don't handle refinement of maps very well, which seems to be important for Elixir code, so maybe it's not yet ready for broader use on Elixir. [...]

I'm proofing Gradualizer in a prod Erlang code which heavily relies on maps instead of records and some glitches pop up. I've recently added some should_pass tests for maps, but getting into the codebase to fix them is a bit over my head - at least in the limited time I could spend on it :/