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

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