Closed sile closed 1 year ago
Thanks. I have fixed the spec with a slightly more accurate commit (keeping the relationship between argument and return value clear).
Thank you!
Joining late to the party.
The commit that adds these changes (commit) makes the assumption that the type variable State
is somewhat bound to its type (state()
). However, due to how Dialyzer works, any type variable State
mentioned in the type signature is bound to its value State :: state()
, i.e., that the exact same State
value is taken as (part of its) input and the exact same State
value is returned as part of the its output. (OTP note clarifying that here, see Note)
Not sure if this helps... Dialyzer will not complain (AFAIK) if you do not pass the exact same value, but this is really the semantics that the type spec describes
That note is not phrased the best. Read the few lines above the note. In type specs a variable refers to a type, not to an exact value. So -spec f(St) -> St.
doesn't mean that St
is unmodified, it means that the function returns the same type it takes as argument. And -spec f(St) -> St when St :: state().
just adds some more information about the type of St
but again it doesn't mean that the value will be returned unmodified.
Where did you find this sentence written or implied?
Read the few lines above the note. In type specs a variable refers to a type, not to an exact value.
Regarding:
So -spec f(St) -> St. doesn't mean that St is unmodified, it means that the function returns the same type it takes as argument (a polymorphic identity function).
I do not think this is correct. In any other language, generics such as the one defined for your f
function normally follow the semantics of System F (in functional languages) so you would be correct. In the type system defined for Erlang, the type variable St
refers to the same value, not type. Thus, -spec f(St) -> St when St :: state()
also refers to the same exact value.
I am not saying that I agree with the semantics...
Nevermind I think you are correct. I wonder why I learned the opposite but it was a long time ago.
I don't think it is worth updating all the code now though but I will try to switch practice for new code.
We probably have a few places wrong as well in OTP, so hopefully with time we can move to the typical System F semantics 😄
So what about this then?
f(items(X)) -> X when X :: mytype().
AFAIK, the value of X
must be the same. AFAIK, Dialyzer does not "understand" types in the typical sense, it works with values
however, at the moment, I think there are issues that make Dialyzer unable to check this, but the semantics are that they expect the same value. Independently of Dialyzer, the types in Erlang should say that they expect the same value
Could there be a way added that would show the relationship between argument/return values? This may not be useful for the type system or Dialyzer but it's useful for documentation (and is probably where my confusion comes from since this originally came from edoc I believe). In the commit's context it tells me I should dismiss what I passed as an argument and use the returned value for any subsequent operations for example, without having the documentation read "takes a state and returns an updated state".
Could you elaborate on the idea? I am going to use some extra notation that does not exist to capture what I think you mean:
-spec f(-tuple()) -> tuple().
In the code above, -tuple()
means that the input value (a tuple) can be discarded or should not be used anymore by the call-site, and that the return value (a tuple()
) can be used.
Essentially, you are asking if there is a way to statically make sure that something marked as "old state" is not used anymore, as follows?
State = ...,
NewState = f(State),
State # error, 'State' was marked as unusable
In other words, you do not want an object (because of mutation), but you are looking for a way to say: "do not use the old state". In some languages, you have the consume(X)
which means that X
is "nullified" and a type system can prevent further uses of X
, but only when you also have linear types (e.g., Rust ownership, Pony language with iso
, etc)
Essentially, you are asking if there is a way to statically make sure that something marked as "old state" is not used anymore, as follows?
Yes but only from the point of view of documentation. Sometimes it makes sense to use the old and new value (for example for logging when debugging). I do not think we want to prevent reuse strictly. Maybe a Dialyzer option could warn about this though.
I don't know if your spec example would work without variables though. I'm thinking more that the when State :: state()
could use a different notation than ::
to indicate this.
ok, you are right, I forgot the type variables :)
it could be cases like -spec foo({ok, State}, [State]) -> State when State :: tuple()
where that would mean that the input values that use the type variable State
should not be used anymore? I can see some of its advantages, but also that it can be tricky for people to use, specially because it is easy to misunderstand the existing type system...
I see more future in changing the existing semantics of types (values) in Dialyzer to use more common generics (System F semantics), but this is a different issue
If you would like, feel free to open a ticket in erlang/otp and explain your proposal 😃
Right it can be confusing. No I think I'll leave it at that, I'm just mind blown and trying to cope. But if there is a possibility of the semantics changing in the future perhaps I should just continue to do it "wrong" and then fix only when Dialyzer starts complaining (if ever).
Thanks for the discussion, cheers.
cowlib
contains the following-spec
that is now invalid on the Erlang/OTP master branch as https://github.com/erlang/otp/pull/6864 was merged.The compile error is as follows:
This PR fixes this error by replacing the unbounded
State
variable withstate()
type.