sz — 2000-12-23 12:35:11

Hello Phimvt,

пятница, 22 декабря 2000 г., you wrote:

>> Hello Phimvt,
>>
>> среда, 20 декабря 2000 г., you wrote:
>>
>> It is more a matter of language design. For example:
>>
>> intToCharString 1 == '1 "Wow! One!!" ;
>> intToCharString 2 == '2 "Wow! Two!!!" ;
>> intToCharString _ == '? "Unknown number." ;

pllea> So, pattern matching? I have considered this several times,
pllea> but put it into the "maybe-later" basket

I just cannot take serious any language without pattern matching. ;)

And one more point - I wrote several first paragraphs of previous
letter in some hurry and mess things up a little.

Basic information channel for Joy' (let's call it so) are stacks. One
stack is main data stack which is used by definitions and another is
permutation stack, where we put items by variable bindings in pattern
matching. Definitions use latter stack too, but in a transparent way.
Compiler also is a stack-driven beast. Compiler stack holds lexems.

Basic phrase of language looks like:
bindings defname '==' body ';'
or
bindings keyword ';'

Function and type definitions use first phrase structure, any control
structures - second. Then NamePhone, usual List and intToCharString
will look like:

NamePhone == [Char List] Int NamePhone ;
a List == a Cons | Nil ;
left right Either == left Left | right Right ;
// A special feature - synonim for function that takes a type
// and produces a string:
a Convertor == (a -- String) synonim ;
// Another synonim:
String = Char List synonim ;

1 intToCharString == '1 "Wow! One!!" ;
_ intToCharString == '? "Unknown number." ;

I thought it will be processed like this: lexer gives us lexem, we put
it into stack, then we encounter '==' (which pops last item), look, is
it TypeName or defName and calls appropriate body processor.

We should place arguments bindings in the order they put into stack.
It holds for both type expressions and definitions.

NumRes == Int Float Either synonim ;
a b minus = a b - ;

As careful reader may notice I'm trying to reinvent ML/Haskell type
system in a Joy way. I think it is not a wasteful job given the fact
that original ML type system (where Haskell borrowed its) was more
like Joy one. For example: "type 'a test = TC of 'a | TN ;;". In a
concatenative style it may be rewritten " 'a Test == 'a TC | TN ;".
The keyword "of" in "TC of 'a" means nothing more than delimiter to
make sure that type expression "'a" is of right kind one, ie, does not
require any specialization.

>> I think that it would be easier to explain in another way.
>> We may define a ordering operator '<=' for stack effect lists like
>> this:
>> %a <= %b if there is (may be empty) list %c such that concatenating %c
>> with %a gives us %b. Otherwise %a is greater than %b or they cannot be
>> compared. %a and %b cannot be compared if NOT (%a <= %b) and NOT
>> (%b <= %a).

pllea> Yes, something along these lines seems correct

This is incomplete.
From that ordering operator we may deduce substraction operator '-':
%c = %a - %b
if concatenation of %c and %b (%c++%b) is equal to %a. It may be Not A
Stack Effect (type clash) if %b is greater than or not comparable with
%a.
Then stack effect matching is simply substraction:
concatenation (%a -- %b) (%c -- %d) is
({%c-%b} %a -- %d) if {%c-%b} exist or
({%a -- {%b-%c} %d) if {%b-%c} exist.
Otherwise it is a stack effect type clash.
If %b is equal to %c we get two identical stack effects.

This is what was written in the original lines:
(%a -- %b %c) (%c -- %d) === (%a -- %b %d)
(%a -- %b) (%c %b -- %d) === (%c %a -- %d)
otherwise it is a type clash.

>> Variant ][.
>> Definition 'main' should have effect (World -- World).
>>
>> main == "Hello, world!" // World [Char List]
>> swap // [Char List] World
>> putStr // [Char List] World -- World
>> ;

pllea> I don't get it. What is being swapped in line 2?

Something of World type (a run-time system data structure) and value
"Hello, world!" of type [Char List].

>> Right now I cannot show how mul_ni will produce type clash. But
>> produce_ni certainly will.

pllea> I find the example very difficult. Could you specify some simpler ones,
pllea> please ?

zerocounter == [dup 0 =] [drop True] [False] ifte ;
is very similar to useful Forth word called "?dup".
It is clearly of wrong stack effect type: different branches of ifte
has (a -- Bool) for [drop True] and (-- Bool) for [False].
But it can be very useful for cyclic control structures.

>> pllea> As to c), you will, I take it, allow lists of lists. But will you
>> pllea> allow heterogenous lists, consisting, say, of a name (a string or
>> pllea> a list of chars) and a phone number?
>>
>> pllea> [ [ "Mary" 19827364 ]
>> pllea> [ "Jane" 83472364 ] ]
>>
>> For me it is better to put them into constructor.
>> data NamePhone == [Char List] Int NamePhone ;

pllea> I'm beginning to see, but what does that list of phone numbers look like
pllea> in your notation?
[ ['M 'a 'r 'y] 123456789 NamePhone "Jane" 987654321 NamePhone]
That direction.

Buy!
sz mailto:sz@...

phimvt@lurac.latrobe.edu.au — 2001-01-24 05:42:08

On Sat, 23 Dec 2000, sz wrote:

> pllea> So, pattern matching? I have considered this several times,
> pllea> but put it into the "maybe-later" basket
>
> I just cannot take serious any language without pattern matching. ;)

That leaves out most languages - are you serious?

