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