Reviews for “Purely Functional Structured Programming”

—————————- REVIEW 1 ————————–

PAPER: 11

TITLE: Purely functional structured programming

 

OVERALL RATING: -2 (reject)

REVIEWER’S CONFIDENCE: 4 (expert)

 

The author proposes a way of combining “purely functional” programming

and “structured” programming. The term “purely functional” is used in

the conventional sense. “Structured” programming means imperative

programming with assignable variables and blocks such as while loops,

conditional statements etc.

 

The main idea of the paper is to add assignable variables to a

functional language, in a different way from the established Haskell

approach of using a monad. The technical idea proposed in the paper is

“linear scope”, and it is explained in the setting of the author’s

language Babel-17; actually in a cut-down version called Mini

Babel-17. A nice feature of the paper is that an interpreter for Mini

Babel-17 is available on the web, and this enables the examples in the

paper (and others) to be tested.

 

Here is the key idea, as I understand it. Variables are introduced

with what looks rather like an ML-style let-binding, e.g. val x = 1. A

variable can be updated by an assignment like x = x + 1, etc. I think

what is going on here is that the initial val declaration introduces

an ML-style reference cell; subsequent occurrences of x are implicitly

dereferenced unless they are on the left hand side of an

assignment. So, because of the implicit dereferences, it is not

possible to use the reference cell itself as a value.

 

There is a further refinement, which justifies the statement that we

still have purely functional programming. The section of code within

which a variable such as x can be referred to, with the implicit

dereference, is called the “linear scope” of x; it is a subset of the

standard lexical scope of x. But the linear scope does not extend into

lambda-expressions within the lexical scope. This means that a

function cannot have behaviour that depends on a reference cell

defined outside the function. It is possible for a function to create

reference cells internally, but because the cell is not available as a

first-class value, these internal reference cells cannot escape.

 

The idea that a function can use reference cells internally but remain

a true function (in the sense of referential transparency) is not new,

I think; for example it can be found informally in Section 8.2 of “ML

for the Working Programmer”.

 

The paper presents a few examples, and gives what it calls an

operational semantics of Mini Babel-17; what is actually presented is

the source code, in Standard ML, of an interpreter for Mini Babel-17.

 

The author claims that this integration of structured and purely

functional programming is an attractive alternative to Haskell’s

approach of using a monad to encapsulate mutable state.

 

So, that’s my understanding of the technical content. Now for my

assessment.

 

I am not sure how original the idea is in a conceptual sense. It is

interesting as part of a complete language design. But I don’t think

there is enough here for an ESOP paper. My summary above is quite

short but I think it captures the whole of the paper; I don’t think it

would be possible to summarise a typical ESOP paper so briefly. The

paper itself is fairly short, indicating that the technical content is

rather light.

 

The operational semantics doesn’t have the usual form for papers in

this area, i.e. a reduction relation defined by inference rules.

 

The paper doesn’t present any technical results. What would I expect

to see? My summary above suggests that Mini Babel-17 can be translated

into ML, so one possibility would be to present a translation; this

could serve directly as a semantics or could complement a more formal

operational semantics. I also mentioned above that a key idea of the

paper seems to be that mutable references can be used, without

producing impure functions, if references are always local to

functions and cannot escape. It should be possible to prove a result

along those lines, although I am not sure how original it would be;

maybe it is just folklore (as suggested by the reference to Paulson’s

book).

 

It would also be interesting to give a more thorough comparison with

the Haskell approach.

 

The paper is well written and quite easy to follow. I think there is a

small problem with the final example on page 11. The text states that

the function returns a list, but the function body seems to return an

integer.

 

As I said earlier, the availability of a working interpreter for the

language is admirable and was very helpful in understanding the

examples.

 

In summary, I am not sure there is an ESOP paper here even if the

technical details are formalised and some results proved. But I could

imagine this material appearing as part of a longer paper on the

design of Babel-17.

 

I do not have any specific questions for the rebuttal phase.

 

 

 

—————————- REVIEW 2 ————————–

PAPER: 11

TITLE: Purely functional structured programming

 

OVERALL RATING: -3 (strong reject)

REVIEWER’S CONFIDENCE: 4 (expert)

 

This paper claims to “make structured programming in integral part of

purely functional programming”.  What it actually does, as far as I

can tell, is to identify an idiom that one could follow in an ML

language, or in Haskell with a state monad, in which one refrains from