> Basic information channel for Joy' (let's call it so) are stacks. One
> stack is main data stack which is used by definitions and another is
> permutation stack, where we put items by variable bindings in pattern
> matching. Definitions use latter stack too, but in a transparent way.
> Compiler also is a stack-driven beast. Compiler stack holds lexems.

Oops. I don't follow. There is the C-stack (invisible to the user)
which is used for recursion. Then there is the Joy-stack, most prominent,
on which all visible operations take place. There is also the symbol
table which has definitions added as they occur - but it is not a stack
at all because you cannot (normally) delete or "pop" definitions,
and there are no unary or binary operations for it. In fact the
symbol table can be implemented in many ways. It can be a growing list
which is searched linearly - but that is not a stack. It can be
a lot of growing lists in a hash bucket. It can be hashed in other ways.
If one insisted on a maximum length of say 3 letters for each
defined name, then it could be an 3 dimensional array [26,26,26]
for which lookup would be constant.

> We should place arguments bindings in the order they put into stack.
> It holds for both type expressions and definitions.
>
> NumRes == Int Float Either synonim ;
> a b minus = a b - ;

I did not understand this.

> As careful reader may notice I'm trying to reinvent ML/Haskell type
> system in a Joy way. I think it is not a wasteful job given the fact
> that original ML type system (where Haskell borrowed its) was more
> like Joy one.

I tink you are right in adopting as much as possible from the
well proven ML and Haskell type systems.

My own thought go along these lines:

Write the Joy-stack in a Prolog like style -
[S1 S2 | S] is a stack of at least two elements S1 and S2,
and S is the (possibly empty) remainder.

Then we have for addition e.g.
+ : [3 2 | S] -> [5 | S]
The general typing rule for addition then is
+ : [Int Int | S] -> [Int | S]
"The type of + is a unary operation from a stack of two integers
on the top to a stack of one integer on top, with the remainder
of the stack unchanged."

We also have for literals:
3 : [S] -> [3 | S]
numeral : [S] -> [Int | S]
"The type of a numeral is a unary operation from any stack
to a stack which has an integer on top, with the remainder..."

I'll write lists of a given type T as T-list.
concat : [T-list T-list | S] -> [T-list | S]
where T is any type.

Literal lists are written inside [..]
[T-list] : [S] -> [T-list | S]

Quotations being used by combinators denote programs from stacks
to stacks. For example, here is the typing rule for map:
If Q : [T | S1] -> [T | S1]
then map : [[Q] T | S2] -> [T | S2]
which one might rewrite in this style:
map : [[[T | S1] -> [T | S1]] T | S2] -> [T | S2]

Very importantly, a rule for program concatenation is needed:
If P : S1 -> S2
and Q : S2 -> S3
then P Q : S1 -> S3
or perhaps in this style:
S1 -> S2 S2 -> S3 : S1 -> S2

I am not too sure about the last two "styles", though.

All of this leaves out input and output. In the prototype Joy
the default mode is for automatic output of the top of stack
when the end of program has been reached. This eliminates
the need for an explicit output operation at the end of the
program. There are two other settings: at the end of program
write the whole stack, or don't write anything. A fourth
and fifth might be: after every operation write the top,
or write the entire stack.

If the idea is to use explicit put for output and get for
input, then the two files have to be made explict in the
typing. Programs are now unary functions from a triple
consisting of a stack and two files to another such triple.
All the above typing rules should now be rewritten, e.g.
+ : ([Int Int | S],Ifile,Ofile) -> ([Int | S],Ifile,Ofile)

The rules for get and put need a notation for the two files:
I'll write them as lists - Ifile in the obvious order,
with the first list element as the next available item for get,
but Ofile with the first element as the most recently added
item by put.
get : (S,[T | Ifile],Ofile) -> ([T | S],Ifile,Ofile)
put : ([T | S],Ifile,Ofile) -> (S,Ifile,[T | Ofile])

Things get messier if one has not just a single input file
but a stack (really) of them. This is what the prototype
Joy has at the moment. A new input file is pushed onto the
Istack by the include operator which expects a string
on top of the stack and pushes the file pointer of a file
of that name onto the Istack. Subsequent input is from that
new file. At end of file the pointer is popped and input resumes
from the previous file (pointer) on top of the stack.

The typing rules for everything now have to be expanded
in a trivial way to replace the Ifile by the Istack.
The typing rule for the include operator now is
include : ([String | S],Istack,Ofile) -> (S,[Newfile | Istack],Ofile)

Even messier once one introduces a stack of output files.

This will have to do for the time being.

> pllea> I'm beginning to see, but what does that list of phone numbers look like
> pllea> in your notation?
> [ ['M 'a 'r 'y] 123456789 NamePhone "Jane" 987654321 NamePhone]

I saw a better one in some ML or Haskell web page some time ago, but
unfortunately I did not keep it. There were some type definitions, and
the phone list looked like this
[ ("Mary" 12345678) ("Jane" 87654321)]
from memory.

I hope your typed Joy will progress well

Best wishes for the new year to all

Manfred von Thun
Philosophy Department, La Trobe University

http://www.latrobe.edu.au/www/philosophy/phimvt/s00bok.html
( SYMBOLIC PROCESSING IN PASCAL - many programs at different levels )
http://www.latrobe.edu.au/www/philosophy/phimvt/j00syn.html
( JOY - a programming language based on function composition )

phimvt@lurac.latrobe.edu.au — 2001-01-25 01:06:45

On Wed, 24 Jan 2001 phimvt@... wrote:

