local variables don't cause side effects 
Author Message
 local variables don't cause side effects

Quote:

> 2.  There is an imperative substrate that is not up to that level
>     Haskell core elements and extensions written in C.  External
>     libraries, system calls.

> 3.  We commonly dismiss that as out of bounds of the problem.

This is exactly the point: I don't see this as out-of-bounds.

I'd like to see an implementation of the Haskell run-time system,
written in Haskell, just as C run-time systems are written in C. With
the added bonus that the Haskell run-time is easier to verify :-)

I'd also like to have APIs that are functional, or where the side
effects are formally specified. I know that this would mean reworking
all libraries in the world, which isn't going to happen anytime soon... ;-)
Actually, it's impossible to even start writing such libraries because
there's no generally accepted formalism that captures precisely the
information that a caller must know about the side effects of a call,
and precisely leaves out what a caller should *not* know. (Actually I'm
not sure that such a formalism exists at all, generally accepted or not.)

Quote:
> 4.  A C implementation can be transformed into semantically
>     equivalent but more provable Haskell one, even though
>     imperative.

I don't think that this holds.

What I do think is that the problems that an imperative program poses to
a proof will be just transformed into its functional equivalent.

I also think that functional programs are easier to prove simply because
functional languages encourage many idioms that are easy to prove, and
discourage many idioms that are difficult to prove. (Real Programmers
can write fortran programs in any language... they just write a Fortran
program and have a translator to that other language *g*)

Regards,
Jo



Mon, 02 Jan 2006 14:35:13 GMT  
 local variables don't cause side effects

Quote:


>> 2.  There is an imperative substrate that is not up to that level
>>     Haskell core elements and extensions written in C.  External
>>     libraries, system calls.

>> 3.  We commonly dismiss that as out of bounds of the problem.

> This is exactly the point: I don't see this as out-of-bounds.

> I'd like to see an implementation of the Haskell run-time system,
> written in Haskell, just as C run-time systems are written in C. With
> the added bonus that the Haskell run-time is easier to verify :-)

Isn't GHC completely implemented in Haskell, as of version 5-something?

More importantly, though, isn't there a chicken-and-egg problem here?
Haskell didn't exist forever (and neither did C, for that matter), so
at some point there was a bootstrapping step.  Haskell-as-a-standard
may be "easy to verify", but Haskell-as-an-implementation, even one
written in standard Haskell, will always depend on the correctness of
the original non-Haskell implementation.

In fact, if you want to get really pathological, even the correctness
of that original implementation is dependent on far more than the
semantics of its implementation language (C, perhaps) -- it depends in
turn on *that* language's implementation's correctness, which depends
still on the system call implementations and thus the operating system
implementation (quite a leap of faith for *cough* some operating systems),
which probably invokes some kind of loop, because the operating system was
probably written in C, and beside the point, the whole thing depends on the
correctness of the *machine's* implementation, hardware-wise!

In *fact*, if you want to get *reeeeally* pathological, even the machine's
implementation depends on the correctness of our understanding of physical
principles and the way the world works, and ... etc.  I'm reminded of Carl
Sagan's quote, "In order to make an apple pie from scratch, you must first
create the universe."

So i guess we have to draw the line somewhere, huh? :)

William



Tue, 03 Jan 2006 01:17:05 GMT  
 local variables don't cause side effects
 > So i guess we have to draw the line somewhere, huh? :)

Well, there's some validity to that. At least that the correctness
ultimately depends on machine correctness (which is highly dubious,
given the lists of errata that Intel publishes...)

However, at least *one* of the holes can be plugged:

Quote:
> Haskell didn't exist forever (and neither did C, for that matter), so
> at some point there was a bootstrapping step.  Haskell-as-a-standard
> may be "easy to verify", but Haskell-as-an-implementation, even one
> written in standard Haskell, will always depend on the correctness of
> the original non-Haskell implementation.

