Pure and Total
============
to support a bit better classification, I'm looking at two new function
attributes:
pure total fun f( .. ) ..
and maybe "impure" and "partial" as well.
"A pure function is one which depends only on its parameters"
"A total function is one which has no preconditions".
These specifications would be perfect in a world without pointers.
Felix already detects when a function is pure.
An impure function is typically one that refers to a variable.
Typically this is an accessor function. For example:
fun f() {
var x = 1;
fun sq() => x * x; // accessor, impure
}
In affect, such a function "would be" pure if the variable were passed
in as an argument. However some functions depend on external
state, for example getenv() depends on the environment,
and setenv() were it available might change the result.
But the environment isn't a variable.
To some extent an even more refined description would be
pure except-for v fun f ....
That may be overkill :)
The idea here is that you can actually assert purity or totality: if you're
wrong the compiler may complain. It may also trust your annotation if
it can't figure it out by itself. This is *always* the case for bindings,
since they're abstract.
A function which is marked total may have a pre-condition.
There are two takes on this: basically total means all arguments
are mapped to a value. However we expression:
div: Z * - {0} -> Z
which is a total function, as:
div(x:int, y:int where y !=0) => ...
Interestingly, this notation doesn't work for C bindings. Syntax! Grr.
Anyhow, there are two interpretations of pre-conditions.
One is that it represents a restriction of the domain, i.e. the actual
domain type is a subset of the declared one.
The other interpretation is that the function has an invariant:
precondition => postcondition
This does NOT mean you can't call the function with an argument not
satisfying the pre-condition, it simply means that if you do, there's
no assurance the postcondition will be met.
Felix adopts the first convention because the second is easily coded
by just making the above line the postcondition.
With that convention, saying a function is total, when it has a pre-condition,
simply asserts that the pre-condition is complete.
The reason for the annotation is that if you just write:
fun f(x:int)=>x;
Felix can deduce that f is pure and total. But it isn't evident to the user
without thinking, and also it's an implementation detail, not part of
the specification.
Possible synonym
==============
Pure and total could be adjectives as shown:
pure total inline fun f ...
But we could also just have
pure f ....
and we could have
.. is pure
.. is total
has property "pure"
etc etc.
We could also try this:
var fun f ... // impure
val fun f ... // pure
For total we could also do:
fun f(x:int where true)
which could be taken to mean there is no pre-condition. As noted this is
potentially different to not stating a pre-condition .. which simply
means we didn't bother to state it (not that there isn't one!)
Pointers and Abstraction
===================
A function which depends entirely on its parameters need not be pure.
If the parameter is explicitly a pointer, it can depend on what the
pointer points at, which, in Felix, is almost always mutable.
Even a non-pointer parameter can be a pointer if the type
is hidden by abstraction (either Felix abstraction, or, C binding).
Even more complex, a value such as a struct can *contain* a pointer.
In light of these considerations the "pure" specifier takes on extra
meaning in providing the compiler a way to learn something it couldn't
(or couldn't easily) do without the annotation.
This applies to total functions too: in particular totality asserts that
the function can't throw an exception (something Felix compiler can't
learn about because Felix doesn't have any exceptions :)
Generators
=========
The "gen" construction in Felix is too general. Some generators
modify external variables. Some modify their environment, such
as "rand". Some only modify their internal environment and return
with a continuation left behind that can be continued, using
the yield mechanism.
A function which simply modifies a variable is really an ordinary
procedure, dressed up to return a value instead of setting
a variable via a pointer.
A yielding generator, on the other hand, is typically also a procedures,
but not an ordinary one: in some ways it's actually a function
that returns a stream of values. Such a function could be pure.
For example a function that returns the integers 0 1 2 3 4 5 ...
is a pure function when considered to be returning an infinite
(lazily evaluated) list. Indeed in Haskell functions exist that do
precisely that, and in Haskell all functions are pure.
It is tempting to make a special construction for streams.
After all, we actually have one, namely yield. And we have
machinery in the grammar for iterators.
In general, streams are just a special case of co-inductive
data types, i.e. ones defined by how you take them apart,
rather than how you build them. Laziness and more general
pattern matching would also help here!
Anyhow, it remains to provide better annotation of generators
so the semantics are more amenable to management,
including optimisation and static checking.
--
john skaller
skal...@users.sourceforge.net
http://felix-lang.org
------------------------------------------------------------------------------
This SF email is sponsosred by:
Try Windows Azure free for 90 days Click Here
http://p.sf.net/sfu/sfd2d-msazure
_______________________________________________
Felix-language mailing list
Felix-language@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/felix-language
