Enhanced type guard syntax

[Chris Pressey]

On Fri, 19 Sep 2003 12:35:24 +0100
Peter-Henry Mander <erlang@REDACTED> wrote:

> [...]
> So (including aspects in an email to Vlad) this has an impact on:-
> 
> 1) code correctness and checking during compilation, without added 
> "binary-baggage" at runtime,
> 
> 2) trapping exceptions at runtime, which is what tagging was meant to 
> achieve, albeit clumsily, I concede.
> 
> 3) optimisation (maybe?).

Congratulations.  What started out as a proposal for a frivolous but
otherwise seemingly harmless piece of syntactic sugar, has blossomed
into yet another a monstrously murky discussion on typing.

(See Pete?  You aren't the only one who can be flippant :)

I think we are all missing something simple and obvious here, and
getting hung up in relatively meaningless details.

Here is my thought - Erlang doesn't need another type _checker_.  Type
checkers do not appeal to the laziness of Erlang programmers, who don't
want to spell out stuff they already know!  What Erlang needs is a type
_inferencer_.  (And if the inferencer can figure out other properties
such as side-effectfulness, which shouldn't be too much extra
difficultly, then all the better.)

Note that I'm not suggesting that Erlang should "have [only] inferred
types."  I don't think such a concept makes much sense in Erlang.  If
you want to tell Erlang that X should be some type y, you should be able
to tell it that (and a guard test is one way to do that.)

But I think that a lot of the time, you actually don't need to do that. 
This is mostly an educated guess, but it seems like ~70% or more of the
type consistency that _counts_ could be inferred by a pre-compile pass.

This information could then be used to generate errors (at compile time
*and* run time) and optimizations and documentation... and pretty
kaliedoscope patterns for your screen-saver, if you like.

Simple examples are easy to come by.  If you have a function like

  hyp(A, B) -> math:sqrt(A * A + B * B).

and you know the type signatures of *, +, and math:sqrt/1, you can
pretty much instantly derive the type signature of hyp/2
(FLOAT x FLOAT -> FLOAT).  Basically, you start with the assumption that
every variable can be of any type, and you pare it down by looking at
how it is used.  The sets module would be handy for this, because it's
all about sets of types.

While you are doing this, you can also learn other things about
functions - for example, a function is side-effectless only if all the
functions and operators it calls are also side-effectless - so you can
put this information in its signature, too.  Constant-time is trickier,
but I _think_ possibly still possible.  (At least, I hope so.)

Now, guards (however they're notated) suddenly play a more important
role in things - they tell the type inferencer what is and is not
allowed.  So when you write

  foo(A) -> A.

all the type inferencer can come up with for the signature of foo/1 is
ANY -> ANY (where ANY is the set of all types.)  But if you add a guard
to foo/1 like so:

  foo(A) when is_integer(A) -> A.

suddenly the type inferencer knows foo/1 is INTEGER -> INTEGER.  And in
some other place in the file, if you call foo(bar), it will complain, at
compile time, that the sets ATOM and INTEGER are disjunct, you silly,
fallible human, you.

This could also open the door for user-defined guards - because it can
check that guard expressions are indeed side-effectless and
constant-time, and disallow them (or refactor them) if they aren't.

My 2 Zorkmids for this morning,

-Chris