[Haskell-cafe] Re: Top Level TWI's again was Re: [Haskell] Re: Parameterized Show

[Conor McBride]

Keean Schupke wrote:
> Can a C function be pure? I guess it can... The trouble is you cannot 
> proove its
> pure?

A C function might have no observable side effects, even if it operates
destructively over its own private data structures. It mightn't be too
hard to establish a sound test for this sort of purity (the one we have
already is sound; it always says no; some improvement may be possible).
Clearly completeness is too much to hope for.

> But - why would you want to use a pure C function. The chances of any 
> useful C library function being pure are slim - and the performance of
 > GHC in some of the benchmarks shows that there is hardly any speed
 > advantage (for a pure function)...

What about the other benchmarks? There are plenty of operations where
programmers can do a neater job than compilers at deciding that a given
data structure is known only to one consumer and can therefore be
manipulated destructively, recycled aggressively etc. I know modern
recycling is marvellous, but reduced consumption is better, isn't it?

The C functions I'm thinking of are the output from Hofmann &co's
LFPL compiler: pure *linear* functional programs which run in the heap
they were born with. There are potential speed gains too: the knowledge
that you don't need to keep the original input means that you can
operate deep inside it in constant time, at the cost of maintaining
some extra pointers. (Does anybody know of a linear type system which
allows this? Basically, a list xs contains a pointer to its tail, so
holding a tail-pointer for xs would be a duplicate reference: problem.
But perhaps it's ok for the holder of xs also to hold its tail-pointer.)
This stuff isn't really my thing, but I'm an interested spectator.

These programs aren't funny interactive hard-drive-formatting things,
so they're probably irrelevant to this particular argument. Nonetheless,
they're hard to write efficiently in functional programming languages as
we know them. They're hard to write safely in C, but sometimes we just
get fed up with knowing useful stuff that we can't tell the compiler.

Is uniqueness worth a second look?

Conor

--
http://www.cs.rhul.ac.uk/~conor                      for one more week