[MLton-devel] IntInf primops

[Stephen Weeks]

> It is definitely a shame to not do IntInf constant folding. 

Agreed.  It is on the todo.

> Note, I don't see how doing constant folding can effect safe-for-space.
> Doesn't it result in a constant amount of space?

Yes.

> I agree that it could be painful (exponential in program size) but it would
> still be asfe for space.

It all depends on how you write your quantifiers in the definition of
safe-for-space.

Let I(p,i) be the maximum memory used by program p running on input i
in some ideal sematics.

Let M(p,i) be the maximum amount of memory used by program p compiled
by MLton and running on input i.

Here are two different definitions of "M is safe-for-space wrt I".

* Exists c. Forall p. Forall i. M(p,i) <= c * I(p,i)
** Forall p. Exists c. Forall i. M(p,i) <= c * I(p,i)

(**) clearly allows more M's to be safe-for-space then (*), since you
can chose the constant based on the program.  I agree that in the
sense of (**) that IntInf constant folding at compile time is
safe-for-space.  It is not in the sense of (*).

When we last talked about this (over three years ago!) we concluded
that the notion that Appel uses in Compiling with Continuations is
equivalent to (**).  Actually, as best as I can tell, he uses

*** Exists f:int -> int. Forall p. Forall i. M(p,i) <= f(|p|) * I(p,i)

Clearly, if M is ***-safe-for-space, then M is **-safe-for-space, just
choose c = f(|p|).  The converse is true as well, since there are only
a finite number of programs of size n, so we can choose 

	f(n) = max { min { c | Forall i. M(p,i) <= c * I(p,i) } | |p| = n }

Anyways, at the time, we decided that we liked (**).  However, I am
now unhappy with that decision, because of the potential exponential
compile-time with IntInf.  I am especially worried about IntInt.<<.
In fact, it occurs to me that ** allows one to hold on to
constant-sized arrays, like Array.array (1000000, 13).  Clearly this is
a bad idea.

So, I would like to propose that we follow a new definition of
safe-for-space that falls between (*) and (**)

**** Exists c. Forall p. Forall i. M(p,i) <= c * |p| * I(p,i)

That is, you're allowed to hold on to stuff linear in the size of the
program, but no more.  I think that rules out the problems.

Regardless of the theory, once we do get IntInf constant folding
working again, I think we should restrict folding of IntInf.{<<, *} to
inputs smaller than some program-independent constant.


-------------------------------------------------------
This SF.net email is sponsored by: Scholarships for Techies!
Can't afford IT training? All 2003 ictp students receive scholarships.
Get hands-on training in Microsoft, Cisco, Sun, Linux/UNIX, and more.
www.ictp.com/training/sourceforge.asp
_______________________________________________
MLton-devel mailing list
MLton-devel@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/mlton-devel