[Haskell-cafe] Pure extremism (was: Re: Why?)

On Fri, Dec 11, 2009 at 7:07 PM, Jason Dusek wrote:

2009/12/11 Luke Palmer :

...

The idea being that any code that is pure could be evaluated anywhere with a very simple interpreter. If you have pure code, you can trace it back and evaluate it in a sandbox where you don't need a C runtime, a linker, or really anything but the simplest substitution engine. *All* effects bubble their way up to the top level, so that we know from the type signature of a value the machinery we will need to run it.

 This sounds good but there is something puzzling about it.  Where do we draw the line between "machinery" and "packages"?  The types don't tell us what libraries we need.

I don't follow this. Do you mean external libraries, such as "the library used to execute an IO type"? That makes sense to me, though in that case the types do tell. Or you might mean what *haskell* libraries does a piece of code depend on? To address that, note that I consider a statement like: import Control.Monad.State As a form of impurity in a sense (it is hard to say what I consider it, actually, but I think it inhibits reasoning and verification). What version are you importing? From where are you importing it ; where is it defined? These things depend on the compiler environment, which means that the meaning of a piece of code depends on who is compiling it. I have brainstormed solutions to this problem while thinking about my (currently on hold or dead) Udon project: http://lukepalmer.wordpress.com/2008/11/19/udon-sketch-2/ . But it is just a brainstorm, nothing I would sign in blood. I'd love it if more people were thinking about these kinds of problems (Any papers you well-read folks know about?)

They don't tell us how much RAM/CPU we need, either.

And these! My ideas for these are now firmly beyond Haskell and way out in the ill-defined vaporware space. I discuss in abstract the idea of distinguishing the performance semantics from the denotation of a piece of code here: http://lukepalmer.wordpress.com/2009/06/12/the-role-of-a-core-calculus/ . Brainstorm disclaimer applies, and I want to see more research! (Papers?)

...

Pure functional code as the minimal essence of pure computation -- everything else an EDSL.

 Partial or total code?

When the state of the art catches up, total for sure. Why reason with DCPOs when you can reason with the mathematical objects themselves? But when you require functions to be total, you end up needing to prove a lot more about them just to convince the compiler that they will terminate. Functional proof assistants are a wonderful area of research, but are still very early and it is frickin' hard to prove stuff about code. My belief is that time is all that is necessary here -- the research will continue and it will become easier and easier to prove properties about code (probably never completely automatic, but someday I hope to "handwave the essence" of a proof and have the computer fill in the bullshit details). But when it's easy enough, then partiality is definitely an "effect" to be modeled as well. It has the advantage, unlike most effects, that given a good model, you can prove your way out of it. I.e. write a function with a partiality effect, then elsewhere prove that it actually is total so you can drop the effect. I seem to recall a proof-of-concept of this idea for Coq. There are many levels to purity, and I think as research progresses we will gradually be able to go to the stricter levels while remaining productive. It gives me comfort to see a long road ahead -- I don't like to see perfect languages, because that's just me seeing my own ignorance :-) Luke