Ideas slowly growing in my head.

sz — 2000-12-04 16:20:26

Hello Concatenative,


I. TYPES

I thought about introducing type system in Joy and finally come
to some interesting ideas. Interesting to me, of course. ;)

I base my observation on works of Jaanus Pцial:

Pцial J.═ "Alternative Syntactic Methods for Defining Stack Based
Languages." Proceedingsof NWPER'98 Nordic Workshop on Programming
Environment Research, Reportsin Informatics No 152, University of
Bergen, Norway, June 1998, 227 - 232.

and

Pцial J.═"Forth and Formal Language Theory." EuroForth'94, Nov 4 - 6, 1994,
Winchester,UK, 1994, 47 - 52.

These papers easily available from
http://www.cs.ut.ee/~jaanus/poialpub.html

The idea is very cute and simple and I explain it down here in brief.

There is a set of stack pictures:
%a <- %A
(%a - is an unknown stack picture, <- - "belongs to", %A - set of
possible stack pictures.)

There is a set of stack effects:
(%a -- %b)
which forms set S of stack effects.

For stack effects a multiplication operation is defined:
(%a -- %b %c) (%c -- %d) === (%a -- %b %d)
(%a -- %b) (%c %b -- %d) === (%c %a -- %d)
other combination of stack effects produce 0 - type clash.
Identity stack effect ( -- ) is unit for this binary operation.

I'd like to introduce named parameters into Joy language
like Manfred did (not so) long time ago. And also I change
syntax and semantics of Joy slightly to better suit my needs.
This is virtual change as I still on the thought way and didn't
finally consider what to implement and what to throw away.

The first change is the presence of named variables. They are
essential for any practical programming needs as they carry meaning
of entities in their symbolic names.

Simplest example of new Joy syntax with variables is swap:
x y dup == y x ;

Which, obviously, has stack effect (a b -- b a), where a and b
are type variables.

Quotation
[ 1 ]
has stack effect
( -- Int).

Another example is new dip combinator:
x y dip == x dequo y dequo ;
which has not so simple stack effect. Actually, it has two (or more)
stack effects:
(%a (%a -- %b %c) (%c -- %d) -- %b %d) and
(%a %b (%b -- %c) (%a %c -- %d) -- %d).

Combinator dequo is the new name for good old i combinator, which
has name which is too short for my purposes. I prefer i to be name
of variable, as it will be referred more often. By the way, dequo
stack effect is
(%a (%a -- %b) -- %b).

dip will have more stack effects if we assume that no stack pictures
could be implicitly empty. I.e., if there is %a, then %a is non-empty.
It is simplify programming of stack effect calculations but clutters
up output. But I didn't come into any conclusion about it so far.

This algebra of stack effects leads me into two philosophical observation:
- first, there should no way to specify a stack effect with unknown
stack picture on either left or right side. I should have either a method
to consume unknown stack effect or method to produce it. Latter is
meaningless because internal structure of arbitrary stack picture on the
right hand side is lost after end of calculation. Former is more usable
because it is possible to have a method which produce, for example, a
string from fixed but unknown at compile time collection of items on
the stack and then prints it on the terminal. Then stack effect
(%a (%a -- String) -- )
is perfectly legal.
- second observation is a mere extention of first which simplify
our deal with stack pictures of unknown structure. We can make them well
known using... sum types. ;)

I should also note that I think that quotation should have only composition
operation, because decomposition of quotation is meaningless (in my humble
opinion). When we take quotation apart what we get? A first element which
takes (or not at all) some (known at compile time) parts of stack picture
and produce unknown stack picture. Then the only stack effect which will
be legal is the stack effect of the rest of quotation. Also quotations
may be hold together in sum types and parts of quotation are always
accessible at compile time.

Of course, previous paragraph is also of philosophical nature. ;)


II. (ALMOST) COMPLETE SYNTAX

I think that my system should be compiler-oriented rather than
interpreter-oriented. That's where all complication grow from.

I split identifier into keywords (such as "module", "data", "typesyn" etc),
(de)constructors (like "True" or "List") and definitions ("dup").

All they have almost identical syntax:
\\ header of module with name "Test" and list of exports in
\\ square brackets.
Test module == [ List, Bool, putstring ] ;

\\ polymorphic type List
a List == a (a List) Cons | Nil ;

\\ Enum type Bool
Bool == True | False ;

\\ a definition using pattern matching
(x s Cons) putstring == x putchar s putstring ;
(Nil) putstring == ;

\\ and variables alone
x y swap == y x ;

\\ class of droppable types
a Drop class == (a -- ) drop ;
\\ class of dupable types
a Dup class == (a -- a a) dup ;

\\ class of numeric types:
a Num class ==
( -- a) 0 | \\ polymorphic constant
(a a -- a) + , - , * , / |
(a -- a) neg == 0 swap - ; \\ default method

