On Nov 2, 2007, at 6:35 , apfelmus wrote:
during function evaluation. Then, we'd need a purity lemma that
states that any function not involving the type *World as in- and
output is indeed pure, which may be a bit tricky to prove in the
presence of higher-order functions and polymorphism.
On Fri, 2007-11-02 at 08:35 -0400, Brandon S. Allbery KF8NH wrote:
On Nov 2, 2007, at 6:35 , apfelmus wrote:
during function evaluation. Then, we'd need a purity lemma that
states that any function not involving the type *World as in- and
output is indeed pure, which may be a bit
Brandon S. Allbery KF8NH wrote:
apfelmus wrote:
during function evaluation. Then, we'd need a purity lemma that
states that any function not involving the type *World as in- and
output is indeed pure, which may be a bit tricky to prove in the
presence of higher-order functions and
On Nov 2, 2007, at 11:51 , Jonathan Cast wrote:
I will grant that hiding *World / RealWorld# inside IO is cleaner
from a practical standpoint, though. Just not from a semantic one.
On the contrary. GHC's IO newtype isn't an implementation of IO in
Haskell at all. It's an implementation in
Hello,
Just a bit of minor academic nitpicking...
Yeah. After all, the uniqueness constraint has a theory with an
excellent pedigree (IIUC linear logic, whose proof theory Clean uses
here, goes back at least to the 60s, and Wadler proposed linear types
for IO before anybody had heard of
Paul Hudak wrote:
loop, loop' :: *World - ((),*World)
loop w = loop w
loop' w = let (_,w') = print x w in loop' w'
both have denotation _|_ but are clearly different in terms of side effects.
One can certainly use an operational semantics such as bisimulation,
but you don't have
On Fri, 2007-11-02 at 11:56 -0400, Brandon S. Allbery KF8NH wrote:
On Nov 2, 2007, at 11:51 , Jonathan Cast wrote:
I will grant that hiding *World / RealWorld# inside IO is cleaner
from a practical standpoint, though. Just not from a semantic one.
On the contrary. GHC's IO newtype
On Fri, 2007-11-02 at 15:43 -0400, Jeff Polakow wrote:
Hello,
Just a bit of minor academic nitpicking...
Yeah. After all, the uniqueness constraint has a theory with
an
excellent pedigree (IIUC linear logic, whose proof theory Clean
uses
here, goes back at least to
