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

## Serguey Zefirov — 2001-12-10 13:37:10

    Hello e1_t,

    суббота, 8 декабря 2001 г., you wrote:

    e> That reasoning could also be used for impure functional languages and

    e> in fact imperative languages as well.

    e> What happens if you write a function that uses 'get'? Does that

    e> function also take a hidden argument (afterall it does cause a side-

    e> effect)? How does the compiler/interpreter know which function takes

    e> hidden arguments and which one doesn't?

    In a current state Joy isn't pure functional. This can be fixed by a

    simple hack - introduce a type World.

    getsome ( World -- World something)

    If you protect type World from being duplicated and dropped, you get a

    pure functional language, like, say, Concurrent Clean.

    I've not thought yet the way that could be done with something like

    Haskell Monads.

    e> The question of whether the compiler needs to know that is in fact

    e> relevant - functional languages are viewed as better then imperative

    e> languages simply because they can be implemented to utilize

    e> equational reasoning (which can ultimatly be used to optimize an

    e> abstract and inefficient program that is easily readable by a human,

    e> i.e. a math formula, into an efficient form that may be harder to

    e> comprehend) and because they are better suited to parallel

    e> programming (the order of evaluation of pure, side-effect free

    e> functions is irrelevant therefore they can be executed in parallel).

    e> One of my current projects is Metafor, a functional language based on

    e> Forth that can be implemented as an extension to Forth. I was

    e> surprised when I came accross Joy as the syntax is very similar. I'm

    e> still designing Metafor and haven't even started implementing it yet

    e> simply because I'm still evaluating the potential flaws and one of

    e> the biggest is the way side-effects are handled in the current

    e> design. In fact I was hoping someone would respond the way you did

    e> because my reasoning behind hiding side-effects in Metafor is similar

    e> (although goes into more detail).

    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

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

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

    This somewhat prevents one from reasoning about programs, especially,

    their parts.

    Best regards,

    Serguey Zefirov               mailto:sz@...

## Billy Tanksley — 2001-12-10 17:25:28

    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.

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

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

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

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

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

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

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

    could.)

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

    >calculate type for expression

    >i i

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

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

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

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

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

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

    that's true for your question in ANY language.

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

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

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

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

    >their parts.

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

    additionally, programmers have been reasoning about Forth programs for three

    decades.

     >Serguey Zefirov               mailto:sz@...

     -Billy

## Louis Madon — 2001-12-11 00:13:54

    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

    >

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

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

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

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

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

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

    >

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

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

    itself.

    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

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

    principle types.

    The hard part in designing a type system however, is to get it to

    guarantee that one or more formal properties will hold for all

    well-typed programs (eg. "no execution can result in an operation being

    applied to a value it is not intended to handle", "no array accesses

    will be out of bounds", etc).  Within these constraints, you could argue

    that some type systems (not languages!) don't produce principle types -

    this is essentially the same as saying those type systems are

    undecidable.

    Kris De Volder has written an interesting thesis called "Type Oriented

    Logic Programs"[*] in which he questions the obsession that many

    language designers have with keeping their type systems decidable.

    Here's a quote from his introduction:

    "We will show that undecidability and ambiguity of type systems is not

    by definition

    a bad thing. Ensuring unambiguity and decidability of typing imposes

    strong restrictions on

    the expressiveness of the type system. When abandoning the restrictions,

    the expressiveness

    of the type system can be increased to the level of a real programming

    language, thus lifting

    its capability for active manipulation of static types to an entirely

    new level. We will show

    by means of examples that this extra expressiveness does have very

    useful and interesting

    applications."

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

    because their language designers chose to limit the expressiveness of

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

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

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

    the first argument.

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

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

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

    > their parts.

     I really have to disagree.

    Louis.

    {*] "Type Oriented Logic Programs"

    Kris De Volder

    http://www.cs.ubc.ca/~kdvolder/publications/phd-summary.htm

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