Thu Dec 20 07:23:05 EST 2007

```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
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

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.