> Quotations being used by combinators denote programs from stacks
> to stacks. For example, here is the typing rule for map:
> If Q : [T | S1] -> [T | S1]
> then map : [[Q] T | S2] -> [T | S2]
> which one might rewrite in this style:
> map : [[[T | S1] -> [T | S1]] T | S2] -> [T | S2]

This is wrong in two ways: 1. The argument and result of Q need not be of
the same type, so I'll take them to be T and U. 2. Map takes a list as
second parameter and produces a list as top value. The two lists are
of type T-list and U-list. Thus

If Q : [T | S1] -> [U | S1]
then map : [[Q] T-list | S2] -> [U-list | S2]
which one might rewrite in this style:
map : [[[T | S1] -> [U | S1]] T-list | S2] -> [U-list | S2]

Sorry,
Manfred

ndg-51@mdstud.chalmers.se — 2001-02-14 20:09:19

I've only toyed a little with Forth and just found out about Joy, but
anyway ..
(On the other hand I know some things about type systems :)

--- In concatenative@y..., phimvt@l... wrote:

> On Sat, 23 Dec 2000, sz wrote:
> > NumRes == Int Float Either synonim ;

I would write that :
type NumRes == Int Float Either ;
This is the type of objects which contain
either an object of type 'Int' or an object of type 'Float'

