Browse Groups

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

(8)
• NextPrevious
• 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 :) ... I would write
Message 1 of 8 , Feb 14, 2001
View Source
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
)

> 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 :

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

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
• ... 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
Message 1 of 8 , Mar 7, 2001
View Source
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,
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
• On Wed, 14 Feb 2001 ndg-51@mdstud.chalmers.se wrote: (sorry thatit took so long to reply - MvT) ... Yes, this looks promising. ... I meant, of course: S1 - S2
Message 1 of 8 , Mar 19, 2001
View Source
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

- Manfred
• ... 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
Message 1 of 8 , Apr 3, 2001
View Source
--- 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,
> 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?

>
> > (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
)

> I'll respond to the later parts of your post soon.
> - Manfred
• ... (no prob) ... object ... exactly !! ... application) ... ooops (of couse i meant s3 :) ... interesting (the \$ operator in haskell is not used too often
Message 1 of 8 , Apr 3, 2001
View Source
--- 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

> 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
++ : (String,String) -> String (no side effect here)
(++ is string concatenation, infix)
and a main program
main : void -> void
{
writeString "What is your name ?\n> " ;
writeString ("Hello, " ++ name ++ ", pleased to meet you !\n") ;
}

writeString : (String,WorldState) -> WorldState
++ : (String,String) -> String

main : WorldState -> WorldState
main w0 = let w1 = writeString (,w0)
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
but it's much harder)
properties like, this function returns a sorted list given that it's
argument is a sorted list ..

writeString : String -> IO Void
++ : (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> " >>
writeString ("Hello, " ++
name ++
", pleased to meet you !\n")
('\x -> ...' is lambda expressions)
or with syntactic sugar :
main = do writeString "What is your name ?\n> "
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
Your message has been successfully submitted and would be delivered to recipients shortly.
• Changes have not been saved
Press OK to abandon changes or Cancel to continue editing
• Your browser is not supported
Kindly note that Groups does not support 7.0 or earlier versions of Internet Explorer. We recommend upgrading to the latest Internet Explorer, Google Chrome, or Firefox. If you are using IE 9 or later, make sure you turn off Compatibility View.