mutating a reference cell except top-level linearly sequenced control

flow (but not in the arguments of a binary operator, for example).  It

does this with a notion of “linear scope”, and the author correctly

writes “Maybe the rules of linear scope sound confusing at first”.

The simple relation between the syntactic structure of programs and

conventional static scoping is not something to be given up lightly.

 

If there really is something here, then perhaps it could be better

captured by identifying whatever reasoning principles are enabled by

that idiom.

 

 

 

—————————- REVIEW 3 ————————–

PAPER: 11

TITLE: Purely functional structured programming

 

OVERALL RATING: -2 (reject)

REVIEWER’S CONFIDENCE: 4 (expert)

 

The paper has serious flaws in the following three main categories.

 

1. Motivation and relevance

 

We read in the introduction that purely functional programming (PFP) is

becoming popular because pure expressions lack ‘side-effects’, mutable state,

etc, and are therefore ‘straightforward’ to turn into parallel executable

code. That PFP is popular only within niche communities such as theorem

proving. That today’s popular programming paradigm is structured programming

(SP), defined simply as programming with if-branches and while-loops

[imperative programming, one guesses]. That PFP rejects SP because it smells

of side effects, destructive updates, and mutable state.

 

Linear scope [to be discussed in point 2 of this review] is proposed as a way

to marry PFP and SP. PFP would become more mainstream if it looked more like

SP, and linear scope is the paper’s proposed means to achieve this goal.  The

toy language Mini Babel-17 is introduced to illustrate the workings of linear

scope.

 

Let’s begin by pointing out that ‘side-effects’ are undesirable in any

language. ‘Effects’, on the contrary, are not only desirable but unavoidable.

The growing popularity of purely functional programming languages such as

Haskell are due to the principled integration of purity and effects which yet

remain separated *by type*, helping compilers optimise pure and effectful

code and exploit their suitability for parallelism accordingly—a task

that’s anything but ‘straightforward’. I emphasise the word *type* because,

as we learn on Section 3, linear scope is presented in a dynamically typed

example-language of which we are not given the type expressions nor the type

rules, only informal descriptions of behaviour like that at the end of page

7. If linear scope and mini-Babel-17 were what we want for PFP, the reader

cannot tell if they’d be suitable for parallelism which was the main reason

for propping PFP. Wouldn’t the dependency of a variable on the place on which

it is defined complicate optimisations? [see below] When introducing a

feature into a language, one must study the consequences on the rest of the

language.

 

Impure functional languages exist, and they have imperative features. As the

author points out, ML has a while keyword that, he complains, is rarely

used. Perhaps the reason is that one can program alternatively, and much

better, without it. The purpose of monads is not only to deal with effects.

And monads should be learnt for many reasons. I don’t understand why we

should have to avoid knowing them, this purporting to be one of the

advantages of using linear scoping, as stated in the abstract.

 

(Also in the abstract: ‘a second advantage is that professional purely

functional programmers can often avoid hard to read functional code by using

structured programming syntax that is often easier to parse mentally’. I take

that professional functional programmers can parse mentally functional code

much better than imperative code. The ‘benefit’ would be for imperative

programmers to think they’re still doing Pascal.)

 

The most popular programming paradigm today is not SP but OOP, of which

Scala, a language cited by the author, is an example.

 

PFP does not reject SP. Functional programs have structure, only that the

notion of computation is based on function application. If-branches are common

in PFP and defining while-loops in a pure setting, even without monads, is a

textbook exercise. The author knows this for he provides a ‘semantics’ of his

mini-Babel language in ML.

 

Whether PFP becomes more mainstream or not will depend, among other things,

on its advantages and on various other social issues. But the point of PFP is

to liberate programming from the Von Neumann (imperative) style. Going back

to it would not benefit ‘professional purely functional programmers’ who

don’t need it. It wouldn’t benefit imperative or OO programmers wishing to

learn PFP either. They’d have the impression that they’re still programming

imperatively. Types, first-class functions, higher-order functions, powerful

abstractions, computation by means of function application and composition.

That’s what PFP is about.

 

 

2. Contribution

 

Linear scope is the rediscovery that a restricted form of mutable variable

can be obtained by nesting scopes or variable renaming appearing on l-value

position. Take the last example in Section 2:

 

(x : Int) => { var y = x*x

val h = () => y

y = y * y

h() * y }

 

This function implements \x.x^8 but, according to the author, with

‘shadowing’ it should implement \x.x^6. But shadowing involves a

re-declaration.  Where’s the redeclaration of ‘y’? Are we to take ‘y = y*y’

as a re-declaration? Despite the missing ‘var’ keyword, we should, according

to the author. A new ‘y’ enters the picture but h()’s ‘y’ refers to the one

defined before the function. Thus, the position of a function matters, move h

down and it’s meaning changes, a side effect.

 

However, use renaming and we get what we want without side-effects:

 

(x : Int) => { val y = x*x

val h = () => y

val z = y * y

h() * z }

 

In fact, the author could argue at this point that he’s not after mutable

variables, in which case h’s body would refer to the ‘y’ in scope, the one

just mutated, delivering x^8 as well. Mutable and immutable variables are

separated in Scala for very good reasons—one taking us back to the

separation between purity and effects code touted in the paper’s

introduction. ‘Successfully married’, says the abstract, indeed, thanks to

separation. Global scope for global variables means they can be placed

anywhere in the code. Being immutable, they stand for values and expressions

using them are still pure.

 

Could linear scope be implemented by means of renaming of variables as in the

above example. The author should address this question.

 

Section 2 is confused on the sales pitch. Shadowing is *not* wrong in PFP,

it’s very well supported, and variables are not state, for a state is meant

to mutate. The main issue is not shadowing or programming with if-branches,

or while-loops.  Linear scope is concerned only with assignment, in giving

the impression or mutation by means of nesting new scopes.  But, as the

purported semantics in Section 6 show, the meaning of linear scope requires

mutable environments (middle of page 8). One can simulate assignment by

moving the change of state (variable renaming) to the environment.

 

That ‘shadowing is purely functional’ (Sec 3, p3) is well known since the

lambda-calculus (e.g., \x.\x.x). What linear scope is doing is not your purely

functional shadowing. The paper’s imperative semantics also illustrate that.

 

 

3. Written style

 

Despite it’s intended tutorial style, the paper is poorly written regarding

structure, aims, contributions, etc. Most of it is devoted to the syntax and

so-called semantics of Mini Babel 17, after a cursory description (via

examples) of linear scope which is the main contribution. Related work is

poorly discussed. Describing the semantics of linear scope monadically would

be a good exercise. Also, the rough corners should be addressed in more

detail: the interaction between a linear scope and regular scope, whence

those ‘x = x’ strange declarations (Sec.5, middle paragraph) and the seeming

non-determinism (list of values, Sec.6, page 7), etc.

 

 

 

—————————- REVIEW 4 ————————–

PAPER: 11

TITLE: Purely functional structured programming

 

OVERALL RATING: -2 (reject)

REVIEWER’S CONFIDENCE: 3 (high)

 

The paper presents the initial design of a programming language combining features of pure functional languages and imperative programming languages. After introducing the notion of linear scope, a mechanism which limits the imperative use of variables, an interpreter for a small core language is presented.

 

I like the general intent of the paper, namely to enable the use of familiar imperative

constructs within a functional languages in the syntax that an imperative programmer is familiar with.

However, I have several reservations on presentation and contents.

 

I found the discussion on shadowing quite confusing. I would have expected the discussion to concentrate on whether a variable can be used in an imperative way or not, rather than on the mechanism with which a variable already in scope can be shadowed by another variable declaration with the same name. I would keep shadowing as a side comment, that variables can be re-bound and transformed from non-linear to linear.

For terminology, I would rather use “imperative scope” than “linear scope”, also to avoid possible confusion with the same notion used in the context of linear types.

 

When reading the paper, I felt that it stopped suddenly at the end of section 7, leaving the reader hanging.

I would have expected some form of evaluation of the design choices, and a more in-depth analysis

of the properties of the language. For example, I would expect that some sort of equational reasoning

is supported by the language, since the imperative features seem encapsulated inside blocks of instructions.

 

In terms of presentation, I was initially confused by the fact that the interpreter is written

using mutable state inside linear environments, and it took me a while to realise that eval_e can in

fact modify the environment despite its type. While I liked the concreteness of presenting the

semantics as an interpreter, I think that some separate formalisation of linear scope would help the reader

grasp the concept without having to understand the details of the interpreter. Also, I feel that the

well-formedness criterion on p.10 could be made more readable by presenting it as an ordinary

type system with inference rules.

 

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s


%d bloggers like this: