[MLton-devel] IntInf primops
Stephen Weeks
MLton@mlton.org
Wed, 22 Jan 2003 14:43:54 -0800
> 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