jlw501 wrote:
I'm new to functional programming and Haskell and I love its expressive
ability! I've been trying to formalize the following function for time.
Given people and a piece of information, can all people know the same thing?
Anyway, this is just a bit of fun... but can anyone help me reduce it or
talk about strictness and junk as I'd like to make a blog on it?
I don't think your representation of unknown information is reasonable.
Haskell is not lazy enough to make it work out:
Prelude> True || undefined
True
Prelude> undefined || True
*** Exception: Prelude.undefined
From a logic perspective, unknown || true == true || unknown == true.
But this behaviour is impossible to implement in Haskell with unknown =
undefined, because you don't know in advance wich argument you should
inspect first. if you choose the undefined one, you will loop forever
without knowing the other argument would have been true.
In theoretical computer science, you would use a growing resource bound
to simulate the parallel evaluation of the two arguments. Maybe you can
use multithreading to implement the same trick in Haskell, but it
remains a trick.
So what can you do instead? I would encode the idea of unknown
information using an algebraic data type:
data Modal a = Known a | Unknown deriving Show
We can express knowing that something is true as (Known True), not
knowing anything as (Unknown) and knowing something as (Known
undefined). The advantage of this aproach is that we can define our
operations as strict or nonstrict as we want by pattern matching on the
Modal constructors.
(&&&) :: Modal Bool -> Modal Bool -> Modal Bool
Known True &&& Known True = Known True
Known False &&& _ = Known False
_ &&& Known False = Known False
_ &&& _ = Unknown
(|||) :: Modal Bool -> Modal Bool -> Modal Bool
Known False ||| Known False = Known False
Known True ||| _ = Known True
_ ||| Known True = Known True
_ ||| _ = Unknown
not' :: Modal Bool -> Modal Bool
not' (Known True) = Known False
not' (Known False) = Known True
not' Unknown = Unknown
By strictness, I'm not talking about Haskell strictness, but about Modal
strictness, that is:
A function (f :: Modal a -> Modal b) is Modal strict
if and only if f Unknown = Unknown
A nice property of modal strictness is that we can test for it. given a
total function f, we can use
isModalStrict :: (Modal a -> Modal b) -> Bool
isModalStrict f = case f Unknown of
Unknown -> True
_ -> False
to so wether it is strict. The results are as expected:
*Truth> isModalStrict not'
True
*Truth> isModalStrict (Known True |||)
False
*Truth> isModalStrict (Known True &&&)
True
*Truth> isModalStrict (&&& Known False)
False
Let's compare the last case to the representation unknown = undefined:
*Truth> (&& False) undefined
*** Exception: Prelude.undefined
As expected, (&& False) is Haskell strict, but (&&& Known False) not
Modal strict.
I don't know if this will help you, in the end you may find that Haskell
is a programming language, not a theorem prover. But at least for me, it
seems better to encode information explicitly instead of using undefined
to encode something.
Tillmann
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
