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

[Keean Schupke]

Have you looked at Linear Aliasing, the type system used for TAL (typed 
assembly
language)... one would assume that if a C compiler which compiles to TAL 
were
produces, then you could proove purity?

Keean.

Conor McBride wrote:

> 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