# Re[4]: [stack] Joy, purely functional?

## Serguey Zefirov — 2001-12-11 11:32:53

    Hello Billy,

    понедельник, 10 декабря 2001 г., you wrote:

    BT> From: Serguey Zefirov [mailto:sz@...]

     >>What is more severe than possible functionalitylessness is a fact that

    >>concatenative languages do not have a type system with principal types

    >>(ie, every expression should have _single_ type). This is also true

    >>for Linear Logic and is certainly sad.

     BT> That doesn't make sense to me -- several people have designed static type

    BT> systems for concatenative languages, although the only one I know of that's

    BT> been implemented is strongForth (look it up on Google or talk to the author

    BT> on this list).  StrongForth isn't perfect, but its principle is, I believe,

    BT> good enough to build a type checker which can handle arbitrary code with no

    BT> runtime performance hit.  (The current version doesn't handle unbalanced

    BT> conditionals and loops; I've been working on a system which I believe

    BT> could.)

    I tried to develop a type notation for applicative languages, based on

    the following algebraic rules:

     0 - type clash

     1 - ( -- )

     * - is a table rule

         ( a -- b c ) ( c -- d)   ->  ( a -- b d)

         ( b -- c ) ( a c -- d)   ->  ( a b -- d)

         everything else is 0

         a,b,c and d are (maybe empty) sets of stack parameters.

    Here EXECUTE (i) has a type:

    ( alpha ( alpha -- beta) -- beta)

    where alpha and beta are lists of stack parameters.

    I tried my best to calculate type for concatenated EXECUTE's and

    failed to obtain a single expression type signature.

    (BTW, I've done several posts about it here a year or so ago)

    Maybe you succeed.

     >>To exemplify that I invite you (and everyone other in the list) to

    >>calculate type for expression

    >>i i

     BT> I, in turn, invite you to calulate the type of the expression i(i), as

    BT> expressed in an applicative language.  To match your challenge, I'm not

    BT> telling you which applicative language, nor giving you any declarations for

    BT> i.  Since I called it an "expression", though, you know for sure it's not

    BT> Lisp and probably not Fortran, so you have one hint I don't have.

    I thought that i is a combinator that resembles EXECUTE word in Forth.

    I was in some hurry writing this. Well, show me type signature for Forth's

    EXECUTE EXECUTE

    in any type notation for concatenative languages you wish. I think

    that it will contain several different signatures due to the lack of

    principal type.

    Then we going to applicative language.

    i(i)

    i is a function (a -> b). Since it is applied to function (a -> b)

    it's signature ( c -> b, c == a -> b), or (a -> b -> b). Repeating

    substitution further we found that we dive into endless recursion and

    hugs (a Haskell implementation) tells us about it.

    BT> In other words, I don't think you've given enough information; and I think

    BT> that's true for your question in ANY language.

    Well, not. ;) In applicative languages it just does not allowed.

     >>'i i' has a bunch of possible types, and their number depends on how

    >>we differe lists of arguments (in my understanding of this).

     BT> How could it?  In a concatenative language there are no arguments.

    Oops, there are. putchar should have char on top of stack to output

    it. There is one argument (stack) but it is just inconvenient to view

    it without details. There are arguments, otherwise type system is

    irrelevant.

     >>This somewhat prevents one from reasoning about programs, especially,

    >>their parts.

     BT> As I've mentioned, several people have designed static type systems;

    BT> additionally, programmers have been reasoning about Forth programs for three

    BT> decades.

    Let's read - "makes it harder to reason about..." When I get

    thirty-two different type expressions for innocent line I get stuck

    for sure. It is joke but not without sense.

    Best regards,

    Serguey Zefirov               mailto:sz@...

