wtanksley@bigfoot.com — 2000-05-12 23:28:50

From: iepos@... [mailto:iepos@...]

>By the way, there's one thing I'd like to bring up. While fiddling
>with my interpreter, I've been getting a lot of mysterious
>Segmentation Faults because of accidentally running things like
>"call", "dip", and "if" with integers on the stack instead of programs.

Right...

>Thus, I've been thinking about adding some type-checking. But,
>I've run into a brick wall. I realized that if we have branching,
>it is sometimes impossible to tell at compile-time what the types
>of things on the stack will be.

Not entirely correct. It's possible to require nearly perfect compile-time
type knowledge, although it requires the programmer to take a little more
care in designing his programs.

>I'm just curious to know what you suggest to remedy this. Here are
>some possible policies the system could have, if it tries to
>find out the type of a thing on the stack but can't, yet would
>like to know because it is getting ready to execute, say, a "+" and
>wants to be sure it's two ints on the stack:

> 1) Emit an error message that the programmer is too sneaky.
> 2) Install a runtime check to make sure the types are right
> (this would involve carrying around some type tags).
> 3) Don't do any checks, and just hope we're okay.

>Right now, I'm leaning toward #1. However, I'm pretty this means
>that there will be some cases that the programmer will be absolutely
>sure is program is safe, yet the system rejects it because it is
>not smart enough. My guess is that this could happen regardless
>of how smart the system is.

I'm afraid you're right. Not only is it possible that the system can't ever
be smart enough, but it's also possible that no human could ever be smart
enough. There's no way of knowing.

So we just emit a safe error message. See ML for examples.

We should also make provision for dynamic typing; there's a lot of times
when it's needed. Fortunately, this is very easily handled by, for each
type named "foo", having the system add a type named "foo-dynamic", and
adding a couple for words to do things like add type information to a static
type "dynamic ( foo -- foo-dynamic )", return a type signature "typeof (
foo-dynamic -- type-signature-foo )".

Have I explained the compile-type-stack method of compile time type checking
and polymorphism? It's very nice, and fits in elegantly with Forth.

>- "iepos" (Brent Kerby)

-Billy

srenner@mail.ru — 2000-05-13 01:51:23

Dynamic type checking is not free, but I think that any reasonable Joy
implementation has to include it. You don't want the programmer to
"have to take reasonable care" to avoid a "mysterious segmentation
fault." Forth has often been associated with very low-level (close to
the hardware) programming. I can see the point of a Joy-like language
written in assembler and running on an embedded system. Type checking
might be out of place. At any higher level, it is needed.

Oberon has dynamic type checking which only costs if it is used. Say
that our Joy-like VM is to execute a word (literal, box, whatever). If
the word is "+" or "dup" it must be performed. If the box is "3" it
must be pushed onto the stack. Of course to Joy this is not two kinds
of thing. Both are functions of type stack-->stack. But the VM
certainly has to make a distinction. There are a limited number of
"ops" like +, dup, and i, perhaps including some user-defined ones.
But there are millions of integers. Each op can be associated with a
function in Oberon, but there would be no point in constructing a
function for each integer encountered that pushed the integer onto the
stack. The VM looks like this:

PROCEDURE VM(VAR word, stack: Box); (* the stack is just another box
== chain of boxes*)
VAR top: Box;
BEGIN
REPEAT
IF word IS opBox THEN (* IS: Type test *)
WITH word:opBox DO word.op END; (* WITH: Type guard *)
ELSE
top := word.Clone; (*clone (copy) of word *)
top.next := stack;
stack := top; (*copy of word is on top of the stack*)
END;
word := word.next;
UNTIL word = NIL (*No more boxes to execute *)
END;

Ops get executed, everything else gets pushed. Remember the
multiple-VMs-as-dataflow-threads idea? That model would work best with
a VM object instead of a VM procedure (object == POINTER TO RECORD, so
that the stack can be an instance variable. That way, multiple VMs are
instances with different stacks.) But that complication aside, the
above procedure is actually THE WHOLE THING. To get Joy, one would
write all the ops, including code to handle different types, a scanner
for input files, and other "frills". But the above procedure really is
a complete virtual machine. I think.

About GC: Yes, it is true that this machine shouldn't need an external
garbage collector. The only thing that gets "lost" each time around
the loop is the word that is executed. The reason that a clone is
pushed instead of the original copy is consistency: either branch
gives us one box of garbage, which we could "collect" at that point.
(Unless the box contains an object that is referenced in the enclosing
context, in which case GC would still be needed.) Baker's linear logic
papers show that if you always clone instead of copying pointers and
always throw things away you don't need GC.

Remember that there is no cost associated with GC being present in a
system if the collector is never called. So it isn't a disadvantage
that Oberon provides GC. Like type tests and type guards, GC is paid
for when it is used.

Oberon is a little tricky about PROCEDURE type instances. I am having
difficulty assigning them to variables. Specifically, the compiler
doesn't like this when the procedures are bound to a record type. ( ==
class methods) It's probably an issue with the specific compiler, not
the language specification.

