Regards,
--
Nils Goesche
"Don't ask for whom the <CTRL-G> tolls."

Matthias>    1. First argument:

Matthias>       - must be a number obtained from a previous call to open/dup/...
Matthias>       - must not have been subjected to "close" in the meantime
Matthias>       - must have been opened for reading

It may be that there are things I do not know about the ML system, or
how an ML OS would work file objects, but as I know file objects from
UNIX (be it represented by a small integer or something else), such an
object has state; so how would it be verifiable at compile time that a
particular call to `read' would not be operating on an object that has
been closed?

Is the ML compiler smart enough to know that in regions following the
close operation, the object has another type and would that work in a
multiprocess setting?

Or did it just misinterpret the extent of your claims (in which case I
must state for the record that it was with no malicious intent :-)

- use of the many code-construction mechanisms that Lisp allows (macros etc)

- easy sharing of the constants needed by the compiler to implement primitives
(assuming your Lisp compiler is written in Lisp :-)

- the ability to develop and test code on-the-fly (sure, if you screw up badly
then you are lost, but many cases this doesn't happen).

I want to store in a variable x a 32-bit quantity that has the exact same
representation as an 'unsigned int' in C but for which I have a
compile-time guarantee that it will never be an odd number.  What I want
to be able to do on these numbers are the "usual" four arithmetic
operations (with division rounding down to the next even number), and
perhaps some comparisons.  And a conversion from/to "unsigned int"
(again, with rounding down to the next even).  In SML I write:

structure Even :> sig

   type even

   val + : even * even -> even
   val - : even * even -> even
   val * : even * even -> even
   val / : even * even -> even
   val compare : even * even -> order
   val fromWord: Word32.word -> even
   val toWord: even -> Word32.word

end = struct

   fun roundeven (x: Word32.word) =
       Word32.andb (x, 0wxfffffffe)

   type even = Word32.word
   val op + = Word32.+
   val op - = Word32.-
   val op * = Word32.*
   fun x / y = roundeven (Word32./ (x, y))
   val compare = Word32.compare
   fun toWord x = x
   val fromWord = roundeven

end

Now, whenever I see a value of type "even", I can be absolutely certain
that it will be an even number -- but the point is that all the
operations (except /) are *precisely* as efficient as the ones on Word32.

How do you do this in Common Lisp?

I don't want a guarantee that works 99.9% of the time because that's not
good enough for this particular application.  What I want is something
that works always, but I want to eliminate the usual runtime penalty for it.

As I have already said in a reply to another such question, I would
probably not have a "close" operation at all -- for pretty much the same
reason that we don't need "free" in Lisp or ML.

And again, not all runtime checks can be eliminated this way -- in
particular not those that are testing for inherently dynamic properties.

And there are static typing mechanisms that would allow one to express the
effect that "close" has (linear types, unique types, monads).

  I assume that if this technique is used at all, it is used all the time,
  it is not suddenly used in a system that did not do this previously, but
  your argument looks like you think someone would suddenly start to do
  some allocation in the garbage collector of a Common Lisp system that had
  never done this before.  I find this a rather peculiar inability to see
  the simplest possible ramification of a suggestion: that it be used all
  the time.  So, at least some of the garbage in from-space is the direct
  result of its collection phase of what is now to-space, right?  In other
  words, there is at least as much space as you allocated last time you
  collected.

  Also, what happens in a system that does not allocate during collection?
  Do they crash and burn if they they have to grow their new-space because
  it did not release enough space on the last allocation?  No?  If not,
  survival tactics of a similar kind _might_ be re-usable in a collector
  that does allocation, don't you think?

  In other words, your fake "problem" does not exist.  If it should spring
  up nonetheless, the solution is the same as for a system that does not
  allocate during collection.  Worst case, we start garbage collection some
  time prior to actually hitting the roof of the available space.  Yet none
  of these very trivial solutions came to mind between starting to write
  your article and deciding to post it after it was written.  How come?

| Also, the subset of Lisp available will be constrained to things that can
| run safely at any allocation point.  E.g. you can't use anything that
| alloctates while holding a lock (I'm assuming the is keeping some data
| structure consistent).

  This makes even less sense than your previous, non-existing problem.
  What other parts of the system inhibits allocation while being locked?
  Please remember that garbage collection happens at a time when the memory
  allocation subsystem has the control of the system, so if you had a lock
  and you never allocated anything before releasing it, you would never
  trigger a garbage collection in the first place.

  Do not waste my time by trying to make me think for you.  Think and post
  in that order. please.

Regards,
--
Nils Goesche
"Don't ask for whom the <CTRL-G> tolls."

Instead of using the normal Lisp accessor function like car and aref,
open-coded equivalents of the same were used everywhere to avoid type
checking and other surprises.  Perhaps we could have achieved the same
by using (optimize inline) and other declarations.  But we didn't.

The semantics of the accessors was further muddied by forwarding
pointers, which were stashed in odd spots.  Even simple things
like car require a check for a forwarding pointer, or not, depending
on the context.  I could imagine that this requirement would break
pieces of the full language, for example conditions and handler-bind
if the handlers are stored in a list.

I wouldn't say that a GC can't cons in the course of doing a
collection, just that it's desirable not to.  It may be awkward to
reclaim the GC's own storage as garbage immediately, especially if in
a two-space collector the storage is simply allocated in to-space.

You can put in arbitrary effort to making the full language available
for use in the GC.  On the other hand, in a Common Lisp implementation
there are a lot of things you into which you can put arbitrary effort :)

Anyway, for the last time, I am not saying that every dynamic check can
be eliminated.  But many can, and those I would like to...

I don't think that there is a need for yet another OS that would only add
compile-time type-safety to its mostly static and autistic
program-components.

What I would want to see in new OS developments are things like moving the
general OS behaviour from patiens to agens. I want the OS to actively
observate the user(s) and try to actively act in a way that helps him/them
to reach his/their goals. I cannot imagine developing such a thing in a
language that is any less dynamic than lisp.

I sometimes wish that the programming environments in our so called "modern
operating systems" would not distinguish so strongly between user
interaction (shells, scripting) and "real" program development. A language
like Lisp would enable a smooth transition from using it as a shell or for
little scripting tasks up to writing whole applications. Communication
between programs would be trivial and scripting would come for free.

ciao,
Jochen

My concern is that many people blur the line between levels of safety (note
the earlier posters confusion between "statically type-checked" and
"provably correct") and that many static typing afficianados like to take
advantage of this blurring to make assertions that languages that do not
provide these checks are somehow deficient rather than having simply
selected a different point on the single axis labeled "type-safe", perhaps
to gain ground on other valuation axes.

Don't provide 'open' and 'close' operations.

Instead, provide (in Haskell syntax, my ML is rusty):

        type ReadableFile = ... opaque
        type WritableFile = ... opaque

        withInputFile  :: (ReadableFile -> IO ()) -> FilePath -> IO ()
        withOutputFile :: (WritableFile -> IO ()) -> FilePath -> IO ()

        readChar :: ReadableFile -> IO (Maybe Char)
        ... etc.

'withInputFile proc filename' opens the file for reading,
calls 'proc <filehandle>', closes the file, and returns ().
(I'm ignoring error conditions for the moment).

There's no way to get a ReadableFile except by passing
a callback procedure to withInputFile, and since this returns ()
the file handle can't "escape" after it's been closed.

(Well, you could use call/cc, mutable variables, or some
other trick to sneak an open file handle out of its dynamic
extent, but I think the above should be safe in a pure HM
type system).

See, open coding such functions is exactly what I want to avoid.  The
question is "implement GC in lisp", not "implement GC in some
pseudo-Lisp with all the guts marked off-limits".

(deftype even (num-type &optional size)
  `(and ,(if size
             (list num-type size)
             num-type)
        (satisfies evenp)))

