Enhanced type guard syntax]

[Thomas Arts]

In the discussion on the type guard syntax I am missing
the vision of what the type language should look like.
Sure, we have the basic types and it all looks nice for
integers and atoms.... but before you introduce a new
syntax for something that is already exist, why not give it
a thought what you want to achieve with it?

A new notiation does not give you new possibilities in
type checking! In particular one should consider whether
one would allow guards with user defined types or guards
with argumented types, polymorphic types, etc.

For example:

is  f(X) when list(integer(X)) ->
a good notation to express that X should be a list of integers?

would that translate into f(X/list(integer)) ?

is f(X,Y) when dictionary(K,V)(X), K(Y) ->
a good notation for a dictionary of key value pairs with
polymorphic type K for keys and V for values and a binding
of the key type for the second argument of the funtion?
would that be
  f(X/dictionary(K,V), Y/K) ?

is f(X/list/list) a notation for list of list or should it be
    f(X/list(list)), in which case the type notation for list is both
   a constant and a unary function.

is it possible to catch in a type notation:
   f(X) when 10<X, X<20 ->
by f(X/[10..20]) ?

My advice is to first discuss a suitable type language, see if that
is realizable without performance penalties and then propose a 
syntactic sugar notation for it.

One more remark, in the typed lambda calculus they use a type
definition along with the variable in the same style as proposed,
but they use : instead of /. I would really be in favour to use that much
more standard notation, thus f(X:list(A), Y:A) ->  ...
One can use the same notation to give types to functions, as type
annotations that can be checked by a compiler (without confusing
it with devision) It will, though, be confused with module application.
An alternative therefor is ::
Semantically the : is "is element of" and a small epsilon could be used
instead. However, we want to keep the ascii character set as convention,
I guess.

sort([]:list(A)) ->
   []:list(A);
sort([X|Xs]:list(A)) ->
   ([ Y:A || Y<-Xs, Y<X] ++ [X]  ++ 
    [ Y:A || Y<-Xs, X=<Y]):list(A).

these annotations help the type checker, if available and can be left out
in compiling for production code.

/Thomas

---
Dr Thomas Arts 
     Program Manager 
     Software Engineering and Management 
IT-university in Gothenburg 
Box 8718, 402 75 Gothenburg, Sweden 
http://www.ituniv.se/

Tel +46 31 772 6031 
Fax +46 31 772 4899