'Either', which is a parametricised algebraic datatype,
could perhaps be defined :
data a b Either == a Left
| b Right ;
or *maybe* like :
data Either == pop Left
| swap pop Right ;
(If you happen to don't like named (type) arguments)
(This is perhaps not the best syntax)

So if an object has type 'a b Either',
for some types a and b, said object contains
either an object of type 'a' or an object of type 'b'
(And you can determine at runtime which alternative
a specific object is)

> > a b minus = a b - ;
>

This seems like a (trivially) pattern matching defined function(/word)
equivalent to :
minus == - ;

Non-trivial possible examples :
0 fac == 1 ;
n fac == n dup 1 - fac * ;

[] len == 0 ;
x xs cons len == 1 xs len + ;

This is a little harder to write without pattern matching,
but now we have to handle formal parameters (where to store them ?) ..
So maybe pattern matching is not wanted because of that ??

Maybe one could do a non-destructuring and non-binding pattern
matching :
0 fac == pop 1 ;
_ fac == dup 1 - fac * ;

[] len == pop 0 ;
_ _ cons len == 1 swap rest len + ;

These easy examples can of course be written with some recursion
combinator instead, but is this feasable for larger functions, like
merging two sorted lists to one sorted list ?

> I did not understand this.
>

I hope this was somewhat understandable

> > As careful reader may notice I'm trying to reinvent ML/Haskell
type
> > system in a Joy way. I think it is not a wasteful job given the
fact
> > that original ML type system (where Haskell borrowed its) was more
> > like Joy one.
>
> I tink you are right in adopting as much as possible from the
> well proven ML and Haskell type systems.
>
> My own thought go along these lines:
>

A somewhat similar approach to typing code using stack :
http://www.cse.ogi.edu/~mpj/pubs/funJava.html
(Which I haven't looked much upon)

> Write the Joy-stack in a Prolog like style -
> [S1 S2 | S] is a stack of at least two elements S1 and S2,
> and S is the (possibly empty) remainder.
>

Would be :
s1 <| ( s2 <| s )
in his notation ( '<|' is meant to resemble the triange he uses)
Or without the parenthesis (if <| is right-associative)
s1 <| s2 <| s

> Then we have for addition e.g.
> + : [3 2 | S] -> [5 | S]
> The general typing rule for addition then is
> + : [Int Int | S] -> [Int | S]

+ : Int <| Int <| s -> Int <| s
(for any (stack) type s)

> "The type of + is a unary operation from a stack of two integers
> on the top to a stack of one integer on top, with the remainder
> of the stack unchanged."
>
> We also have for literals:
> 3 : [S] -> [3 | S]
> numeral : [S] -> [Int | S]

<numeral> : s -> Int <| s
(so Int is the type of the actual object residing on stack,
but 5 has abovementioned function (stack transformer) type
)

> "The type of a numeral is a unary operation from any stack
> to a stack which has an integer on top, with the remainder..."
>
> I'll write lists of a given type T as T-list.
> concat : [T-list T-list | S] -> [T-list | S]
> where T is any type.
>

If 'List' is a parametricised algebraic datatype :
data a List = []
| a (a List) cons
or maybe
data a List = []
| a a List cons
(pushing two 'a':s on type stack and then using List to transform
top element to type 'a List'. If cons would be given object
on stack corresponding to those types, it would construct an object
of type 'a List'
for any type 'a'
)

concat : t List <| t List <| s -> t List <| s
(for any type 't' and stack type 's')

> Literal lists are written inside [..]
> [T-list] : [S] -> [T-list | S]
>

[<object0 of type 't'> <object1 of type 't' ..]
: s -> t List <| s

> Quotations being used by combinators denote programs from stacks
> to stacks. For example, here is the typing rule for map:
> If Q : [T | S1] -> [T | S1]
> then map : [[Q] T | S2] -> [T | S2]
> which one might rewrite in this style:
> map : [[[T | S1] -> [T | S1]] T | S2] -> [T | S2]
ITYM
map : [[[T | S1] -> [T | S1]] T-list | S2] -> [T-list | S2]
>

map : (t <| s0 -> u <| s0) <| t List <| s -> u List <| s
(for any type 't','u','s')

> Very importantly, a rule for program concatenation is needed:
> If P : S1 -> S2
> and Q : S2 -> S3
> then P Q : S1 -> S3
> or perhaps in this style:
> S1 -> S2 S2 -> S3 : S1 -> S2
>

Wouldn't this be like trying to type function application in e.g.
haskell (@ is explicit left-associative infix function application)

(a -> b) a : b

Or with explicit function application '@' :

(a -> b) @ a : b

So if we write the (implicit) function composition with '.' :

(s1 -> s2) . (s2 -> s3) : s1 -> s2

Curiously enough, Haskell has an explicit function application
operator '$' which is defined as :
f $ x = f x

Maybe this is what you aim at here,
i.e explicit function composition operator ?

> I am not too sure about the last two "styles", though.
>

Why not ?
With the right syntax I think they could be quite readable

(Although, one could argue that '<|' and '->' should follow the same
postfix notation as everywhere else
This way we wouldn't have to use parenthesis at all in types
But these types looks much harder to understand now,
so probably this is a bad idea :( :
concat : t List t List s <| <| t List s <| ->
map : t s0 <| u s0 <| -> t List s <| <| u List s <| ->
)

> All of this leaves out input and output. In the prototype Joy
> the default mode is for automatic output of the top of stack
> when the end of program has been reached. This eliminates
> the need for an explicit output operation at the end of the
> program. There are two other settings: at the end of program
> write the whole stack, or don't write anything. A fourth
> and fifth might be: after every operation write the top,
> or write the entire stack.
>
> If the idea is to use explicit put for output and get for
> input, then the two files have to be made explict in the
> typing. Programs are now unary functions from a triple
> consisting of a stack and two files to another such triple.
> All the above typing rules should now be rewritten, e.g.
> + : ([Int Int | S],Ifile,Ofile) -> ([Int |
S],Ifile,Ofile)
>
> The rules for get and put need a notation for the two files:
> I'll write them as lists - Ifile in the obvious order,
> with the first list element as the next available item for get,
> but Ofile with the first element as the most recently added
> item by put.
> get : (S,[T | Ifile],Ofile) -> ([T | S],Ifile,Ofile)
> put : ([T | S],Ifile,Ofile) -> (S,Ifile,[T | Ofile])
>

Couldn't you let the files be ADTs and pass them on the stack :
get : Ifile <| s -> Char <| Ifile <| s
put : Char <| Ofile <| s -> Ofile <| s

(If you want referential transparency you'll have to use either
linear types or monads, though
)

> Things get messier if one has not just a single input file
> but a stack (really) of them. This is what the prototype
> Joy has at the moment. A new input file is pushed onto the
> Istack by the include operator which expects a string
> on top of the stack and pushes the file pointer of a file
> of that name onto the Istack. Subsequent input is from that
> new file. At end of file the pointer is popped and input resumes
> from the previous file (pointer) on top of the stack.
>
> The typing rules for everything now have to be expanded
> in a trivial way to replace the Ifile by the Istack.
> The typing rule for the include operator now is
> include : ([String | S],Istack,Ofile) -> (S,[Newfile |
Istack],Ofile)
>

(When I see this I wan't to hide state in a monad)

> Even messier once one introduces a stack of output files.
>
> This will have to do for the time being.
>
> > pllea> I'm beginning to see, but what does that list of phone
numbers look like
> > pllea> in your notation?
> > [ ['M 'a 'r 'y] 123456789 NamePhone "Jane" 987654321 NamePhone]
>
> I saw a better one in some ML or Haskell web page some time ago, but
> unfortunately I did not keep it. There were some type definitions,
and
> the phone list looked like this
> [ ("Mary" 12345678) ("Jane" 87654321)]
> from memory.
>

Oh yes, you must mean :
[("Mary",12345678),("Jane",87654321)] (In Haskell syntax)

An expression ( e1 , e2 ) is a pair of type '( t1 , t2 )'
given that the types of e1 and e2 is 't1' and 't2'

The only difference between this and the previous, is that we are
reusing the pair type instead of creating a new algebraic datatype

A definition for pairs :
data a b Pair = a b makePair ;

So the example then becomes :
["Mary" 123456789 Pair "Jane" 987654321 Pair]

(Of course the pairs in haskell is just syntactic sugar for this)

> I hope your typed Joy will progress well
>

It's a little cumbersome to always have to write the stack type
so what if we change the way we represent the type like this :

(<| is right associative
|> is left associative
)

dup : t <| s -> t <| t <| s
becomes
dup : t -> t |> t
which is equivalent to
dup : t |> t0 -> t |> t |> t0
dup : t |> t0 |> t1 -> t |> t |> t0 |> t1
...

and
+ : Int <| Int <| s -> Int <| s
becomes
+ : Int |> Int -> Int

(Building the stack from the top instead of from the bottom,
so to speak
)

So all the types of the rest of the stack will anyway not change,
so we might as well don't write them (as s), instead only write what
types we will change

This seems to be (almost) exactly the same as
the informal (a -- a a) specification

But what about :
i : (s -> t) <| s -> t
becomes
i : (t0 |> t1 |> ... -> s0 |> s1 |> ... ) |> t0 |> t1 |> ...
-> s0 |> s1 |> ...
It seems like this type would be infinitely large, not good !

Maybe this can be recovered with the use of restricted version of i,
which promise to only touch a finite amount of arguments.
e.g. :
i2_3 : (a0 <| a1 <| s -> b0 <| b1 <| b2 <| s) <|
a0 <| a1 <| s -> b0 <| b1 <| b2 <| s
becomes :
i2_3 : (a0 |> a1 -> b0 |> b1 |> b2) |>
a0 |> a1 -> b0 |> b1 |> b2
Although it seems a bit tedious to defined such versions of i
Maybe one could use both variants at the same time

At last, if a type system were realized, I think that the <| or |>
would be redundant (I've used it here for expliciticy)

I.e. dup would have type :
dup : a s -> a a s
respectively
dup : a -> a a
(compare (a -- a a))

> Best wishes for the new year to all
>
> Manfred von Thun
> Philosophy Department, La Trobe University
>
> http://www.latrobe.edu.au/www/philosophy/phimvt/s00bok.html
> ( SYMBOLIC PROCESSING IN PASCAL - many programs at different
levels )
> http://www.latrobe.edu.au/www/philosophy/phimvt/j00syn.html
> ( JOY - a programming language based on function composition )

Just my speculations

--
Stefan Lj
md9slj [at] mdstud [dot] chalmers [dot] se

Manfred von Thun — 2001-03-08 01:42:52

On Wed, 14 Feb 2001 ndg-51@... wrote:

> --- In concatenative@y..., phimvt@l... wrote:
>
> > On Sat, 23 Dec 2000, sz wrote:
> > > NumRes == Int Float Either synonim ;
>
> I would write that :
> type NumRes == Int Float Either ;
> This is the type of objects which contain
> either an object of type 'Int' or an object of type 'Float'

I think it will need a lost of discussion whether concatenative
notation (Forth, Joy) is really the best to use for types.
Also, distinguish concatenative notation from postfix notation.
For example,
add_three == + +
is perfectly OK concatenative notation, but of course the right
hand side does not denote a number. Let us now ask whether
there might be a use for
alt_three == Either Either
Maybe there is, but I don't see it yet. If there is no use for
that, then your particular example is best seen as just postfix
notation.
EXPRESSION denotes VALUE

arithmetic postfix --> number
type postfix --> type

arithmetic concatenative --> numeric_stack function
type concatenative --> type_stack function ???

> 'Either', which is a parametricised algebraic datatype,
> could perhaps be defined :
> data a b Either == a Left
> | b Right ;
> or *maybe* like :
> data Either == pop Left
> | swap pop Right ;

But Left and Right are not functions on type_stacks, I think (?).
It looks to me as though (in the first) a and b are given as
values to the Left and Right functions, and (in the second)
items 2 and 1 from the top of the type_stack are given as
value. Should one think of them as some sort of assignment?

> (If you happen to don't like named (type) arguments)

Could you elaborate on this a bit more, please.

> So if an object has type 'a b Either',
> for some types a and b, said object contains
> either an object of type 'a' or an object of type 'b'
> (And you can determine at runtime which alternative
> a specific object is)

I'm sorry it took so long to respond.
I'll respond to the later parts of your post soon.
- Manfred

Manfred von Thun — 2001-03-20 06:28:28

On Wed, 14 Feb 2001 ndg-51@... wrote:
(sorry thatit took so long to reply - MvT)

> > > As careful reader may notice I'm trying to reinvent ML/Haskell
> type
> > > system in a Joy way. I think it is not a wasteful job given the
> fact
> > > that original ML type system (where Haskell borrowed its) was more
> > > like Joy one.
> >
> > I tink you are right in adopting as much as possible from the
> > well proven ML and Haskell type systems.
> >
>
> If 'List' is a parametricised algebraic datatype :
> data a List = []
> | a (a List) cons
> or maybe
> data a List = []
> | a a List cons
> (pushing two 'a':s on type stack and then using List to transform
> top element to type 'a List'. If cons would be given object
> on stack corresponding to those types, it would construct an object
> of type 'a List'
> for any type 'a'
Yes, this looks promising.

> concat : t List <| t List <| s -> t List <| s
> (for any type 't' and stack type 's')
>
> > Literal lists are written inside [..]
> > [T-list] : [S] -> [T-list | S]
> >
>
> [<object0 of type 't'> <object1 of type 't' ..]
> : s -> t List <| s
> > Very importantly, a rule for program concatenation is needed:
> > If P : S1 -> S2
> > and Q : S2 -> S3
> > then P Q : S1 -> S3
> > or perhaps in this style:
> > S1 -> S2 S2 -> S3 : S1 -> S2
I meant, of course:
S1 -> S2 S2 -> S3 : S1 -> S3
^
or perhaps better:
(S1 -> S2) (S2 -> S3) : (S1 -> S3)
in other words: the concatenation of two (now unnamed) programs,
one of type (S1 -> S2) and the other of type (S2 -> S3),
has the type (S1 -> S3).

> Wouldn't this be like trying to type function application in e.g.
> haskell (@ is explicit left-associative infix function application)
>
> (a -> b) a : b
>
> Or with explicit function application '@' :
>
> (a -> b) @ a : b
>
> So if we write the (implicit) function composition with '.' :
>
> (s1 -> s2) . (s2 -> s3) : s1 -> s2
^ (you meant s3, I am sure)
Yes, this is exactly what I had in mind.

> Curiously enough, Haskell has an explicit function application
> operator '$' which is defined as :
> f $ x = f x
>
> Maybe this is what you aim at here,
> i.e explicit function composition operator ?
No, I did not want to make function composition explicit.
(There might be a good reason for making composition explicit
in case another binary operation is introduced that is best
written in infix. One candidate is "|", to be pronounced
"or", or "alternatively", similar to the vertical bar
in regular expressions and grammars. The "|" might
be paired with a "fail" operator to give backtracking.
So "." and "|" would be similar to "," and ";" in Prolog.
But just as regular expressions and grammars do quite
nicely without making both infix operators explicit,
so could Joy which has other infix operators.
Anyone out there want to implement a backtracking version
of Joy? If you do, take a look at the Pascal pages on my
web page. Lots of backtracking programs there.

> (Although, one could argue that '<|' and '->' should follow the same
> postfix notation as everywhere else
> This way we wouldn't have to use parenthesis at all in types
> But these types looks much harder to understand now,
> so probably this is a bad idea :( :
> concat : t List t List s <| <| t List s <| ->
> map : t s0 <| u s0 <| -> t List s <| <| u List s <| ->
Yes, agreed.
>
> > All of this leaves out input and output.

> > If the idea is to use explicit put for output and get for
> > input, then the two files have to be made explict in the
> > typing. Programs are now unary functions from a triple
> > consisting of a stack and two files to another such triple.
> >
> > The rules for get and put need a notation for the two files:
> > I'll write them as lists - Ifile in the obvious order,
> > with the first list element as the next available item for get,
> > but Ofile with the first element as the most recently added
> > item by put.
> > get : (S,[T | Ifile],Ofile) -> ([T | S],Ifile,Ofile)
> > put : ([T | S],Ifile,Ofile) -> (S,Ifile,[T | Ofile])
>
> Couldn't you let the files be ADTs and pass them on the stack :
> get : Ifile <| s -> Char <| Ifile <| s
> put : Char <| Ofile <| s -> Ofile <| s
Two comments: 1. I do not take get and put to be restricted to Chars.
2. One can indeed think of _both_ files as sitting on top of
the stack. Then all operations go from stacks to stacks. Only get
and put affect the top two elements of the stack. All other
operations only affect things below. [Of course an implementation
will make good use of this difference: treat the top two elements
differently.] Otherwise there is really no significant difference
between us, I think.

> (If you want referential transparency you'll have to use either
> linear types or monads, though
It would be great If you could elaborate on this. My own knowledge
is too superficial to comment at all.

> > Things get messier if one has not just a single input file
> > but a stack (really) of them. This is what the prototype
> > Joy has at the moment. A new input file is pushed onto the
> > Istack by the include operator which expects a string
> > on top of the stack and pushes the file pointer of a file
> > of that name onto the Istack. Subsequent input is from that
> > new file. At end of file the pointer is popped and input resumes
> > from the previous file (pointer) on top of the stack.
> >
> > The typing rules for everything now have to be expanded
> > in a trivial way to replace the Ifile by the Istack.
> > The typing rule for the include operator now is
> > include : ([String | S],Istack,Ofile) -> (S,[Newfile |
> Istack],Ofile)
>
> (When I see this I wan't to hide state in a monad)
Oh please explain how that would be done. I really would be
grateful.

> > Even messier once one introduces a stack of output files.
I suppose this can be done monadically, too

This will have to do for today. I'll respond to the remainder
of your long posting soon.

- Manfred

ndg-51@mdstud.chalmers.se — 2001-04-03 15:25:58

--- In concatenative@y..., Manfred von Thun <phimvt@l...> wrote:

>
> On Wed, 14 Feb 2001 ndg-51@m... wrote:
>
> > --- In concatenative@y..., phimvt@l... wrote:
> >
> > > On Sat, 23 Dec 2000, sz wrote:
> > > > NumRes == Int Float Either synonim ;
> >
> > I would write that :
> > type NumRes == Int Float Either ;
> > This is the type of objects which contain
> > either an object of type 'Int' or an object of type 'Float'
>
> I think it will need a lost of discussion whether concatenative
> notation (Forth, Joy) is really the best to use for types.

Yes, of course.
I think it would be nice to be as much uniform as possible,
i.e. concatenative notation with types as well, but if this is
awkward/unnessesary/too general/not wanted, there shouldn't be any
hindrance to use another notation

> Also, distinguish concatenative notation from postfix notation.
> For example,
> add_three == + +
> is perfectly OK concatenative notation, but of course the right
> hand side does not denote a number. Let us now ask whether
> there might be a use for
> alt_three == Either Either
> Maybe there is, but I don't see it yet. If there is no use for

I think one could come up with good used. (?)

> that, then your particular example is best seen as just postfix
> notation.

If the concatenative is not needed/used i'd like prefix more then
postfix (just a taste issue)

> EXPRESSION denotes VALUE
>
> arithmetic postfix --> number
> type postfix --> type
>
> arithmetic concatenative --> numeric_stack function
> type concatenative --> type_stack function ???
>

Hmm, maybe if the type expressions (concatenative) is (type) stack
transformers, then the final type would be denoted by a stack with
only one type on it. I.e. :

"type word"
Int (type_stack transform/function)
Char (ditto)
List (ditto)
Either (ditto)

type exression meaning
Int an integer
Char a character
Int List a list of integers
Int List List a list of list of integers
Int Char Either either an int or a char (possible to discern them)

so if we say that the "type" of types (i.e. kind) is '*'
Int : s -> * <| s
Char : s -> * <| s
List : * <| s -> * <| s
Either : * <| * <| s -> * <| s

so if we say
length : a List -> Int

'a List' could be seen as a type expression executed on an initial
empty type stack (presumable at compile-time) resulting in a type
stack with only one type on it (the resulting type)

> > 'Either', which is a parametricised algebraic datatype,
> > could perhaps be defined :
> > data a b Either == a Left
> > | b Right ;
> > or *maybe* like :
> > data Either == pop Left
> > | swap pop Right ;
> But Left and Right are not functions on type_stacks, I think (?).

Left and Right are words (functions/transforms on the data stack).
(maybe i should have named them left, right ..)
anyway

5 : s -> Int <| s
5 Left : s -> Int a Either <| s
5 Right : s -> a Int Either <| s
(for any type a and any (stack) type s)

so
5 Left
pushes a box labelled with 'Left' and 5 within on the stack

[] 5 Left cons 'a' Right cons
with type
s -> Int Char Either List <| s
pushes on the stack a list of either integers or characters

> It looks to me as though (in the first) a and b are given as
> values to the Left and Right functions, and (in the second)
> items 2 and 1 from the top of the type_stack are given as
> value. Should one think of them as some sort of assignment?

hmm, i've got to think a little about this

>
> > (If you happen to don't like named (type) arguments)
> Could you elaborate on this a bit more, please.

it's just that in applicative style you name the formal parameters to
a function and use them within it's body,
but in concatenative style you have the parameters on the stack and
manipulate the via dup,rot, etc (i.e. no naming of arguments)

but here i sort of reintroduced named arguments (if only in the type
langage)

>
> > So if an object has type 'a b Either',
> > for some types a and b, said object contains
> > either an object of type 'a' or an object of type 'b'
> > (And you can determine at runtime which alternative
> > a specific object is)
>
> I'm sorry it took so long to respond.

No problem with me (am i worse ? :-)
(actually i looked into this group a couple of times after my post but
not much had appeared, so i half forgot about this group until now :(
)

> I'll respond to the later parts of your post soon.
> - Manfred

ndg-51@mdstud.chalmers.se — 2001-04-03 16:19:04

--- In concatenative@y..., Manfred von Thun <phimvt@l...> wrote:

>
> On Wed, 14 Feb 2001 ndg-51@m... wrote:
> (sorry thatit took so long to reply - MvT)

(no prob)

>

> > If 'List' is a parametricised algebraic datatype :
> > data a List = []
> > | a (a List) cons
> > or maybe
> > data a List = []
> > | a a List cons
> > (pushing two 'a':s on type stack and then using List to transform
> > top element to type 'a List'. If cons would be given object
> > on stack corresponding to those types, it would construct an

object

> > of type 'a List'
> > for any type 'a'
> Yes, this looks promising.
>
> > concat : t List <| t List <| s -> t List <| s
> > (for any type 't' and stack type 's')
> >
> > > Literal lists are written inside [..]
> > > [T-list] : [S] -> [T-list | S]
> > >
> >
> > [<object0 of type 't'> <object1 of type 't' ..]
> > : s -> t List <| s
> > > Very importantly, a rule for program concatenation is needed:
> > > If P : S1 -> S2
> > > and Q : S2 -> S3
> > > then P Q : S1 -> S3
> > > or perhaps in this style:
> > > S1 -> S2 S2 -> S3 : S1 -> S2
> I meant, of course:
> S1 -> S2 S2 -> S3 : S1 -> S3
> ^
> or perhaps better:
> (S1 -> S2) (S2 -> S3) : (S1 -> S3)
> in other words: the concatenation of two (now unnamed) programs,
> one of type (S1 -> S2) and the other of type (S2 -> S3),
> has the type (S1 -> S3).

exactly !!

> > Wouldn't this be like trying to type function application in e.g.
> > haskell (@ is explicit left-associative infix function

application)

> >
> > (a -> b) a : b
> >
> > Or with explicit function application '@' :
> >
> > (a -> b) @ a : b
> >
> > So if we write the (implicit) function composition with '.' :
> >
> > (s1 -> s2) . (s2 -> s3) : s1 -> s2
> ^ (you meant s3, I am sure)

ooops (of couse i meant s3 :)

> Yes, this is exactly what I had in mind.
>
> > Curiously enough, Haskell has an explicit function application
> > operator '$' which is defined as :
> > f $ x = f x
> >
> > Maybe this is what you aim at here,
> > i.e explicit function composition operator ?
> No, I did not want to make function composition explicit.
> (There might be a good reason for making composition explicit
> in case another binary operation is introduced that is best
> written in infix. One candidate is "|", to be pronounced
> "or", or "alternatively", similar to the vertical bar
> in regular expressions and grammars. The "|" might
> be paired with a "fail" operator to give backtracking.
> So "." and "|" would be similar to "," and ";" in Prolog.
> But just as regular expressions and grammars do quite
> nicely without making both infix operators explicit,
> so could Joy which has other infix operators.
> Anyone out there want to implement a backtracking version
> of Joy? If you do, take a look at the Pascal pages on my
> web page. Lots of backtracking programs there.

interesting

(the $ operator in haskell is not used too often
example of use :
function1 (function2 arg1 (function3 (function4 arg2)))
can be written as :
function1 $ function2 arg1 $ function3 $ function4 arg2
or it can be written in this style :
(function1 . function2 arg1 . function3 . function4) arg2
this is almost equivalent to concatenative style
(function4 is executed first though)
)

> > (Although, one could argue that '<|' and '->' should follow the

same

> > postfix notation as everywhere else
> > This way we wouldn't have to use parenthesis at all in types
> > But these types looks much harder to understand now,
> > so probably this is a bad idea :( :
> > concat : t List t List s <| <| t List s <| ->
> > map : t s0 <| u s0 <| -> t List s <| <| u List s <| ->
> Yes, agreed.
> >
> > > All of this leaves out input and output.
>
> > > If the idea is to use explicit put for output and get for
> > > input, then the two files have to be made explict in the
> > > typing. Programs are now unary functions from a triple
> > > consisting of a stack and two files to another such triple.
> > >
> > > The rules for get and put need a notation for the two files:
> > > I'll write them as lists - Ifile in the obvious order,
> > > with the first list element as the next available item for get,
> > > but Ofile with the first element as the most recently added
> > > item by put.
> > > get : (S,[T | Ifile],Ofile) -> ([T | S],Ifile,Ofile)
> > > put : ([T | S],Ifile,Ofile) -> (S,Ifile,[T | Ofile])
> >
> > Couldn't you let the files be ADTs and pass them on the stack :
> > get : Ifile <| s -> Char <| Ifile <| s
> > put : Char <| Ofile <| s -> Ofile <| s
> Two comments: 1. I do not take get and put to be restricted to

Chars.

how do you mean ?

do you mean that get and put should be sort of overloaded for many
different data objects
(that could be achieved with ad-hoc overloading or type-classes (a la
haskell and mercury))

> 2. One can indeed think of _both_ files as sitting on top of
> the stack. Then all operations go from stacks to stacks. Only get
> and put affect the top two elements of the stack. All other
> operations only affect things below. [Of course an implementation
> will make good use of this difference: treat the top two elements
> differently.] Otherwise there is really no significant difference
> between us, I think.

that sound doable, but not so beautiful (IMHO)

> > (If you want referential transparency you'll have to use either
> > linear types or monads, though
> It would be great If you could elaborate on this. My own knowledge
> is too superficial to comment at all.

referential transparency means roughly that no function (word) has
(detectable) side-effects

that is, every function call given the same arguments should produce
the same result (so readChar which just reads from stdin and puts the
read char on the stack is prohibited)

monads is a way to use side-effects in a referential transparent way
(among other used)
(linear types is another way)

i could maybe elaborate more, but i've only used monads in functional
langages (but i think its doable in concatenative style) so i would
have to explain in that setting i think

> > > Things get messier if one has not just a single input file
> > > but a stack (really) of them. This is what the prototype
> > > Joy has at the moment. A new input file is pushed onto the
> > > Istack by the include operator which expects a string
> > > on top of the stack and pushes the file pointer of a file
> > > of that name onto the Istack. Subsequent input is from that
> > > new file. At end of file the pointer is popped and input resumes
> > > from the previous file (pointer) on top of the stack.
> > >
> > > The typing rules for everything now have to be expanded
> > > in a trivial way to replace the Ifile by the Istack.
> > > The typing rule for the include operator now is
> > > include : ([String | S],Istack,Ofile) -> (S,[Newfile |
> > Istack],Ofile)
> >
> > (When I see this I wan't to hide state in a monad)
> Oh please explain how that would be done. I really would be
> grateful.

one way to make (some) imperative programs into functional is to make
the state explicit and pass it from function to function.
(for example in problems with inherent state)
after a while this gets very tedious.

say imperative program :

we have some predefined functions (with side-effects)
writeString : String -> void
readLine : void -> String
++ : (String,String) -> String (no side effect here)
(++ is string concatenation, infix)
and a main program
main : void -> void
{
writeString "What is your name ?\n> " ;
name := readLine void ;
writeString ("Hello, " ++ name ++ ", pleased to meet you !\n") ;
}

functional variant (a la haskell)
writeString : (String,WorldState) -> WorldState
readLine : WorldState -> (String,WorldState)
++ : (String,String) -> String

main : WorldState -> WorldState
main w0 = let w1 = writeString (,w0)
(name,w2) = readString w1
w3 = writeString ("Hello, " ++
name ++
", pleased to meet you !\n"
,w2)
in w3

('let ... in ..' is local declarations)
here we explicitely pass world state from function to function
(w0 is first world state, w1 is w0 changed by first writeString ,etc)
what we gain by doing this is that we can reason about programs much
better, i.e. we can substitute equal be equal and prove properties
about our programs (we can prove properties about imperative programs,
but it's much harder)
properties like, this function returns a sorted list given that it's
argument is a sorted list ..

monadic functional style :
writeString : String -> IO Void
readString : IO STring
++ : (String,String) -> String

>> : (IO a,IO b) -> IO b ("sequence")
>>= : (IO a,a -> IO b) -> IO b ("bind")

main : IO Void
main = writeString "What is your name ?\n> " >>
readString >>= \name ->
writeString ("Hello, " ++
name ++
", pleased to meet you !\n")
('\x -> ...' is lambda expressions)
or with syntactic sugar :
main = do writeString "What is your name ?\n> "
name <- readString
writeString ("Hello, " ++
name ++
", pleased to meet you !\n")

IO Int represents a program (function) that takes a world state and
transforms it into a new world state and also returns an Int
but here the actual world state is hidden "inside" IO so you dont have
to pass it explicitely
'>>=' and '>>' sequences two programs (= world state
transformers+return value)
'>>=' passes the return value of the first program to the next as a
argument, while '>>' discards the result of the first program

are we sufficiently confused yet ? :-)

really, if you want to learn about monads (it's actually not that
difficult that it seems like here) i think we should discuss it
elsewhere ... (?)

> > > Even messier once one introduces a stack of output files.
> I suppose this can be done monadically, too

yes, i believe so

> This will have to do for today. I'll respond to the remainder
> of your long posting soon.
>
> - Manfred

Re[4]: [stack] Ideas slowly growing in my head.