Re: Laws and partial values (was: [Haskell-cafe] mapM_ - Monoid.Monad.map)
On Sat, 2009-01-24 at 03:08 -0700, Luke Palmer wrote: On Sat, Jan 24, 2009 at 2:40 AM, Ryan Ingram ryani.s...@gmail.com wrote: On Fri, Jan 23, 2009 at 10:49 PM, Thomas Davie tom.da...@gmail.com wrote: Isn't the point of bottom that it's the least defined value. Someone above made the assertion that for left identity to hold, _|_ `mappend` () must be _|_. But, as there is only one value in the Unit type, all values we have no information about must surely be that value, so this is akin to saying () `mappend` () must be (), which our definition gives us. But _|_ is not (). Correction: _|_ is not always (). For example: in Haskell. Prelude () `seq` True True Prelude (undefined `asTypeOf` ()) `seq` True *** Exception: Prelude.undefined jcc ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Laws and partial values (was: [Haskell-cafe] mapM_ - Monoid.Monad.map)
On Fri, Jan 23, 2009 at 10:49 PM, Thomas Davie tom.da...@gmail.com wrote: Isn't the point of bottom that it's the least defined value. Someone above made the assertion that for left identity to hold, _|_ `mappend` () must be _|_. But, as there is only one value in the Unit type, all values we have no information about must surely be that value, so this is akin to saying () `mappend` () must be (), which our definition gives us. But _|_ is not (). For example: data Nat = Z | S Finite proveFinite :: Nat - () proveFinite Z = () proveFinite (S x) = proveFinite x infinity :: Nat infinity = S infinity somecode x = case proveFinite x of () - something_that_might_rely_on_x_being_finite problem = somecode infinity If you can pretend that the only value of () is (), and ignore _|_, you can break invariants. This becomes even more tricky when you have a single-constructor datatype which holds data relevant to the typechecker; ignoring _|_ in this case could lead to unsound code. -- ryan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Laws and partial values (was: [Haskell-cafe] mapM_ - Monoid.Monad.map)
On 24 Jan 2009, at 10:40, Ryan Ingram wrote: On Fri, Jan 23, 2009 at 10:49 PM, Thomas Davie tom.da...@gmail.com wrote: Isn't the point of bottom that it's the least defined value. Someone above made the assertion that for left identity to hold, _|_ `mappend` () must be _|_. But, as there is only one value in the Unit type, all values we have no information about must surely be that value, so this is akin to saying () `mappend` () must be (), which our definition gives us. But _|_ is not (). For example: data Nat = Z | S Finite proveFinite :: Nat - () proveFinite Z = () proveFinite (S x) = proveFinite x infinity :: Nat infinity = S infinity somecode x = case proveFinite x of () - something_that_might_rely_on_x_being_finite problem = somecode infinity If you can pretend that the only value of () is (), and ignore _|_, you can break invariants. This becomes even more tricky when you have a single-constructor datatype which holds data relevant to the typechecker; ignoring _|_ in this case could lead to unsound code. Your proveFinite function has the wrong type – it should be Nat - Bool, not Nat - () – after all, you want to be able to distinguish between proving it finite, and proving it infinite, don't you (even if in reality, you'll never return False). Bob___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Laws and partial values (was: [Haskell-cafe] mapM_ - Monoid.Monad.map)
On Sat, Jan 24, 2009 at 2:40 AM, Ryan Ingram ryani.s...@gmail.com wrote:
On Fri, Jan 23, 2009 at 10:49 PM, Thomas Davie tom.da...@gmail.com
wrote:
Isn't the point of bottom that it's the least defined value. Someone
above
made the assertion that for left identity to hold, _|_ `mappend` () must
be
_|_. But, as there is only one value in the Unit type, all values we
have
no information about must surely be that value, so this is akin to saying
()
`mappend` () must be (), which our definition gives us.
But _|_ is not ().
Correction: _|_ is not always ().
I'm no expert in topology, but I think it goes something like this:
You can interpret partiality in (at least) two ways. The one you're using
is to treat () as the Sierpinski space, which has one open set (which you
can think of as ()) and one closed set (as _|_). Bottoms are explicit, and
nontermination is an essential part of the calculus. The rest of the
topology is generated as follows: each function f : a - () defines an open
and a closed set of as. The open set is { x | f(x) = () }, and the closed
set is { x | f(x) = _|_ }. It is a fatal error to ignore _|_ in this
semantics.
There is another topology. Here the points are bottom-free values, possibly
infinite. It is generated by, for each *finite *partial value v, choosing
the set of all fully-defined x such that v is less defined than x. So, for
example, the open set representing Left _|_ in the space Either Bool Bool is
{ Left True, Left False }, whereas _|_ in this space is { Left True, Left
False, Right True, Right False }.
As far as I know, this is a valid topology as well, in which
scott-continuity corresponds to topological continuity. However, if you are
using this topology, then () = _|_.
I think the difference is that the latter topology ignores nontermination.
When programs terminate, the two interpretations agree. But the latter does
not give you any way to prove that something will not terminate.
FWIW, that last paragraph was gross speculation. :-)
For example:
data Nat = Z | S Finite
proveFinite :: Nat - ()
proveFinite Z = ()
proveFinite (S x) = proveFinite x
infinity :: Nat
infinity = S infinity
somecode x = case proveFinite x of () -
something_that_might_rely_on_x_being_finite
If some code relies on a value being finite, the only way it can go wrong if
you give it something infinite is not to terminate. This is kind of the
point of continuity.
problem = somecode infinity
If you can pretend that the only value of () is (), and ignore _|_,
you can break invariants. This becomes even more tricky when you have
a single-constructor datatype which holds data relevant to the
typechecker; ignoring _|_ in this case could lead to unsound code.
Except in those cases (in the absense of unsafeCoerce, I'm talking about
GADTs etc.) the compiler is checking them for you.
Luke
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Laws and partial values (was: [Haskell-cafe] mapM_ - Monoid.Monad.map)
On Fri, 23 Jan 2009, Luke Palmer wrote: For example, it is possible to prove that foldr mappend mempty (x:xs) = foldr1 mappend (x:xs). Which means that anywhere in the source where we see the former, we can clean it up to the latter. However, if monad laws don't apply to partial values, then we first have to prove that none of the (x:xs) are _|_, perhaps even that no substrings are _|_. This is a much more involved transformation, so much so that you probably just wouldn't do it if you want to be correct. Bottoms are part of Haskell's semantics; theorems and laws have to apply to them to. You can pretend they don't exist, but then you have to be okay with never using an infinite data structure. I.e. if your programs would run just as well in Haskell as they would in a call-by-value language, then you don't have to worry about bottoms. BTW, This last statement isn't true. The expression (let x = 1:x in x) won't work in CBV, but it is a well defined value without any bottoms. In fact, every subexpression in that value is a well defined value wihtout any bottoms. Now I'm wondering how many bottoms I use in my actual code, because it seems like, even though I make use of lazy evaluation, I still don't have sub-expressions with bottoms. If it is the case that I never make use of bottoms, then having laws only apply to total values is fine. Obviously I use bottoms via the error function etc, but I don't count these. These can only be accessed by calling functions with paramters violating their preconditions. If I had dependent types, I'd place the preconditions formally into the definition of the function. I'm looking for a place where I have a partial value as a sub-expression of my program in some essential way. I find it plausible that this never happens. -- Russell O'Connor http://r6.ca/ ``All talk about `theft,''' the general counsel of the American Graphophone Company wrote, ``is the merest claptrap, for there exists no property in ideas musical, literary or artistic, except as defined by statute.''___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Laws and partial values (was: [Haskell-cafe] mapM_ - Monoid.Monad.map)
On Fri, Jan 23, 2009 at 08:10:38PM -0500, rocon...@theorem.ca wrote: I'd like to argue that laws, such as monoid laws, do not apply to partial values. But I haven't thought my position through yet. Before you do, you may want to read Fast and Loose Reasoning is Morally Correct: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.59.8232 Lauri ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Laws and partial values (was: [Haskell-cafe] mapM_ - Monoid.Monad.map)
On Sun, 25 Jan 2009, Lauri Alanko wrote: On Fri, Jan 23, 2009 at 08:10:38PM -0500, rocon...@theorem.ca wrote: I'd like to argue that laws, such as monoid laws, do not apply to partial values. But I haven't thought my position through yet. Before you do, you may want to read Fast and Loose Reasoning is Morally Correct: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.59.8232 This is very good. -- Russell O'Connor http://r6.ca/ ``All talk about `theft,''' the general counsel of the American Graphophone Company wrote, ``is the merest claptrap, for there exists no property in ideas musical, literary or artistic, except as defined by statute.'' ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Laws and partial values (was: [Haskell-cafe] mapM_ - Monoid.Monad.map)
On Sat, Jan 24, 2009 at 10:32 AM, rocon...@theorem.ca wrote:
On Fri, 23 Jan 2009, Luke Palmer wrote:
For example, it is possible to prove that foldr mappend mempty (x:xs) =
foldr1 mappend (x:xs). Which means that anywhere in the source where we
see
the former, we can clean it up to the latter. However, if monad laws
don't apply to partial values, then we first have to prove that none of
the
(x:xs) are _|_, perhaps even that no substrings are _|_. This is a much
more involved transformation, so much so that you probably just wouldn't
do
it if you want to be correct.
Bottoms are part of Haskell's semantics; theorems and laws have to apply
to
them to. You can pretend they don't exist, but then you have to be okay
with never using an infinite data structure. I.e. if your programs would
run just as well in Haskell as they would in a call-by-value language,
then
you don't have to worry about bottoms.
BTW, This last statement isn't true. The expression (let x = 1:x in x)
won't work in CBV, but it is a well defined value without any bottoms.
In fact, every subexpression in that value is a well defined value wihtout
any bottoms.
That's not what I said. My statement was a hypothetical: *if* it works
call-by-value, then you don't have to worry about bottom. This program does
not work in CBV, so my statement is true.
I'm just being pedantic, of course.
The deeper reason that you have to worry about bottoms in this expression is
that its denotation is a limit: { _|_, 1:_|_, 1:1:_|_, 1:1:1:_|_, ... }.
Bottom has an essential role in describing infinity, not just programs which
don't halt.
Luke
**
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Laws and partial values (was: [Haskell-cafe] mapM_ - Monoid.Monad.map)
On Fri, 23 Jan 2009, Derek Elkins wrote: mempty `mappend` undefined = undefined (left identity monoid law) The above definition doesn't meet this, similarly for the right identity monoid law. That only leaves one definition, () `mappend` () = () which does indeed satisfy the monoid laws. So the answer to the question is Yes. Another example of making things as lazy as possible going astray. I'd like to argue that laws, such as monoid laws, do not apply to partial values. But I haven't thought my position through yet. -- Russell O'Connor http://r6.ca/ ``All talk about `theft,''' the general counsel of the American Graphophone Company wrote, ``is the merest claptrap, for there exists no property in ideas musical, literary or artistic, except as defined by statute.'' ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Laws and partial values (was: [Haskell-cafe] mapM_ - Monoid.Monad.map)
On Fri, Jan 23, 2009 at 6:10 PM, rocon...@theorem.ca wrote: On Fri, 23 Jan 2009, Derek Elkins wrote: mempty `mappend` undefined = undefined (left identity monoid law) The above definition doesn't meet this, similarly for the right identity monoid law. That only leaves one definition, () `mappend` () = () which does indeed satisfy the monoid laws. So the answer to the question is Yes. Another example of making things as lazy as possible going astray. I'd like to argue that laws, such as monoid laws, do not apply to partial values. But I haven't thought my position through yet. Please try to change your mind. You know how annoying it is when you are doing math, and you want to divide, but first you have to add the provision that the denominator isn't zero. Saying that monoid laws do not apply to partial values, while easing the implementation a bit, add similar provisions to reasoning. For example, it is possible to prove that foldr mappend mempty (x:xs) = foldr1 mappend (x:xs). Which means that anywhere in the source where we see the former, we can clean it up to the latter. However, if monad laws don't apply to partial values, then we first have to prove that none of the (x:xs) are _|_, perhaps even that no substrings are _|_. This is a much more involved transformation, so much so that you probably just wouldn't do it if you want to be correct. Bottoms are part of Haskell's semantics; theorems and laws have to apply to them to. You can pretend they don't exist, but then you have to be okay with never using an infinite data structure. I.e. if your programs would run just as well in Haskell as they would in a call-by-value language, then you don't have to worry about bottoms. Luke ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Laws and partial values (was: [Haskell-cafe] mapM_ - Monoid.Monad.map)
Thanks for letting me reflect on this. I assume that my final program (my final value) is always a total value. Anything else is an error. Therefore, if we required relaxed monoid laws of the form x `mappend` mzero = x then we could safely substitute (x `mappend` mzero) by x without changing the final value (I think this true). But the reverse substituion ,replacing x with (x `mappend` mzero), might not be sound. Now, I can see why you would prefer that the laws hold for partial values. On Fri, 23 Jan 2009, Luke Palmer wrote: On Fri, Jan 23, 2009 at 6:10 PM, rocon...@theorem.ca wrote: On Fri, 23 Jan 2009, Derek Elkins wrote: mempty `mappend` undefined = undefined (left identity monoid law) The above definition doesn't meet this, similarly for the right identity monoid law. That only leaves one definition, () `mappend` () = () which does indeed satisfy the monoid laws. So the answer to the question is Yes. Another example of making things as lazy as possible going astray. I'd like to argue that laws, such as monoid laws, do not apply to partial values. But I haven't thought my position through yet. Please try to change your mind. You know how annoying it is when you are doing math, and you want to divide, but first you have to add the provision that the denominator isn't zero. Saying that monoid laws do not apply to partial values, while easing the implementation a bit, add similar provisions to reasoning. For example, it is possible to prove that foldr mappend mempty (x:xs) = foldr1 mappend (x:xs). Which means that anywhere in the source where we see the former, we can clean it up to the latter. However, if monad laws don't apply to partial values, then we first have to prove that none of the (x:xs) are _|_, perhaps even that no substrings are _|_. This is a much more involved transformation, so much so that you probably just wouldn't do it if you want to be correct. Bottoms are part of Haskell's semantics; theorems and laws have to apply to them to. You can pretend they don't exist, but then you have to be okay with never using an infinite data structure. I.e. if your programs would run just as well in Haskell as they would in a call-by-value language, then you don't have to worry about bottoms. Luke -- Russell O'Connor http://r6.ca/ ``All talk about `theft,''' the general counsel of the American Graphophone Company wrote, ``is the merest claptrap, for there exists no property in ideas musical, literary or artistic, except as defined by statute.''___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Laws and partial values (was: [Haskell-cafe] mapM_ - Monoid.Monad.map)
On 24 Jan 2009, at 02:33, Luke Palmer wrote: On Fri, Jan 23, 2009 at 6:10 PM, rocon...@theorem.ca wrote: On Fri, 23 Jan 2009, Derek Elkins wrote: mempty `mappend` undefined = undefined (left identity monoid law) The above definition doesn't meet this, similarly for the right identity monoid law. That only leaves one definition, () `mappend` () = () which does indeed satisfy the monoid laws. So the answer to the question is Yes. Another example of making things as lazy as possible going astray. I'd like to argue that laws, such as monoid laws, do not apply to partial values. But I haven't thought my position through yet. Please try to change your mind. I'd actually argue that this is just the wrong way of formulating my statement. Please correct my possibly ill informed maths, if Im doin it rong though... Isn't the point of bottom that it's the least defined value. Someone above made the assertion that for left identity to hold, _|_ `mappend` () must be _|_. But, as there is only one value in the Unit type, all values we have no information about must surely be that value, so this is akin to saying () `mappend` () must be (), which our definition gives us. Bob ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
