Type def and spec syntax

classic Classic list List threaded Threaded
7 messages Options
Reply | Threaded
Open this post in threaded view
|

Type def and spec syntax

Robert Virding
Is there any better documentation of type defs and specs than that which occurs in the Erlang Reference manual? If so where is it?

I am trying to define an equivalent type/spec syntax for LFE so I am going through the valid syntax then trying to work out what they mean. And there is a lot of strangeness from simple things like the predefined type names are 'reserved' so this is valid:

-type atom(X) :: list(X).

(whatever it means) to much more strange things like:

-spec foo(Y) -> integer() when atom(Y).
-spec foo(Y) -> integer() when atom(Y :: integer()).

(whatever they mean) neither of which are mentioned in the docs.

So is there a more complete and understandable documentation some where?

Robert

P.S. I am a bad boy with types and really only use specs for saying a function never returns to keep dialyzer quiet. :-)

-spec generate_a_foo_error(any()) -> no_return().


_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions
Reply | Threaded
Open this post in threaded view
|

Re: Type def and spec syntax

Tuncer Ayaz
On 2 October 2016 at 00:56, Robert Virding <[hidden email]> wrote:

> So is there a more complete and understandable documentation some
> where?

It's not documentation, but have you looked at
lib/hipe/cerl/erl_types.erl and lib/hipe/cerl/erl_bif_types.erl?
_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions
Reply | Threaded
Open this post in threaded view
|

Re: Type def and spec syntax

Kostis Sagonas-2
In reply to this post by Robert Virding
On 10/02/2016 12:56 AM, Robert Virding wrote:
> Is there any better documentation of type defs and specs than that which
> occurs in the Erlang Reference manual? If so where is it?

In light of recent discussions on this mailing list, I wish that those
who complain about documentation took a bit of time to tell us which
aspects of the current documentation they find unsatisfactory and why.

It's very difficult to know how to make something "better" if one does
not get told why it's not good enough as it is.


> I am trying to define an equivalent type/spec syntax for LFE so I am
> going through the valid syntax then trying to work out what they mean.

OK, here is a thing I try hard to teach students who take my compiler
courses: Do NOT mix up in your mind(s) syntax and semantics of a
language. They are certainly not the same thing; they may not even be
related in any way.

So it's not particularly surprising that you cannot "work out what they
mean" by looking at the valid syntax of types and specs.


> And there is a lot of strangeness from simple things like the predefined
> type names are 'reserved' so this is valid:
>
> -type atom(X) :: list(X).
>
> (whatever it means) to much more strange things like:
>
> -spec foo(Y) -> integer() when atom(Y).
> -spec foo(Y) -> integer() when atom(Y :: integer()).
>
> (whatever they mean) neither of which are mentioned in the docs.

First of all, why should the above be mentioned in the reference manual,
especially if they are "strange"?

Second, why do you find the first of these examples strange?  Erlang has
been designed so that e.g. functions do not have just some alphanumeric
sequence of characters as a name but their name includes an arity.  This
means that length/1 is reserved (you cannot redefine it), while length/3
is not.

In this prism, why do you find it strange that the atom/1 type is not?
(Only atom/0 is.)


As to what the above examples mean, well it's very simple:

  - The type declaration defines a polymorphic type called atom that is
an alias for the built-in polymorphic type list.  Granted that it's a
very stupid name for this type, but there is nothing that forces good
naming convensions in Erlang.  I can certainly define a length/3
function that takes integer() arguments and returns a binary() of some sort.

  - The first foo/1 spec has no meaning because you cannot use the
atom/1 type as a subtype constraint.  In fact, if you put this spec in a
file and try to compile it, you will get a warning, which is consistent
with the (very bad IMO) philosophy of the Erlang compiler to not refuse
to compule code which is damn stupid.  If you use dialyzer on this spec,
you will discover that this tool is more sane as far as tolerating
constructs which have no meaning.  You will get a dialyzer error in this
case.

  - The second foo/1 spec is rejected even by the compiler.  Have you
actually tried this and the compiler accepted it?


> So is there a more complete and understandable documentation some where?

Suggestions on how to make the current documentation more complete and
understandable are welcome!

Kostis
_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions
Reply | Threaded
Open this post in threaded view
|

Re: Type def and spec syntax

Robert Virding
I think you have reiterated what I said: what does this mean? I worked out myself that the first form:

-type atom(X) :: list(X).

works as the pre-defined types are not "reserved words" in any sense. BUT THIS IS NOT STATED IN THE DOCUMENTATION. I discovered it by looking at the what the parser output.

So I continued to look in the parser to see if there were more things which are allowed but not documented and I found the second two (plus more). So my question was what do they mean? While my examples may be erroneous does this syntax have any possible meaning at all? You seem to imply that it doesn't. If not why is is there at all? Was someone just having a wild time chucking in whatever they could dream up? And it if can be used in a meaningful way why isn't it documented? I think that having syntax which can never legal is a great way to complicate things. Which we don't need.

I quite agree that semantics is the important thing but we need syntax to express ourselves. And if the documentation doesn't cover all the legal syntax then all legal syntax might have a meaning so it is reasonable to ask what it means.

So my suggestion is that the documentation should cover all legal type syntax. And that we should remove all syntax which can never be legal.

Robert


On 2 October 2016 at 20:42, Kostis Sagonas <[hidden email]> wrote:
On 10/02/2016 12:56 AM, Robert Virding wrote:
Is there any better documentation of type defs and specs than that which
occurs in the Erlang Reference manual? If so where is it?

In light of recent discussions on this mailing list, I wish that those who complain about documentation took a bit of time to tell us which aspects of the current documentation they find unsatisfactory and why.

It's very difficult to know how to make something "better" if one does not get told why it's not good enough as it is.


I am trying to define an equivalent type/spec syntax for LFE so I am
going through the valid syntax then trying to work out what they mean.

OK, here is a thing I try hard to teach students who take my compiler courses: Do NOT mix up in your mind(s) syntax and semantics of a language. They are certainly not the same thing; they may not even be related in any way.

So it's not particularly surprising that you cannot "work out what they mean" by looking at the valid syntax of types and specs.


And there is a lot of strangeness from simple things like the predefined
type names are 'reserved' so this is valid:

-type atom(X) :: list(X).

(whatever it means) to much more strange things like:

-spec foo(Y) -> integer() when atom(Y).
-spec foo(Y) -> integer() when atom(Y :: integer()).

(whatever they mean) neither of which are mentioned in the docs.

First of all, why should the above be mentioned in the reference manual, especially if they are "strange"?

Second, why do you find the first of these examples strange?  Erlang has been designed so that e.g. functions do not have just some alphanumeric sequence of characters as a name but their name includes an arity.  This means that length/1 is reserved (you cannot redefine it), while length/3 is not.

In this prism, why do you find it strange that the atom/1 type is not? (Only atom/0 is.)


As to what the above examples mean, well it's very simple:

 - The type declaration defines a polymorphic type called atom that is an alias for the built-in polymorphic type list.  Granted that it's a very stupid name for this type, but there is nothing that forces good naming convensions in Erlang.  I can certainly define a length/3 function that takes integer() arguments and returns a binary() of some sort.

 - The first foo/1 spec has no meaning because you cannot use the atom/1 type as a subtype constraint.  In fact, if you put this spec in a file and try to compile it, you will get a warning, which is consistent with the (very bad IMO) philosophy of the Erlang compiler to not refuse to compule code which is damn stupid.  If you use dialyzer on this spec, you will discover that this tool is more sane as far as tolerating constructs which have no meaning.  You will get a dialyzer error in this case.

 - The second foo/1 spec is rejected even by the compiler.  Have you actually tried this and the compiler accepted it?


So is there a more complete and understandable documentation some where?

Suggestions on how to make the current documentation more complete and understandable are welcome!

Kostis


_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions
Reply | Threaded
Open this post in threaded view
|

Re: Type def and spec syntax

Fred Hebert-2
On 10/03, Robert Virding wrote:
>And it if can be used in a
>meaningful way why isn't it documented? I think that having syntax which
>can never legal is a great way to complicate things. Which we don't need.

The three samples for syntax were:

-type atom(X) :: list(X).
-spec foo(Y) -> integer() when atom(Y).
-spec foo(Y) -> integer() when atom(Y :: integer()).

So here's a valid way to use them that is useful, at the very least in
some cases:

    -module(mod).
    -export([main/0]).
   
    -type collection(K, V) :: #{K => V}
                            | dict:dict(K, V)
                            | gb_trees:tree(K, V).
   
    -spec lookup(K,F,C) -> V when
                  C :: collection(K, V),
                  F :: fun((K, C) -> V).
    lookup(K, F, C) -> F(K, C).
   
    main() ->
        C = maps:from_list([{a,1},{b,2},{c,3}]),
        lookup(b, fun maps:get/2, C),
        lookup("bad ignored type", fun maps:get/2, C),
        lookup(b, C, fun maps:get/2).

This module defines an accessor function using the parametrized types
and 'when' parts of typespecs syntax. Sadly the analysis is currently
not good enough to figure out that "bad ignored type" is not an
acceptable value of `K' for the lookup (it appears dialyzer does not do
the parametrized inference this deep), but in the third call, it can
definitely infer that I swapped the collection and the accessor
function:

    mod.erl:13: Function main/0 has no local return
    mod.erl:17: The call mod:lookup('b',C::#{'a'=>1, 'b'=>2,
    'c'=>3},fun((_,_) -> any())) does not have a term of type
    dict:dict(_,_) | gb_trees:tree(_,_) | map() (with opaque subterms)
    as 3rd argument

Had I otherwise defined my spec as:

    -spec lookup(K,F,C) -> V when
                  K :: atom(),
                  C :: collection(K, V),
                  F :: fun((K, C) -> V).

Which adds a constraint that keys must be atoms, Then dialyzer would
have caught my error:

    mod.erl:17: The call mod:lookup("bad ignored type",fun((_,_) ->
    any()),C::#{'a'=>1, 'b'=>2, 'c'=>3}) breaks the contract (K,F,C) ->
    V when K :: atom(), C :: collection(K,V), F ::
    fun((K,collection(K,V)) -> V)

If you're using rebar3, you should also be getting colored rebar3
output, which does make the error a lot easier to see by putting the bad
value in red and the piece of contract it breaks in green*:
http://i.imgur.com/AjNgVCB.png

Regards,
Fred.

* we should find a way to somehow parametrize the colors to help
* colorblind users I guess.
_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions
Reply | Threaded
Open this post in threaded view
|

Re: Type def and spec syntax

Jesper Louis Andersen-2
In reply to this post by Robert Virding


-spec foo(Y) -> integer() when atom(Y).
-spec foo(Y) -> integer() when atom(Y :: integer()).


Hi Robert,

Putting this in the limestone spotlight, we can muse over why this can happen:

A language consists of 3 things: A grammar of accepted syntax, a static semantics ("statics"), run on the grammar before execution, and a dynamic  semantics which tells how the program executes ("dynamics"). Almost *every* language has all three. The reason is that the grammar often accepts more input than what are valid programs. One example would be in common lisp, where

(defun x)

is a valid s-expression, but it isn't a valid program. In fact, SBCL rejects this program. One could argue it is within the valid syntax of a Lisp (S-exp) but isn't valid according to the statics. Another, better, example is the following Erlang module:

-module(z).
-export([t/1, u/1]).
t(X) ->
    t(X, a).

u(X) -> X + Y.

which is valid from a parsing perspective, but isn't a valid erlang program due to an arity mismatch on t/2 which is undefined. And u/1 uses the unbound variable Y. What erlang uses is a linting step as part of its statics to rule out such a module as valid. It is very nice to allow for being lax in the notation of the grammar and then tighten up the valid programs later on. In fact, type checking/inference is often part of the statics in order to constrain the valid programs and simplify the later compiler parts. Most notably the dynamic semantics of the program.

The key part is that Erlang *does* have a type checker, but it is rather weak since it is really the linting step + more correctness steps inside the compiler. It verifies structurality of your expressions, but it doesn't verify that the types you pass around are valid. You cannot avoid it if you have any kind of way to exit the compiler with some kind of structural error, like an undefined variable. The alternative is to postpone these kinds of errors until the dynamics at runtime, but only very insane programming languages do this. One such example is Guido in which you can write:

def foo():
    return y

which is accepted as a program, but once you run it, it fails spectacularly[0]:

Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
  File "<stdin>", line 2, in foo
NameError: name 'y' is not defined

The TL;DR is that you can't judge the valid programs by the grammar and syntax alone. You have to know the statics of a program as well to be able to define what constitutes a valid program.

And what does this have to do with types? Well, types are just languages with grammar rules as well. So it is likely that you have grammar-valid syntax which isn't a valid type because there is a statics which encode what the valid types are. This is often called a kind-system, and it encodes certain rules for what to check to rule out the invalid programs at the type level.

If you think about it, this is also why BNF is a lousy way to document what are the valid programs. What you really need are operational semantics so you can properly encode what the valid programs are. Preferably in machine verifiable form (Agda, Coq, Twelf, ...)

[0] To be very polite: HOW THE HELL DO PEOPLE PROGRAM LARGE SOFTWARE SYSTEMS WITH THIS????

_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions
Reply | Threaded
Open this post in threaded view
|

Re: Type def and spec syntax

Robert Virding
In reply to this post by Fred Hebert-2
I have done some more checking and the problem still remains. These following type specifications are all legal in the sense that compiler does not complain about them or it gives a strange error:

-spec f5(_) -> integer() when atom(integer()).
-spec f6(Y) -> integer() when atom(Y :: integer()).

The first is passed by the compiler without any warnings or errors while the second you get the error "type variable 'Y' is only used once (is unbound)". So if the first is legal then what does it mean? And why is the second illegal because Y occurs more than once?

Does this mean I should strictly only accept exactly what is in the manual and not what lint accepts?

Robert


On 3 October 2016 at 19:16, Fred Hebert <[hidden email]> wrote:
On 10/03, Robert Virding wrote:
And it if can be used in a
meaningful way why isn't it documented? I think that having syntax which
can never legal is a great way to complicate things. Which we don't need.

The three samples for syntax were:

-type atom(X) :: list(X).
-spec foo(Y) -> integer() when atom(Y).
-spec foo(Y) -> integer() when atom(Y :: integer()).

So here's a valid way to use them that is useful, at the very least in some cases:

   -module(mod).
   -export([main/0]).
      -type collection(K, V) :: #{K => V}
                           | dict:dict(K, V)
                           | gb_trees:tree(K, V).
      -spec lookup(K,F,C) -> V when
                 C :: collection(K, V),
                 F :: fun((K, C) -> V).
   lookup(K, F, C) -> F(K, C).
      main() ->
       C = maps:from_list([{a,1},{b,2},{c,3}]),
       lookup(b, fun maps:get/2, C),
       lookup("bad ignored type", fun maps:get/2, C),
       lookup(b, C, fun maps:get/2).

This module defines an accessor function using the parametrized types and 'when' parts of typespecs syntax. Sadly the analysis is currently not good enough to figure out that "bad ignored type" is not an acceptable value of `K' for the lookup (it appears dialyzer does not do the parametrized inference this deep), but in the third call, it can definitely infer that I swapped the collection and the accessor function:

   mod.erl:13: Function main/0 has no local return
   mod.erl:17: The call mod:lookup('b',C::#{'a'=>1, 'b'=>2,    'c'=>3},fun((_,_) -> any())) does not have a term of type    dict:dict(_,_) | gb_trees:tree(_,_) | map() (with opaque subterms)    as 3rd argument

Had I otherwise defined my spec as:

   -spec lookup(K,F,C) -> V when
                 K :: atom(),
                 C :: collection(K, V),
                 F :: fun((K, C) -> V).

Which adds a constraint that keys must be atoms, Then dialyzer would have caught my error:

   mod.erl:17: The call mod:lookup("bad ignored type",fun((_,_) ->    any()),C::#{'a'=>1, 'b'=>2, 'c'=>3}) breaks the contract (K,F,C) ->    V when K :: atom(), C :: collection(K,V), F ::    fun((K,collection(K,V)) -> V)

If you're using rebar3, you should also be getting colored rebar3 output, which does make the error a lot easier to see by putting the bad value in red and the piece of contract it breaks in green*: http://i.imgur.com/AjNgVCB.png

Regards,
Fred.

* we should find a way to somehow parametrize the colors to help * colorblind users I guess.


_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions