Is Strictness a Hack?
Adrian Hey
Recent assertions that laziness (non strictness) is a hack have surprised
me, because I'd always felt the same way about strict FPLS.
A strict FPL would presumably allow a function definition like this..
ite b t f = if b then t else f
but in reality I suspect that..
ite b t f /= if then t else f
because, according to strict semantics..
ite True t _|_ = _|_
but in any (sane implementation of) strict FPL..
if True then t else _|_ = t
So the if-then-else doesn't look like a proper expression at all
to me. It's more like an imperative control constuct.
How do advocates of strict semantics in an FPL deal with this kind
of wierdness?
Maybe they don't they deal with it at all, in which case it seems
to me that strictness must be a hack :-)
Regards
--
Adrian Hey
Neelakantan Krishnaswami
>
> Recent assertions that laziness (non strictness) is a hack have
> surprised me, because I'd always felt the same way about strict
> FPLS.
>
> A strict FPL would presumably allow a function definition like this..
> ite b t f = if b then t else f
> but in reality I suspect that..
> ite b t f /= if then t else f
> because, according to strict semantics..
> ite True t _|_ = _|_
> but in any (sane implementation of) strict FPL..
> if True then t else _|_ = t
>
> So the if-then-else doesn't look like a proper expression at all to
> me. It's more like an imperative control constuct.
Bingo! The reason that strict "functional" languages like Scheme and
SML/NJ are so cool is because they are actually the most expressive
*imperative* languages around. The combination of call/cc and mutable
state permits a programmer to efficiently encode any effect that can
be expressed in terms of a monad.
I think, but haven't proven, that any effect that can be expressed as
an arrow can be explained in terms of stack inspection -- looking at
the pieces of a continuation. This would let you to turn aspect
oriented programming into a library!
> How do advocates of strict semantics in an FPL deal with this kind
> of wierdness?
By recognizing that nontermination is, indeed, an effect. So as a
matter of style, we write pure programs that we can easily prove
terminate -- folds, combined with non-recursive values, are extremely
helpful here -- and then carefully use side-effects to go beyond that
can break termination for things like recursive values, mutable state,
and so on.
> Maybe they don't they deal with it at all, in which case it seems
> to me that strictness must be a hack :-)
No, we are just programming in a dynamically-effected imperative
language. It's indeed unfortunate that we have to rely on programmer
discipline to program properly, but we may hope that this will not
always be the case. :)
--
Neel Krishnaswami
ne...@alum.mit.edu
Ken Shan
> I think, but haven't proven, that any effect that can be expressed as
> an arrow can be explained in terms of stack inspection -- looking at
> the pieces of a continuation. This would let you to turn aspect
> oriented programming into a library!
I certainly don't know whether it makes a difference that you are
considering here not just any effect that can be expressed as a monad
but any effect that can be expressed as an arrow, but in case you are
not aware of Filinski's PhD thesis work, you should be:
@STRING{org_cmu_cs = "School of Computer Science, Carnegie Mellon University" }
@STRING{techreport = "Tech.\ Rep." }
@STRING{proc_popl_1 = "{POPL} '" }
@STRING{proc_popl_2 = ": Conference Record of the Annual {ACM} Symposium on Principles of Programming Languages" }
@STRING{pub_acm = "{ACM} {P}ress" }
@STRING{pub_acm_addr = "{N}ew {Y}ork" }
@PhDThesis{ filinski-controlling,
author = "Andrzej Filinski",
title = "Controlling Effects",
school = org_cmu_cs,
year = 1996,
note = "Also as " # techreport # " CMU-CS-96-119",
url = "http://www.diku.dk/~andrzej/papers/CE-abstract.html
http://www.diku.dk/~andrzej/papers/CE.dvi.gz
http://www.diku.dk/~andrzej/papers/CE.ps.gz
http://www.cs.cmu.edu/People/clamen/reports/1996.html
ftp://reports.adm.cs.cmu.edu/usr/anon/1996/CMU-CS-96-119.ps",
abstract = "Many computational effects, such as exceptions,
state, or nondeterminism, can be conveniently
specified in terms of \emph{monads}. We investigate
a technique for uniformly adding arbitrary
such effects to ML-like languages, without
requiring any structural changes to the programs
themselves. Instead, we use \emph{monadic
reflection}, a new language construct for explicitly
converting back and forth between representations of
effects as \emph{behavior} and as \emph{data}.\par
Using monadic reflection to characterize concisely
all effects expressible with a given monad, we
can give a precise meaning to the notion of
\emph{simulating} one effect by another, more general
one. We isolate a simple condition allowing such a
simulation, and in particular show that any monadic
effect can be simulated by a continuation monad. In
other words, under relatively mild assumptions on
the base language (allowing formation of a suitably
large answer type), control becomes a \emph{universal
effect}.\par Concluding the development, we show
that this universal effect can itself be explicitly
implemented in terms of only standard first-class
continuations (\emph{call/cc}) and a piece of global
state. This means that we can specify an effect such
as nondeterminism abstractly, in terms of result
lists, then directly obtain from this description
a nondeterministic-choice operator performing
imperatively-implemented backtracking. We include
a full realization of the general construction
in Standard ML of New Jersey, and give several
programming examples."
}
@InProceedings{ filinski-layered,
author = "Andrzej Filinski",
title = "Representing Layered Monads",
pages = "175--188",
crossref = "popl1999",
url = "http://www.diku.dk/~andrzej/papers/RLM-abstract.html
http://www.diku.dk/~andrzej/papers/RLM.dvi
http://www.diku.dk/~andrzej/papers/RLM.ps.gz",
subject = "{\bf D.3.2} Software, PROGRAMMING LANGUAGES, Language
Classifications. {\bf F.4.1} Theory of Computation,
MATHEMATICAL LOGIC AND FORMAL LANGUAGES, Mathematical
Logic. {\bf F.3.2} Theory of Computation, LOGICS
AND MEANINGS OF PROGRAMS, Semantics of Programming
Languages. {\bf D.3.1} Software, PROGRAMMING
LANGUAGES, Formal Definitions and Theory.",
abstract = "There has already been considerable research on
constructing modular, monad-based specifications
of computational effects (state, exceptions,
nondeterminism, etc.) in programming languages. We
present a simple framework in this tradition,
based on a Church-style effect-typing system
for an ML-like language. The semantics of this
language is formally defined by a series of monadic
translations, each one expanding away a layer of
effects. Such a layered specification is easy to
reason about, but its \emph{direct} implementation
(whether by parameterized interpretation or by actual
translation) is often prohibitively inefficient.\par
By exploiting deeper semantic properties of monads,
however, it is also possible to derive a vastly
more efficient implementation: we show that each
layer of effects can be uniformly simulated by
continuation-passing, and further that multiple such
layers can themselves be simulated by a standard
semantics for call/cc and mutable state. Thus, even
multi-effect programs can be executed in Scheme or
SML/NJ at full native speed, generalizing an earlier
single-effect result. As an example, we show how a
simple resumption-based semantics of concurrency
allows us to directly simulate a shared-state
program across all possible dynamic interleavings of
execution threads."
}
@Proceedings{ popl1999,
key = "{\relax ACM}",
title = proc_popl_1 # "99" # proc_popl_2,
booktitle = proc_popl_1 # "99" # proc_popl_2,
address = pub_acm_addr,
publisher = pub_acm,
year = 1999,
issn = "0730-8566",
location = "San Antonio"
}
--
Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig
Consing onto proper lists since 1989.
Neelakantan Krishnaswami
> Neelakantan Krishnaswami <ne...@alum.mit.edu> wrote in article <slrnbdc1ts...@h00045a4799d6.ne.client2.attbi.com> in comp.lang.functional:
> > I think, but haven't proven, that any effect that can be expressed as
> > an arrow can be explained in terms of stack inspection -- looking at
> > the pieces of a continuation. This would let you to turn aspect
> > oriented programming into a library!
>
> I certainly don't know whether it makes a difference that you are
> considering here not just any effect that can be expressed as a
> monad but any effect that can be expressed as an arrow, but in case
> you are not aware of Filinski's PhD thesis work, you should be:
It's Filinski's thesis that led me down this line of speculation. He
showed that any monadic effect can be expressed as call/cc plus a
mutable state, and that is basically what convinced me that strict
languages were a fundamentally good idea, and not just a hack. Since
you can implement first-class continuations at a relatively small
performance cost, this means that his encodings let you get any kind
of monadic effect very efficiently.
Where arrows come in is that they basically turn the second argument
of the monadic "bind" operation from a first class function into an
abstract data type, which means you can supply operations on them. So
the continuation argument in CPS code, which can be expressed as a
monad, can be "arrow-ized" so that the continuation becomes an ADT,
and you can do stack inspection. This is basically the source of my
suspicion about the relationship between arrows and stack inspection.
Actually proving the relationship would require some math that I am
not yet competent to do, which is why I start grad school this
fall. :)
--
Neel Krishnaswami
ne...@alum.mit.edu
Tim Sweeney
type-theoretically equal. In its absence, proofs-as-propositions
works, and lazy evaluation is observationally equivalant to strict
evaluation. So, clearly, _|_ is the point of controversy, and not
lazy vs strict.
It would be good for future languages that aspire to be pure to allow
a clear distinction between expressions that admit _|_ and expressions
that disallow it. The former can be used in propositional proofs,
proof-carrying-code, and other metamathematical formulations
regardless of evaluation strategy, while the later are necessary for
many mainstream programming tasks.
Effects are not monads and _|_ is not an effect. We should view these
concepts as if we have a languages with a base axiom system that
doesn't admit _|_ or effects. And then we have additional axioms that
we can add in to the evaluation of terms in particular contexts, to
capture the additional evaluation semantics.
Adding axioms can sometimes make the type theoretic equality
relationship more specific (for example, in allowing the distinction
of terms which differ only in effects not visible under the base
axioms), and sometimes narrow it, for example by collapsing it into a
single term _|_.
Ken Shan
> In the presence of _|_, all types are inhabited and all values are
> type-theoretically equal. In its absence, proofs-as-propositions
> works, and lazy evaluation is observationally equivalant to strict
> evaluation. So, clearly, _|_ is the point of controversy, and not
> lazy vs strict.
I *think* I understand and agree with you when you say that the point of
controversy is _|_ rather than lazy vs strict, but I am unclear why "all
values are type-theoretically equal" in the presence of _|_. Can you
please elaborate?
> It would be good for future languages that aspire to be pure to allow
> a clear distinction between expressions that admit _|_ and expressions
> that disallow it. The former can be used in propositional proofs,
> proof-carrying-code, and other metamathematical formulations
> regardless of evaluation strategy, while the later are necessary for
> many mainstream programming tasks.
Do you mean to exchange "former" and "latter" in the second sentence
above? Assuming so, I believe Daniel Wang and I both agree with you.
I also believe Daniel Wang and I both agree with the rest of your post,
except there seems to be a difference in terminology definition when you
say that
> Effects are not monads and _|_ is not an effect.
It is quite clear to me that _|_ is a monad (namely the monad taking
each type x to x + unit). The term "effect" is rather vague, and
while I am happy to take monads to be a technical approximation to the
intuitive notion, I am also happy to entertain alternative definitions.
Can you explain yours a bit more?
Tim Sweeney
> controversy is _|_ rather than lazy vs strict, but I am unclear why "all
> values are type-theoretically equal" in the presence of _|_. Can you
> please elaborate?
This isn't something you run into when writing and running programs in
languages like Haskell. Rather, it comes up when trying to prove
properties about them in a manner independent of the evaluation rules.
If a language admits _|_, then you can write a function that
polymorphically "returns" an element of any type (here, I mean it
claims to return such a thing, but actually never returns). For
example, if unbounded recursion is allowed, then you can write:
f(t:type):t = f(t)
Given that, you can "produce" an element of an uninhabited type.
Specifically, if t is the type of propositions that a=b, then f(t) is
a proof that a=b, for any possible a and b. So, when a type system
allows _|_, you can prove anything.
> > It would be good for future languages that aspire to be pure to allow
> > a clear distinction between expressions that admit _|_ and expressions
> > that disallow it. The former can be used in propositional proofs,
> > proof-carrying-code, and other metamathematical formulations
> > regardless of evaluation strategy, while the later are necessary for
> > many mainstream programming tasks.
>
> Do you mean to exchange "former" and "latter" in the second sentence
> above? Assuming so, I believe Daniel Wang and I both agree with you.
Oops, yes.
> I also believe Daniel Wang and I both agree with the rest of your post,
> except there seems to be a difference in terminology definition when you
> say that
>
> > Effects are not monads and _|_ is not an effect.
>
> It is quite clear to me that _|_ is a monad (namely the monad taking
> each type x to x + unit). The term "effect" is rather vague, and
> while I am happy to take monads to be a technical approximation to the
> intuitive notion, I am also happy to entertain alternative definitions.
> Can you explain yours a bit more?
Well, you could model the notion of "a term that is either _|_ or a
pure value" using Haskell's Maybe monad. This is similar to the
notion of _|_ that comes up when considering functions that throw
exceptions (without associated values) that can be caught upstream in
a program, as some parser combinators do.
But, _|_ comes up in other situations where Maybe doesn't capture the
essence of what's happening. Consider the type of (potentially
infinite recursive) functions from integers to integers, for example.
If you model these as f :: int->Maybe int, then you would expect to be
able to write code like
a = f 7
b = case a of
Nothing -> ..
Maybe x -> ..
Here, we've tried to hide _|_ (the low-level potential for no-return)
in the Maybe monad. We would expect "f" to be a pure function that is
certain to return in finite time, and to either return a value or a
Nothing tag. How do you generate such an "f" from a traditional
recursive function definition? That would require solving the halting
problem.
Of course, that's not possible, so any language that tries to hide _|_
in a monad like Maybe is either impossible to implement, or would have
to be incapable of expressing general recursion.
BUT:
If you were to modify the Haskell compiler, you could still use such a
monad to encapsulate terms that potentially evaluate to _|_. You'd
probably just do this with a newtype aliasing the identity monad, and
only allowing calling of generally recursive functions using that
monad.
This situation would be similar to the RefMonad parts of IO and ST.
There is some consensus (still unproven) that it's not possible to
actually implement typesafe references directly with Haskell monads.
But monads do provide a clean way of exposing built-in runtime
features like this and limiting the scope where they can be used.
Neelakantan Krishnaswami
>
> This situation would be similar to the RefMonad parts of IO and
> ST. There is some consensus (still unproven) that it's not possible
> to actually implement typesafe references directly with Haskell
> monads. But monads do provide a clean way of exposing built-in
> runtime features like this and limiting the scope where they can be
> used.
What do you mean by "typesafe references"? Do you mean like ML refs,
which have to abide by the value restriction?
--
Neel Krishnaswami
ne...@alum.mit.edu
Ed Avis
>But, _|_ comes up in other situations where Maybe doesn't capture the
>essence of what's happening. Consider the type of (potentially
>infinite recursive) functions from integers to integers, for example.
>If you model these as f :: int->Maybe int, then you would expect to
>be able to write code like
>
>a = f 7
>b = case a of
> Nothing -> ..
> Maybe x -> ..
>
>Here, we've tried to hide _|_ (the low-level potential for no-return)
>in the Maybe monad. We would expect "f" to be a pure function that
>is certain to return in finite time, and to either return a value or
>a Nothing tag.
To make the discussion clearer I think it would be better to use some
name other than 'Maybe' for this monad, perhaps 'NT' for
non-termination.
Haven't you tried to write a function b of type
NT Int -> Int
or something similar? Surely this is no more possible than writing a
function of type
IO Int -> Int
The point of wrapping it up in a monad is that you cannot then try to
pattern-match or otherwise 'escape' from the nontermination. Yes,
Maybe is a monad, but it is a data type first and the monad machinery
is just a syntactically convenient way of handling it.
(There could be an unsafePerformComputation function of type NT x -> x
as an analogue unsafePerformIO. You'd use it when you were certain
that a computation really would terminate, despite its being in the NT
monad.)
--
Ed Avis <e...@membled.com>
Tim Sweeney
is that RefMonad encapsulates typesafe references to mutable values
stored on a heap, passed around in Monadic style using IO or ST, which
are instances of a new typeclass RefMonad denoting "monads capable of
storing references".
> To make the discussion clearer I think it would be better to use some
> name other than 'Maybe' for this monad, perhaps 'NT' for
> non-termination.
>
> Haven't you tried to write a function b of type
>
> NT Int -> Int
>
> or something similar? Surely this is no more possible than writing a
> function of type
>
> IO Int -> Int
>
> The point of wrapping it up in a monad is that you cannot then try to
> pattern-match or otherwise 'escape' from the nontermination. Yes,
> Maybe is a monad, but it is a data type first and the monad machinery
> is just a syntactically convenient way of handling it.
>
> (There could be an unsafePerformComputation function of type NT x -> x
> as an analogue unsafePerformIO. You'd use it when you were certain
> that a computation really would terminate, despite its being in the NT
> monad.)
This works, but to do this meaningfully, you'd need to modify the
Haskell compiler to assure that it's impossible to write potentially
infinite-recursive functions unless you're computing within an NT
monad, right?
The problem is, that rules out the use of general fixpoint recursion,
so you'd have to expose some other kinds of constructs for more
limited recursion schemes, such as primitive recursion. This makes it
VERY hard to write programs. For example, this definition is no
longer allowable:
fac :: integer -> integer
fac 0 = 1
fac n = n * fac (n - 1)
Such a framework might be useful for proofs-as-programs research, but
I can't imagine writing significant software without general
recursion.
Ed Avis
>>To make the discussion clearer I think it would be better to use
>>some name other than 'Maybe' for this monad, perhaps 'NT' for
>>non-termination.
>>(There could be an unsafePerformComputation function of type NT x ->
>>x as an analogue unsafePerformIO. You'd use it when you were
>>certain that a computation really would terminate, despite its being
>>in the NT monad.)
>
>This works, but to do this meaningfully, you'd need to modify the
>Haskell compiler to assure that it's impossible to write potentially
>infinite-recursive functions unless you're computing within an NT
>monad, right?
Yes, I think this is where the discussion came from. We were talking
about languages that let you write guaranteed-terminating expressions,
perhaps interfacing somehow with unrestricted expressions. (Or at
least I was ;-).)
>The problem is, that rules out the use of general fixpoint recursion,
Yes of course. Check the archives of this group.
--
Ed Avis <e...@membled.com>
Daniel C. Wang
{stuff deleted}
> The problem is, that rules out the use of general fixpoint recursion,
> so you'd have to expose some other kinds of constructs for more
> limited recursion schemes, such as primitive recursion. This makes it
> VERY hard to write programs. For example, this definition is no
> longer allowable:
>
> fac :: integer -> integer
> fac 0 = 1
> fac n = n * fac (n - 1)
>
> Such a framework might be useful for proofs-as-programs research, but
> I can't imagine writing significant software without general
> recursion.
The primitive recurisve definition for fact is not so bad..
datatype 'a nat_schema = Zero | Succ of ( int * 'a )
(* val nat_prim_rec : ('a nat_schema -> 'a) -> int -> 'a *)
fun nat_prim_rec f 0 = f Zero
| nat_prim_rec f n = f (Succ(n,nat_prim_rec f (n-1)))
val fact = nat_prim_rec (fn Zero => 1
| Succ(n,m) => n * m)
In fact, I can really get by with just a normal "fold".
datatype 'a nat_schema = Zero | Succ of 'a
(* val nat_fold : ('a nat_schema -> 'a) -> int -> 'a *)
fun nat_fold f 0 = f Zero
| nat_fold f n = f (Succ (nat_fold f (n-1)))
val fact' = nat_fold (fn Zero => (1,0)
| Succ(n,m) => (n+1,n * m))
val fact = (fn (_,n) => n) o fact'
Anyway, the majority of my ML code is almost always expressable has
some simple recursive function that could easily be replaced by a fold
of some sort. Programing with folds, espcially folds that can return
higher-order functions is quite a nice programming style. This styles
gurantees termination of my code. It's unfortunate that I can't take
advantage of that fact.
Dylan Thurston
> But, _|_ comes up in other situations where Maybe doesn't capture the
> essence of what's happening. Consider the type of (potentially
> infinite recursive) functions from integers to integers, for example.
> If you model these as f :: int->Maybe int, then you would expect to be
> able to write code like
>
> a = f 7
> b = case a of
> Nothing -> ..
> Maybe x -> ..
>
> Here, we've tried to hide _|_ (the low-level potential for no-return)
For the Maybe monad to properly model non-termination, it must be an
abstract type. Let's call it NT. NT, in addition to the monad
operations, should support operations like
fail :: NT a
fix :: (a -> a) -> NT a
but should not support, e.g., equality.
> Of course, that's not possible, so any language that tries to hide _|_
> in a monad like Maybe is either impossible to implement, or would have
> to be incapable of expressing general recursion.
I'm not sure what you mean by 'a monad like Maybe'. It would be
possible to write a language (in which types are not lifted by default)
which supports the operations above and can express general recursion
(using fix). Whether you think the abstract monad NT is like Maybe or
not is, I guess, a matter of taste.
Peace,
Dylan
Neelakantan Krishnaswami
> Neel: Google for "RefMonad", "newIORef", "readIORef", etc. The notion
> is that RefMonad encapsulates typesafe references to mutable values
> stored on a heap, passed around in Monadic style using IO or ST, which
> are instances of a new typeclass RefMonad denoting "monads capable of
> storing references".
Thanks.
--
Neel Krishnaswami
ne...@alum.mit.edu