Tornadoes never come near the lake, maybe because there are no
trailers here.

sr

iepos@tunes.org — 2000-05-13 13:26:16

> >Thus, I've been thinking about adding some type-checking. But,
> >I've run into a brick wall. I realized that if we have branching,
> >it is sometimes impossible to tell at compile-time what the types
> >of things on the stack will be.
>
> Not entirely correct. It's possible to require nearly perfect compile-time
> type knowledge, although it requires the programmer to take a little more
> care in designing his programs.

Yes. That was the kind of thing I was thinking of doing... Okay,
here's one rule the system might enforce: the two branches of an
"if" must always have the same type, taking the same type inputs and
giving the same type outputs. The important thing is that after
the "if" is finished, the compiler must know what types are then on
the stack, regardless of which branch was chosen.

Okay, here's another one: when one reaches the end of a loop,
returning back to the beginning, the same type things must be on
the stack as when the loop was originally entered.

I'm not sure if these two rules are enough ...

> I'm afraid you're right. Not only is it possible that the system can't ever
> be smart enough, but it's also possible that no human could ever be smart
> enough. There's no way of knowing.

Right. Here's an example of a program that would be impossible to decide:

foo [0] [[]] if call

Suppose that "foo" is a program that pushes an unknown boolean onto
the stack. If it cannot be determined what it pushes (for instance,
because it relies on user input), then the system has no way of determining
which of the "0" or the "[]" will end up getting on the stack. If it's
a "0", then we're toast, because we're going to try to "call" it.

> So we just emit a safe error message. See ML for examples.

Yeah... ML has a pretty nice type system, I suppose. I've fiddled around
with Objective CAML, but haven't done much with it.

I guess the type rules ML enforces are similar to the ones C enforces ...
Both branches in "if" must have the same types; this is guaranteed by
the fact that "if"s in those languages never have return values, and
only take parameters from the environment. Similarly, loops do not
have return values, and only take parameters from the environment.

> We should also make provision for dynamic typing; there's a lot of times
> when it's needed. Fortunately, this is very easily handled by, for each
> type named "foo", having the system add a type named "foo-dynamic", and
> adding a couple for words to do things like add type information to a static
> type "dynamic ( foo -- foo-dynamic )", return a type signature "typeof (
> foo-dynamic -- type-signature-foo )".

Yes. In particular, this could be useful when writing an interactive
interpreter. However, it seems like you'd want just a single "dynamic"
type, rather than a bunch of them; that way, you could mix up your
new dynamic things through "if"s without the system complaining.

> Have I explained the compile-type-stack method of compile time type checking
> and polymorphism? It's very nice, and fits in elegantly with Forth.

Maybe you have ... I'm not sure ...

> >- "iepos" (Brent Kerby)
>
> -Billy

One other thing relevant to type-checking ... I think it would be useful
if the user could assert what types of things are on the stack.
Maybe something like FORTH stack-comments:

( inputtypes -- outputtypes )

Except that the system would enforce them. But, maybe we'd want to avoid
the same syntax as ordinary comments (with parentheses), since
stack-comments would no longer really be just comments.

Ahh... one other thing... We are going to need more than just a few
primitive types, such as "int", "float", and "boolean". We'll
need whole schemes of types for programs-pushing and program-popping
programs. We might use Joy's convention and say that if

int -- float

is the type of a program that takes a int and yields a float, then

-- [int -- float]

is a program that pushes such a program. We might allow the "--" to
be omitted when there are no inputs, so that we'd say "int" instead
of "-- int". Or, we could use the approach brought up earlier
of not using "--", but instead using "-" (and maybe "+"), using
something like

-int -int +int

for the type of "+", "-", "*", "/", etc.

Oh, and one other thing... what about out-of-bounds exceptions for
arrays? It would be cool if the type system could be made strong
enough so that it could be guaranteed at compile-time that array
fetches and stores were always in-bounds. But, that sounds tricky;
I don't think I'd attempt it yet. But, it's an interesting idea
to keep in mind ...

- "iepos" (Brent Kerby)

wtanksley@bigfoot.com — 2000-05-14 00:58:57

From: iepos@... [mailto:iepos@...]

>> >Thus, I've been thinking about adding some type-checking. But,
>> >I've run into a brick wall. I realized that if we have branching,
>> >it is sometimes impossible to tell at compile-time what the types
>> >of things on the stack will be.

>> Not entirely correct. It's possible to require nearly
>> perfect compile-time
>> type knowledge, although it requires the programmer to take
>> a little more care in designing his programs.

>Yes. That was the kind of thing I was thinking of doing... Okay,
>here's one rule the system might enforce: the two branches of an
>"if" must always have the same type, taking the same type inputs and
>giving the same type outputs. The important thing is that after
>the "if" is finished, the compiler must know what types are then on
>the stack, regardless of which branch was chosen.

That sounds reasonable.

>Okay, here's another one: when one reaches the end of a loop,
>returning back to the beginning, the same type things must be on
>the stack as when the loop was originally entered.

Close enough. Each loop or conditional word can run its own typechecking,
so that the proper constraints can be achieved. For example, some loops
have to be able to loop zero times as well as n times.

>I'm not sure if these two rules are enough ...

A more powerful version of those two typechecks would involves backtracking
until convergence. In other words, you can have an unbalanced 'if' so long
as a later conditional sets things right. I personally don't think that's a
good idea; it encourages long definitions, which is not something we want to
encourage.

>I guess the type rules ML enforces are similar to the ones C
>enforces ...

C doesn't really enforce any real type rules, does it?

>Both branches in "if" must have the same types; this is guaranteed by
>the fact that "if"s in those languages never have return values, and
>only take parameters from the environment. Similarly, loops do not
>have return values, and only take parameters from the environment.

'if's in ML do have return values. Perhaps you're thinking of the wrong
language, because I can't think of a worse comparison than one between ML
and C. ML is strongly typed; C is hardly typed at all (almost everything's
an integer). ML uses an immensely powerful backtracking engine which allows
type inference; C requires everything to be declared, and even with that it
gets things wrong.

>> We should also make provision for dynamic typing; there's a
>> lot of times
>> when it's needed. Fortunately, this is very easily handled
>> by, for each
>> type named "foo", having the system add a type named
>> "foo-dynamic", and
>> adding a couple for words to do things like add type
>> information to a static
>> type "dynamic ( foo -- foo-dynamic )", return a type
>> signature "typeof (
>> foo-dynamic -- type-signature-foo )".

>Yes. In particular, this could be useful when writing an interactive
>interpreter. However, it seems like you'd want just a single "dynamic"
>type, rather than a bunch of them; that way, you could mix up your
>new dynamic things through "if"s without the system complaining.

I forgot to mention that there's a type hierarchy. For example, both
pointers and integers are "cells", and there's a version of SWAP which will
therefore handle them. double integers are double cells, and there's a
version of SWAP to handle double cells, and another version which takes as
input a double and a single, and another one whose input is the other way
around.

An "integer-dynamic" is almost certainly a double-cell type, whereas an
"object-dynamic" is probably a single-cell type (its type info is probably
stored in the object itself). Both are subtypes of "dynamic", just as they
are also subtypes of "integer" or "object".

>> Have I explained the compile-type-stack method of compile
>> time type checking
>> and polymorphism? It's very nice, and fits in elegantly with Forth.

>Maybe you have ... I'm not sure ...

I'm lacking enthusiasm right now (very strange of me, I know), so I'm going
to point you to Dejanews and then go back to programming Omega.

http://x45.deja.com/%5bST_rn=ps]/getdoc.xp?AN=601942654&search=thread&CONTEXT=
958265382.201785353&HIT_CONTEXT=958265382.201785353&HIT_NUM=2&hitnum=12

I really, really wish I knew how to shorten that link -- I know it can be
done, but after about 15 minutes of working with it I'm at a loss. Please
don't let its length stop you from checking it out; it's a facinating, low
overhead solution for typechecking which seems to be a perfect fit for
concatenative languages.

>- "iepos" (Brent Kerby)

-Billy

iepos@tunes.org — 2000-05-14 01:47:43

> >I guess the type rules ML enforces are similar to the ones C
> >enforces ...
>
> C doesn't really enforce any real type rules, does it?

Hmm... well my "gcc" complains if I try to call an "int" or add two
functions, or pass wrong-type parameters to functions. Of course,
the rules aren't really "enforced", since you can always get around
them with a cast; I guess that's what you meant.

> >Both branches in "if" must have the same types; this is guaranteed by
> >the fact that "if"s in those languages never have return values, and
> >only take parameters from the environment. Similarly, loops do not
> >have return values, and only take parameters from the environment.
>
> 'if's in ML do have return values. Perhaps you're thinking of the wrong
> language, because I can't think of a worse comparison than one between ML
> and C.

Okay, you're right. I'd better stop talking about ML :-)

> I forgot to mention that there's a type hierarchy. For example, both
> pointers and integers are "cells", and there's a version of SWAP which will
> therefore handle them. double integers are double cells, and there's a
> version of SWAP to handle double cells, and another version which takes as
> input a double and a single, and another one whose input is the other way
> around.

Okay, that makes sense.

> >> Have I explained the compile-type-stack method of compile
> >> time type checking
> >> and polymorphism? It's very nice, and fits in elegantly with Forth.
>
> >Maybe you have ... I'm not sure ...
>
> I'm lacking enthusiasm right now (very strange of me, I know), so I'm going
> to point you to Dejanews and then go back to programming Omega.
>
> http://x45.deja.com/%5bST_rn=ps]/getdoc.xp?AN=601942654&search=thread&CONTEXT=
> 958265382.201785353&HIT_CONTEXT=958265382.201785353&HIT_NUM=2&hitnum=12

Ahh... this is the discussion on comp.lang.forth ...

> >- "iepos" (Brent Kerby)
>
> -Billy

- "iepos (Brent Kerby)