Gradualizer
Gradualizer copied to clipboard
josefs
Reverse map assocs check
It seems like some of them make sense. Considering usage is compared to expected.
subtype ( ? t ( # { a => b } ) , ? t ( # { } ) )
Ok probably a mistake. It thinks it expects an empty map in this situation. Also, if the left side is what is produced, even if you write
#{ a => b}
It will be inferred as
#{ a := b }
Here's another one
subtype ( ? t ( # { a => b , c => d } ) , ? t ( # { a => b } ) )
Well yea, you're adding a key that isn't expected? Is the test wrong? The compat stuff is called via subtype. The comment on top says:
%% The first argument is a "compatible subtype" of the second.
Not sure #{ a => b, c => d} is a compatible subtype of #{ a => b }, is it?
@FrankBro both of the examples you bring up are correct. A msub is a subtype of another map msup if it contains at least all the keys of msup. That certainly holds in all of the examples. In the first example, there are no keyes in the supertype so any record is a subtype of that. For the second example, the subtype contains all the keys and more.
A useful analog here might be to think about inheritance in an object oriented language. For instance in Java, you can defined a subclass (which corresponds to a subtype for us) by adding methods and members to an existing class. In a similar vein, we can add keys to a map to form a new subtype of that map.
From that description alone, it would mean #{b := b} is indeed not a subtype of #{a => a, b => b}, which is the initial example I gave. Unless we start to introduce the assoc/exact difference. I guess I'm wondering what's the exact law of map subtyping in this situation. Maybe then it makes sense to go over the second map's keys instead of the first one. We should just skip if it's => and not present in the first one then?
The last change has only 1 failure then. One of them is a known problem being solved. Looking into it.
Alrighty then, name of the branch is bad but everything makes sense. Fixed a known problem, removed a failing test that was supposed to pass and added a few tests. The solution was simpler than anticipated 😅
Codecov Report
Merging #286 (dd3fc2b) into master (c83a9b4) will increase coverage by
0.12%. The diff coverage is91.66%.
@@ Coverage Diff @@
## master #286 +/- ##
==========================================
+ Coverage 87.36% 87.49% +0.12%
==========================================
Files 18 18
Lines 2739 2758 +19
==========================================
+ Hits 2393 2413 +20
+ Misses 346 345 -1
| Impacted Files | Coverage Δ | |
|---|---|---|
| src/typechecker.erl | 90.45% <91.66%> (+0.15%) |
:arrow_up: |
Continue to review full report at Codecov.
Legend - Click here to learn more
Δ = absolute <relative> (impact),ø = not affected,? = missing dataPowered by Codecov. Last update c83a9b4...dd3fc2b. Read the comment docs.
Found a problem. no_match catches too many things. If the same key is used wrong, should be an error. Fixing...
-spec optional_fail() -> #{a => a, b => b}.
optional_fail() -> #{a => b, b => b}.
@josefs
A
msubis a subtype of another mapmsupif it contains at least all the keys ofmsup.
That's not the full story. #{} is the empty map type, where no keys are allowed. If you add keys, it's not a subtype of the empty map. The supertype of all maps is #{top() => top()}.
All keys in the map subtype have to be a subtype of some key in the map supertype and the value must be a subtype of the corresponding value type. A map subtype can also turn optional keys from the supertype into mandatory keys.
@FrankBro
Unless we start to introduce the
assoc/exactdifference.
We already have some handling of optional/mandatory (assoc/exact) associations, although it seems it's not entirely correct.
I'd like to see unit tests in typechecker_tests for map subtyping, to isolate this subtyping logic from other typechecking logic.
@zuiderkwast so then this is wrong? The fact it says a MIGHT be in, does it change anything? It might not be there and therefore, valid.
subtype ( ? t ( # { a => b } ) , ? t ( # { } ) )
This is how I understand map types and a draft of an informal rule for map subtyping: https://github.com/josefs/Gradualizer/wiki/Map-types
@zuiderkwast Thanks for writing this document! That's super helpful and a good basis for further discussion.
That being said, there are a few things that I disagree with. You say "Type #{}: The empty map type has only one value: The empty map #{}. No keys are allowed." But the syntax of Erlang disagrees. Consider the following program:
f(#{}) ->
ok.
I'd argue that it should have the following spec: f(#{}) -> ok. That would mean that we can only call it with the empty map according to you semantics. But the pattern matching semantics in Erlang has subtyping built in. The call f(#{a => b}). doesn't crash, it returns ok.
The same story goes for pattern matching against associations. Here's an example:
h(#{ a := B }) ->
ok.
This function should have the type h(#{ a := B }). But should still be fine to call this function with a map that contains more associations, like h(#{a => b, c => d}) which returns ok if you try it in the repl.
If we're going to have correct type refinement for maps is it vital that we allow the kind of subtyping I outline above.
I'd argue that the function actually has the spec f(#{any() => any()) -> ok. The documentation is quite specific in disallowing more associations. Unfortunately it doesn't talk about subtyping but I believe @zuiderkwast's documentation is correct.
I'd argue that the function actually has the spec f(#{any() => any()) -> ok.
I assume you're referring to the first function. I think it'd be very confusing and unfortunate to give the function that type. We have a piece of syntax, #{}, which occurs both on the type level, as a value, and as a pattern. We should make sure to keep their meaning together. It seems obvious that when patternmatching on an empty map #{}, that such a pattern would give rise to expecting the scrutinee to have the type #{}. Anything else would be confusing.
The documentation is quite specific in disallowing more associations.
What documentation are you referring to? Are you referring to this sentence from the "Types and Function Specifications" section in the reference manual:
The notation #{} specifies the singleton type for the empty map. Note that this notation is not a shorthand for the map() type.
Just because the type denotes a singleton value doesn't mean that it cannot have subtypes.
Unfortunately it doesn't talk about subtyping but I believe @zuiderkwast's documentation is correct.
It's not correct for type refinement of maps. The pattern for the empty map matches all maps, not only the empty map.
We have a piece of syntax,
#{}, which occurs both on the type level, as a value, and as a pattern. We should make sure to keep their meaning together. It seems obvious that when patternmatching on an empty map#{}, that such a pattern would give rise to expecting the scrutinee to have the type#{}. Anything else would be confusing.
The overloaded syntax with different meanings in patterns, expressions and types is confusing indeed. Unfortunately we cannot change the syntax of Erlang patterns and expressions. Regarding types, I think we should follow the reference manual.
A pattern can only have := associations and extra keys don't prevent the pattern from matching. Map patterns are documented in the reference manual for expressions. That means, agreeing with @Zalastax, that the pattern #{} has the type #{any() => any()} (or maybe #{top => top()}). Perhaps we need to clarify somewhere what it means that a pattern has a type, since it's usually values that have types....
The notation #{} specifies the singleton type for the empty map. Note that this notation is not a shorthand for the map() type.
Just because the type denotes a singleton value doesn't mean that it cannot have subtypes.
Well..... it has any() and none() as a subtypes. It probably also has the unknown map (map() or #{any() => any()} as a subtype (since #{} is equivallent to #{none() => none()} and we have any() :: none().) Apart from that, it's similar to other singletons, such as [] and {} IMO.
It's not correct for type refinement of maps. The pattern for the empty map matches all maps, not only the empty map.
That's a very good point❗️ When we do refinement based on patterns, we should be careful. For example, we shouldn't infer the type #{} from the pattern #{}.
I volunteer to add some section about map patterns on in the same wiki page. Probably we should cover it on the refinement page as well.
This is how I understand map types and a draft of an informal rule for map subtyping: https://github.com/josefs/Gradualizer/wiki/Map-types
If I understand the conversation and the documentation above correctly, Gradualizer does not currently support subtyping #{} :: #{_ -> _}?
If I understand the conversation and the documentation above correctly, Gradualizer does not currently support subtyping
#{} :: #{_ -> _}?
I don't remember anymore what's implemented and what's not. We'd need a test or a known problem to figure out. Or just try!
Most of the discussion above is about the confusing difference in the pattern #{}, the value or expression #{} and the type #{} which look the same but are very different. The pattern #{} doesn't have the type #{}.
This PR has been inactive for a long time and significant work has happened on maps in the meantime. I'm closing it. Please let me know if it needs revisiting.
