[Haskell-cafe] Looking for a paper [Dijkstra-Dot]

[Anthony Clayden]

>> On 6/5/20 7:05 AM, Anthony Clayden wrote:
>>* Hi Michael, I apologise if I'm being dumb, but that ewd.pdf is not a*
>>* 'publication' and is not by Dijkstra, right?*

> Sure.


>> *It's taking some of the ideas from Dijkstra's EWD1300, but misapplying*
>>* them to Haskell in a rather badly-informed way.*

> I wouldn't say so, for reasons explained below.

An undated pdf without even the authors names,
but using a respected author's name seems dodgy to me.
It's not "with E.W.Dijkstra" at all, indeed I'd say it's "against" him.
I think what they impute to EWD is wrong in fact and wrong in attitude,
for reasons explained below.


>>* After all, Haskell already has a 'Application Operator' spelled ($),*
>>* which is perfectly first-class and with which you can do the equational*
>>* reasoning (with lambdas) that the doco is talking about.*

> The thread that I was recalling (Language complexity & beginners) can be
found here,
>
> https://mail.haskell.org/pipermail/haskell-cafe/2016-February.txt

> and it started as a discussion about the use of ($) for function
> application. Namely, what should its type be?

Its type is :: (a -> b) -> a -> b; that's in the Haskell Report
and what you get at the GHCi prompt :t ($) -- at GHC 6.5 with no extensions on.

Also while we're at it Data.Function.& :: a -> (a -> b) -> b
-- reverse application, which'll do for the paper Ben suggested.

> Whatever you answer is going to be wrong.

That's a fine type for the purposes of the 'thought-dialogue'
-- which is not a language specification.
If GHC's type under the hood is polykinded/higher-ordered/typeRep'd/etc
yes that'll confuse beginners, but won't upset the 'thought'.

> The root of that problem is that ($) is itself a
> function, and you can't insist on using a function to apply function
> application without risk of severe injury. So the only way to even use
> ($) is via the true function application syntax, namely whitespace.

So that's what the authors of EWD.pdf do at the end of the piece,
so that they derive (.) by eta-reduction. It's bogus.

Also bogus their is putting '.' between the lambda and the bound variable.
WTF is that? You don't 'apply' lambda to a variable;
it's not a function; it's a binding mechanism.
Some syntaxes for lambda calculus put a dot _after_ the bound
variable, where Haskell uses ->.

To put it bluntly: the authors are blundering.


> But whitespace as function application syntax has its own problems.

EWD1300 has only a short section on 'Invisible operators'. Dijkstra
doesn't like them.

To expand his examples, in:

>    π + x sin(y)

The invisible space (juxtaposition) between x and sin means multiplication;
the invisible non-spaces within "sin" are not juxtaposition, they're
merely a multi-letter name;
the invisible non-space between "sin" and parens is function application.
(To be precise in C-family languages, it's the pair of parens: rand()
is niladic function rand applied to no arguments.)

Practical programming languages are limited to ASCII, so can't have
UTF-8 chars in names, so we'd have to spell π as "pi" -- which
includes another invisible non-space.

Then EWD1300 wants to put alternating operators with names, thusly:

>    pi + x * sin.y


> So we want something like ($), but we want it to be *syntax*,

Yes. EWD1300's syntax is that (presumably) what's lexed as a
(sequence-of) symbol
alternates with what's lexed as a name/sequence-of letter.
And there's precedence/associativity; and parens' only purpose is to override.

EWD1300 does not claim that what's between "pi" and + or between + and x
is function application. EWD1300 does not consider operator sections
or partial application of operators; only partial application of functions.
There's brief mention of 'lambda-abstraction' (partial application),
but no working of actual lambda expressions.

EWD1300 is not talking about Haskell's peculiar syntax at all.
Including not talking about lambda syntax.
And I'm sure he'd complain about the iffy use of parens in operator sections
-- they're not there merely to override precedence;
(5) === 5;  (pi) === pi;  (+) =/= +

> and it should take the place of " " rather than supplement it.
> That's the argument those guys (and the paper Ben suggested) are trying to make.

EWD1300 does not suggest there's function application between an
operator and its operands
-- although one could argue that's just as much juxtaposition.
Suggesting that for any other operator than ($) would be OK
and thereby deals with Haskell's operator sections.
But suggesting it for ($) leads to infinite regress.
Dijkstra (the real one) was smart enough to see that.

The pdf poses a bogus problem; direct consequence of the authors not
understanding EWD1300.


AntC
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20200607/6ae1a599/attachment.html>