[eeps] comments on eep8

[Joe Armstrong]

Hello,

I'm not sure where to discuss eeps - so I've posted to the eeps
mailing list :-).

For some reason, I seem to have missed eeps, so I missed the original posting on
eep8.

Comments:

1) Do I understand rightly that atoms have to be quoted in type declarations?

2) The eep would benefit from a large number of examples of types in the
   concrete syntax.

3) The declarations are rather verbose

   why -spec(id/1 :: (X) -> X).

   why not

    -spec id(X) -> X.

4) I don't like the leading "-" character

   I'd like

   @spec id(X) -> X.

   "-" is reserved for annotations and I think types are so important
they deserve
   their own special syntax

   (I use the above notation my book, so I'm biased)

5) Why -type(orddict(Key, Val) :: [{Key,Val}]).

   This is again too verbose

   how about

   @type orddict(Key, Val) = [{Key,Val}]

6) Exception types are missing

   @type foo(X, Y) -> Z raises exit(Type)

   In the case where the explicitly terminates with a exit, throw or error I'd
   like to *explicitly* document this

7) I don't like the word "contract" - in some papers I've used the
word contract for
   describing protocols.

   What's wrong with spec (specification) or "type signature"

8) Unclear what the concrete syntax is - I assume the syntax
   "[" Type "]" means list(Type) - but it does not say.

9) I'd like to see a proposal for both the concrete AND the abstract
(parsed) syntax for types - AND for some information about where they
are stored.

  In an earlier mail

  http://mail.google.com/mail/#search/types/11642c19e14b0b3b

  I proposed something like this:

    The type declaration

      @spec fac(Int) -> Int

      In the module M

      would generate the following pseudo function, to be compiled
into the module

      type_spec(fac, 1) ->
         {[int], int, nil}.

     and type_specs() ->  [...{fac,1},...]

     (Rather like module_info which is automatically generated)


10) In the spirit of 9) I'd like to have user defined type checking


    @spec xxx(foo:bar) -> baz:oop

    This means that the arg 1 of xxx is of type X if foo:bar(X)
evaluates to true.

    The point of this is to move towards describing the properties of a system
which can only be checked at run-time and not compile time.

    Then we could have types like fileMustExist() meaning the file
must exist at run
time.

    Today a file is just a string (type wise) but we might like to document
  the fact that this string represents a file that *must* exist.


11) I don't like all these :: things - Often I'd like to group types and use
    uppercase letters for types


    foo(File) -> [File];
    bar(File, Opt) -> Mod where File = string(), Opt = Bool

13) I'd like to *standardise* the internal forms of types - I sent out
a mail with a proposal for this earlier.

This mail and the followup threads have the proposal in more detail -
you might like to re-read them.

14) I'd like to get away from the type() syntax and used variable instead.

   Example - many function manipulate files, I'd like to say

   @spec open(File) -> ...
   @spec ls(Dir) -> [File]

   @type Dir = File = string()

   Any variable not defined X, Y ... ect. is a type variable

   And NOT

   -spec(open/1 :: file() -> ...).
   ... and so on ...

15) I'd like range types Min..Max

16) Limitations of recursive types

Why not use a 'where' statement

    @spec a(X) -> Y; b(P,Q) -> R
        where
            X = A,
            B = P

   ... like letrec


I have appended the module I wrote for type checking since it has
examples of everything I have been talking about.



/Joe


-module(lib_type_check).

%% dynamic type checker
%% To make a type checker you need a callback module that
%% exports the function type(Name)
%% To test a type do the following
%%  lib_type_check:type_check(Type, Val).
%%
%% exports
%%   type_check(AbsType, Value)
%%   Abs type is a parse tree represeting a type
%%
%%  Type  = int | bin | str | bool | float | iolist | pid | ref
%%          | list | tuple | any | {range, Min, Max} | {constant, C} |
%%          | {list, Type} | {tuple, [Type]} | {record, Name} |
%%          | afun | {type, Mod, Name}
%%
%%  Most of these types are self-evident. The interesting type
%%  is {type, Mod, Name}
%%  This means that Mod *must* export a function
%%  module_type(Name::atom) -> Type
%%  type_check(Type, Val) -> Bool

-export([type_check/2]).

%% these are for testing
-export([test/0, module_type/1]).

-record(test_record,{name}).

