[Haskell-cafe] Knowledge

[Tillmann Rendel]

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