(defun blark (x)
  (declare (type (even unsigned-byte 32) x))
  (+ x 42))

and whether that will be slower or faster than if you left out the
declaration depends only on compilation settings.  Sure, you'll say
that I won't have any guarantee that x will in fact be an even
number.  Well, that's right:  There is no guarantee that you
won't have any runtime type errors in CL.  That's the point:
I think it doesn't matter :-)  I don't have any guarantee that
I won't try to use too large array indices, either, for instance.

This reminds me of what some people percieve as contradicting goals
of physicists and mathematicians:  The physicists want to get the
job done.  If they can't prove some formula they need rigorously
they'll use it anyway.  They have no time to do otherwise.
Some of them don't like mathematicians because they think that
mathematicians were always trying to force them to prove everything
rigorously or whatever, but strangely I have never met a
mathematician who actually did that.  In the same way, I want
to get the program done.  Fast.  I can't spend days and days
to find workarounds for some obscure restrictions on types
of elements of modules or something that are only there to ensure
the soundness of your carefully designed type system when I know
that what I am trying to do will work anyway in that case.
And I want to be able to quickly redesign and change arbitrarily large
parts of my software, and your type system will certainly get
in the way again.

You'll disagree, of course.  Let's leave it at that.  There is
no way you or I can /prove/ that our respective views on
practical programming is correct.  Only practice can show -- people
have to try out for themselves :-)

Regards,
--
Nils Goesche
Ask not for whom the <CONTROL-G> tolls.

So the efficiency argument is really a red-herring.  A couple of more
interesting arguments are that the OS design might be simplified and
that errors might happen at a more convenient time.  The former I
don't know about (to make such a system work would require such
radical changes that it's hard to reason about simplicity), the latter
is also fairly bogus because you still need to handle things like the
disk filling up, ECC errors from main memory and so on - no amount of
theorem proving will make these go away or mean that well-written
applications (databases say) need to try and cope.