## Serguey Zefirov — 2001-12-11 11:45:53

    Hello Louis,

    вторник, 11 декабря 2001 г., you wrote:

    LM> On Monday, December 10, 2001, at 11:37  PM, Serguey Zefirov wrote:

     >> What is more severe than possible functionalitylessness is a fact that

    >> concatenative languages do not have a type system with principal types

    >> (ie, every expression should have _single_ type). This is also true

    >> for Linear Logic and is certainly sad.

    >>

    >> To exemplify that I invite you (and everyone other in the list) to

    >> calculate type for expression

    >>

    >> i i

    >>

     LM> Joy doesn't have a type notation, so I'll invent one quickly: [t] means

    LM> a quoted type for some arbitrary type t, [[t]] means double quoted and

    LM> this is indeed the type required by ii. Many kinds of values have the

    LM> type [[t]] including for example [[3]] and [[4 +] 3 cons]

    This is just a part of type signature. One single line. It does not

    mention relationship between input stack, output stack and stack on

    entry of enclosed quotation.

     >> 'i i' has a bunch of possible types, and their number depends on how

    >> we differe lists of arguments (in my understanding of this).

    >>

     LM> If you're getting multiple types for some expression, then that is more

    LM> an artifact of the type system you've chosen rather than the language

    LM> itself.

    LM> As an extreme example, I can state that all programs in any language

    have the type "a ->> b" where a is some arbitrary input and b is some

    LM> derived output. From this, I can conclude that all languages have

    LM> principle types.

    This is very reasonable, I agree, but simplistic to no-use. As no-use

    as "concatenative programs have no parameters".

    LM> Languages like Clean and Haskell do have decidable type systems but only

    LM> because their language designers chose to limit the expressiveness of

    LM> the underlying untyped language.  For example, if the type system didn't

    LM> get in the way, you would be able to define a 'printf' type function

    LM> where the types of the second and subsequent arguments are determined by

    LM> the first argument.

    BTW, so called existential types handle this as well without

    sacrificing decidability.

    LM> If you wanted to, you could similarly limit Joys expressiveness and so

    LM> define a decidable type system for it, but I dislike that approach.

    Well, I'd like to see your approach.

    Best regards,

    Serguey Zefirov               mailto:sz@...

## Louis Madon — 2001-12-11 12:47:06

    On Tuesday, December 11, 2001, at 09:45  PM, Serguey Zefirov wrote:

     > Hello Louis,

     Hello Serguey,

     >

    > вторник, 11 декабря 2001 г., you wrote:

    >>> To exemplify that I invite you (and everyone other in the list) to

    >>> calculate type for expression

    >>>

    >>> i i

    >>>

    >

    > LM> Joy doesn't have a type notation, so I'll invent one quickly: [t]

    > means

    > LM> a quoted type for some arbitrary type t, [[t]] means double quoted

    > and

    > LM> this is indeed the type required by ii. Many kinds of values have

    > the

    > LM> type [[t]] including for example [[3]] and [[4 +] 3 cons]

    >

    > This is just a part of type signature. One single line. It does not

    > mention relationship between input stack, output stack and stack on

    > entry of enclosed quotation.

     Well the full signature would be [[t]] -> t

    Though I have no idea what you mean by "stack on entry of enclosed

    quotation".

     >

    > LM> Languages like Clean and Haskell do have decidable type systems but

    > only

    > LM> because their language designers chose to limit the expressiveness

    > of

    > LM> the underlying untyped language.  For example, if the type system

    > didn't

    > LM> get in the way, you would be able to define a 'printf' type function

    > LM> where the types of the second and subsequent arguments are

    > determined by

    > LM> the first argument.

    >

    > BTW, so called existential types handle this as well without

    > sacrificing decidability.

     Hmmm, really?  Can you show me?

     >

    > LM> If you wanted to, you could similarly limit Joys expressiveness and

    > so

    > LM> define a decidable type system for it, but I dislike that approach.

    >

    > Well, I'd like to see your approach.

     I'm working on it :-)

    Louis.

    [Non-text portions of this message have been removed]