# What 'purity' in functional languages means

## Massimo Dentico — 2001-12-11 02:09:42

    I think this message from Mark William Hopkins, posted several years

    ago to comp.lang.functional, could be of interest for you:

        "What Is Purity? The Synthesis Of Imperative And Functional

        Programming Languages Via The Infinitary Lambda Calculus"

        - http://www.uwm.edu/~whopkins/functional/purity.txt

    and other related material here:

        - http://www.uwm.edu/~whopkins/

        * Loop Invariants In The Infinitary Lambda Calculus

        * Applicative And Normal Order Evaluation In The Lambda Calculus:

          Formal Definition And Derivation Of Evaluation Machines

        * JOLT -- The Purely Functional Imperative Programming Language

        * The C-BC Programming Language

        * Infinite Lambda Calculus, SEQCD & Imperative Functional Languages

    See also a recent thread on comp.lang.ml:

        "Future of functional languages is ..." (1st message 16/10/2001, by X)

    a replay from François-René Rideau to a message from Mark William Hopkins

    (in which Hopkins reiterates what you can find on his web site cited above)

    could be also of interest:

    ----------------------------------------------------------------------------

    whopkins@... (Mark William Hopkins) writes:

       > Indeed, if one takes the equivalence

      >

      > while (e) s  =   if (e)  (s; while (e) s)

      >

      > then one is forced to the conclusion that a loop must be

      > represented by an operator which resides in an INFINITARY LANGUAGE;

     Only if you want to manipulate *trees*. It's still *finitary graphs*.

    Besides, as soon as you'll have sharing, in e.g. call-by-need semantics,

    or an optimal reduction strategy, or a non-deterministic setting,

    or side-effects, or graph-reduction machines, or whatever,

    you'll see that *graphs*, not trees, are the right way to look at things.

       > [...] A second most straightforward extension of the Lambda Calculus

      > consists of infinite terms whose parse trees may have an infinite

      > number of distinct subtrees, but whose constituent structure is

      > specifiable by a finite set of syntatic definitions of the form

     Looks like a very contrived way of saying "finitary graphs".

    Yours freely,

    François-René Rideau

    [snipped entire signature]

    ----------------------------------------------------------------------------

    --

    Massimo Dentico

## Louis Madon — 2001-12-11 21:58:28

    On Tuesday, December 11, 2001, at 12:09  PM, Massimo Dentico wrote:

     > I think this message from Mark William Hopkins, posted several years

    > ago to comp.lang.functional, could be of interest for you:

    >

    >     "What Is Purity? The Synthesis Of Imperative And Functional

    >     Programming Languages Via The Infinitary Lambda Calculus"

    >

    >     - http://www.uwm.edu/~whopkins/functional/purity.txt

     Interesting Post!  I had not considered that assignment could be seen as

    "pure" in the absence of loops. I'll have to read more of his stuff when

    I get a chance.

    Louis.

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