test() ->
    true  = tc(int, 1234),
    false = tc(int, abcd),
    true  = tc({constant, 1234}, 1234),
    false = tc({constant, 1234}, 12343),
    true  = tc({constant, true}, true),
    true  = tc(bin, <<"123">>),
    true  = tc({list, int}, [1,2,3,4]),
    false = tc({list, int}, [1,2,abc,4]),
    true  = tc({tuple, [int,{constant,123},{constant,abc}]},
	       {123456,123,abc}),
    true  = tc({type, ?MODULE, b}, <<"123">>),
    false = tc({type, ?MODULE, b}, 123),
    {'EXIT', _} = (catch tc({type, ?MODULE, undef}, 123)),
    true  = tc(bool, true),
    true  = tc(bool, false),
    false = tc(bool, fals1e),
    true  = tc({type, ?MODULE, mixed}, [12,abc,3,f,45]),
    false = tc({type, ?MODULE, mixed}, [12,abc,3.14159,f,45]),
    true  = tc({type, ?MODULE, myiolist}, [<<"1bc">>,34,[<<12>>,34,56]]),
    true  = tc(iolist, [<<"1bc">>,34,[<<12>>,34,56]]),
    false = tc({type, ?MODULE, myiolist}, [<<"1bc">>,34,[<<12>>,abc,34,56]]),
    false = tc(iolist, [<<"1bc">>,34,[<<12>>,abc,34,56]]),
    true  = tc(str, "1263163"),
    false = tc(str, [1,2,3,4,abc]),
    true  = tc(afun, fun(X) -> 1 + X end),
    true  = tc({record,test_record},#test_record{}),
    true  = tc(pid, spawn(fun() -> hello end)),
    true  = tc(ref, make_ref()),
    true  = tc(float, 3.141259),
    true  = tc(any, glurk),
    horray.

tc(Type, Val) ->
    io:format("Checking ~p ~p~n",[Type, Val]),
    type_check(Type, Val).

module_type(b) ->
    bin;
module_type(mixed) ->
    {list, {type, ?MODULE, aori}};
module_type(aori) ->
    {alt, int,atom};
module_type(myiolist) ->
    {alt,
     bin,
     {alt,
      byte,
      {list, {type,  ?MODULE, myiolist}}}};
module_type(byte) ->
    {range, 0, 255}.

type_check(Type, Val) ->
    %% io:format("tc check ~p isa ~p~n",[Val, Type]),
    tc(Type, Val, 0).

tc(_, _, N) when N > 1000 ->
    %% note we only increment N when we enter a "deep" type
    %% we don't increment the level as we traverse a list
    %% so I've set a fairly low limit here
    %% io:format("** type test of ~p undecided",[Type]),
    true;
tc(atom, X, _)  when is_atom(X) -> true;
tc(int, X,  _)  when is_integer(X) -> true;
tc(float, X, _) when is_float(X) -> true;
tc(bin, X, _)   when is_binary(X) -> true;
tc(list, X, _)  when is_list(X) -> true;
tc(pid, X, _)   when is_pid(X) -> true;
tc(ref, X, _)   when is_reference(X) -> true;
tc(afun, X, _)  when is_function(X) -> true;
tc({record,Name}, X, _) when element(1, X) =:= Name -> true;
tc(tuple, X, _) when is_tuple(X) -> true;
tc(byte, X, _)  when is_integer(X), 0 =< X, X =< 255 -> true;
tc({range,A,B}, X, _) when A =< X, X =< B -> true;
tc(str, X, _)      -> tc_str(X);
tc(bool, true,  _) -> true;
tc(bool, false, _) -> true;
tc(any, _, _)      -> true;
tc({constant, A}, A, _) -> true;
tc({type, Mod, Name}, X, N) ->
    tc(Mod:module_type(Name), X, N+1);
tc({typeConstrain, Mod, Name}, X, N) ->
    Mod:module_type(Name, X);
tc({alt, A, B}, X, N) ->
    tc(A, X, N+1) orelse tc(B, X, N+1);
tc({list, Type}, L, N) when is_list(L) ->
    tc_list(L, Type, N+1);
tc({tuple, Ts}, Tup, N) when is_tuple(Tup), size(Tup) == length(Ts) ->
    tc_tuple(Ts, Tup, 1, N+1);
tc(iolist, X, N) ->
    tc_io_list(X, N+1);
tc(_X, _Y, _) ->
    %% io:format("is ~p a ~p~n",[_X,_Y]),
    false.

tc_io_list(X, N) ->
    tc(byte, X, N) orelse tc(bin, X, N) orelse tc({list,iolist}, X, N+1).


tc_list([H|T], Type, N) ->
    case tc(Type, H, N) of
	true -> tc_list(T, Type, N);
	false -> false
    end;
tc_list([], _, _) ->
    true.

tc_str([H|T]) when 0 =< H, H =< 255 -> tc_str(T);
tc_str([]) -> true;
tc_str(_) -> false.

tc_tuple([H|T], Tuple, Index, N) ->
    tc(H, element(Index, Tuple), N)
	andalso tc_tuple(T, Tuple, Index+1, N);
tc_tuple([], _, _, _) ->
    true.