This is not the case. If somebody writes a Haskell compiler that emits C
or machine code, you don't have to go back to the initial
implementation: it's enough to inspect the machine code generated by the
compiler when it compiles itself.
If you wish to reduce the task, you first build a compiler for a
sublanguage which is barely powerful enough to compile the full
compiler, have it compile itself to check the implementation, then run
the full compiler through it. (This can be done in more than one stage
if desired.)
A popular test for compiler correctness is to compile the compiler, then
use the compiler to compile itself; the original compiler and the
results of that compilation must be bitwise identical. It's nothing more
than a first quick test, but given that the compiler for the sublanguage
is stripped down exactly to those features that are useful for writing
compilers, code coverage is usually quite good.

In other words, the correctness of a compiler is not that of the weakest
link in the chain (which is a Good Thing, else we'd be writing compilers
from scratch all the time).

Regards,
Jo



Tue, 03 Jan 2006 01:50:47 GMT  
 local variables don't cause side effects

Quote:

> In Sisal this code looks something like this (can't remember the exact
> syntax),

>    initial
>       s = 0;
>       i = 0;
>    in while i <= n d0
>       new s = s + i;
>       new i = i + 1;
>    yields s

AFAIR, you must use 'old', not 'new':

s=old s+old i;
i=old i+1;

:)

--
Ivan Boldyrev

                               There are 256 symbols in English alphabet.



Thu, 05 Jan 2006 23:17:43 GMT  
 local variables don't cause side effects

Quote:

> The real question is: what limitations would a type system have to
> impose on programs in order for it to admit
> purely-functional-constructs-with-opaque-imperative-implementations
> without introducing potential deadlocks or nondeterminism?  (An open
> question, I think.)

Isn't "no object aliasing" enough? That is to say, there can only be one
client of any given memory address.

Lately that seems to me a very desirable property for a programming
language to have, although I don't know of any languages that do have
it.

Marshall



Sat, 07 Jan 2006 13:02:24 GMT  
 local variables don't cause side effects

:> The real question is: what limitations would a type system have to
:> impose on programs in order for it to admit
:> purely-functional-constructs-with-opaque-imperative-implementations
:> without introducing potential deadlocks or nondeterminism?

: Isn't "no object aliasing" enough? That is to say, there can only be one
: client of any given memory address. Lately that seems to me a very
: desirable property for a programming language to have, although I don't
: know of any languages that do have it.

Sounds a little like Clean's "uniqueness typing"? Does that fit your bill?

-Greg



Sat, 07 Jan 2006 13:18:43 GMT  
 local variables don't cause side effects

Quote:



> :> The real question is: what limitations would a type system have to
> :> impose on programs in order for it to admit
> :> purely-functional-constructs-with-opaque-imperative-implementations
> :> without introducing potential deadlocks or nondeterminism?

> : Isn't "no object aliasing" enough? That is to say, there can only be one
> : client of any given memory address. Lately that seems to me a very
> : desirable property for a programming language to have, although I don't
> : know of any languages that do have it.

> Sounds a little like Clean's "uniqueness typing"? Does that fit your bill?

I guess I'll have to check! :-)

Marshall



Mon, 09 Jan 2006 15:27:33 GMT  
 local variables don't cause side effects

Quote:

> Isn't "no object aliasing" enough? That is to say, there can only be one
> client of any given memory address.

> Lately that seems to me a very desirable property for a programming
> language to have, although I don't know of any languages that do have
> it.

Mercury has a comprehensive uniqueness system which can be used to support
this sort of thing.  This is how arrays and IO, for instance, are handled
in Mercury.  Have a look at www.mercury.cs.mu.oz.au

-- Ralph



Tue, 10 Jan 2006 09:57:34 GMT  
 
 [ 83 post ]  Go to page: [1] [2] [3] [4] [5] [6]

 Relevant Pages 
 

 
Powered by phpBB® Forum Software