Expressions in brackets are pattern-matching and variable binding
expressions. I hide elements from stack into variables and then
compiler deals with stack rearrangement. Actual implementation
may use whatever it wish for it - from second stack to stack
frame like in C language. But essential characteristics of type for
compiler to deal with it freely is the presence of dup and drop
operations. One operation produces a copy of item, another - deletes
it. Objects with these operations are non-linear (in the sense of
linear logic). Restricting dup and drop rights we may get desirable
effects - for example, the only way for FILE object to disappear is
to use fclose definition:
fclose (FILE -- ERRNO) ;

There are many things I can speculate about, but this letter is already
too long for me. So...


III. WHERE IS HENRY BAKER HOMEPAGE?!

I decided to reread his papers on linear logic and failed to find
his homepage.


Best regards,
sz mailto:sz@...

phimvt@lurac.latrobe.edu.au — 2000-12-20 05:04:04

On Mon, 4 Dec 2000, sz wrote:

> I thought about introducing type system in Joy and finally come
> to some interesting ideas. Interesting to me, of course. ;)

> [some stuff snipped]

> The idea is very cute and simple and I explain it down here in brief.
>
> There is a set of stack pictures:
> %a <- %A
> (%a - is an unknown stack picture, <- - "belongs to", %A - set of
> possible stack pictures.)
>
> There is a set of stack effects:
> (%a -- %b)
> which forms set S of stack effects.
>
> For stack effects a multiplication operation is defined:
> (%a -- %b %c) (%c -- %d) === (%a -- %b %d)
> (%a -- %b) (%c %b -- %d) === (%c %a -- %d)
> other combination of stack effects produce 0 - type clash.

It would be nice to see some examples - I could not quite
see how this would look like in practice

[More stuff snipped]

> The first change is the presence of named variables. They are
> essential for any practical programming needs as they carry meaning
> of entities in their symbolic names.
>
> Simplest example of new Joy syntax with variables is swap:
> x y dup == y x ;
>
> Which, obviously, has stack effect (a b -- b a), where a and b
> are type variables.
>
> Quotation
> [ 1 ]
> has stack effect
> ( -- Int).
>
> Another example is new dip combinator:
> x y dip == x dequo y dequo ;
> which has not so simple stack effect. Actually, it has two (or more)
> stack effects:
> (%a (%a -- %b %c) (%c -- %d) -- %b %d) and
> (%a %b (%b -- %c) (%a %c -- %d) -- %d).
>
> Combinator dequo is the new name for good old i combinator, which
> has name which is too short for my purposes. I prefer i to be name
> of variable, as it will be referred more often. By the way, dequo
> stack effect is
> (%a (%a -- %b) -- %b).
>
If you want type variables (even multiletter) that will not be
mistaken for Joy2 operators, maybe you should use capitals -
they are hardly used in Joy except for a tiny number of reserved
words that will hardly be confused with the type variables.
>
>
> I should also note that I think that quotation should have only composition
> operation, because decomposition of quotation is meaningless (in my humble
> opinion).

I agree in a way. Joy currently is an "intensional language", and
it is not entirely clear whether that is a good idea. You might
want to look at my (relatively new) paper "Rationale for Joy"
on the web page. I discuss the problem(?) towards the end.
For a compiled version of Joy indeed such a prohibition makes
a lot of sense.

> I think that my system should be compiler-oriented rather than
> interpreter-oriented. That's where all complication grow from.
>
> I split identifier into keywords (such as "module", "data", "typesyn" etc),
> (de)constructors (like "True" or "List") and definitions ("dup").
>
Don't be too ambitious. Try small things first. Modules might be
a great, useful and perhaps indispensible idea, but not for a
first version.

[lots of good stuff snipped]

. But essential characteristics of type for
> compiler to deal with it freely is the presence of dup and drop
> operations. One operation produces a copy of item, another - deletes
> it. Objects with these operations are non-linear (in the sense of
> linear logic). Restricting dup and drop rights we may get desirable
> effects - for example, the only way for FILE object to disappear is
> to use fclose definition:
> fclose (FILE -- ERRNO) ;
>
I would like to see more examples of how you think the dup and drop/pop
operations should be restricted, and what benefit that would have.

In general, if you want more discussion, give us some examples of
a) wrongly typed programs (with proposed error message), and
b) correctly typed programs (with proposed run time behaviour), and
c) programs (if any) which would be OK in Joy but not in your
typed version.
As to c), you will, I take it, allow lists of lists. But will you
allow heterogenous lists, consisting, say, of a name (a string or
a list of chars) and a phone number?

[ [ "Mary" 19827364 ]
[ "Jane" 83472364 ] ]

You might have to go for what in ML and Haskell are called tuples,
I think (experts please comment).

As a final comment, I would urge you not to attempt a compiler, not
even one that compiles into C or Oberon or whatever. Try your ideas
about typing Joy on an interpreter, it is so much easier.

In any case, best wishes for your project.

To all in the group, a happy Christmas.

- Manfred (expecting 40 degrees Centigrade here in Melbourne tomorrow !)