Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Haskell: Type safety with logically different Boolean values

Lets say I've got the following code

type IsTall = Bool
type IsAlive = Bool

is_short_alive_person is_tall is_alive = (not is_tall) && is_alive

Say, later on, I've got the following

a :: IsAlive
a = False

b :: IsTall
b = True

And call the following, getting the two arguments around the wrong way:

is_short_alive_person a b

This successfully compiles unfortunately, and at runtime tall dead people are instead found instead of short alive people.

I would like the above example not to compile.

My first attempt was:

newtype IsAlive = IsAlive Bool
newtype IsTall = IsTall Bool

But then I can't do something like.

switch_height :: IsTall -> IsTall
switch_height h = not h

As not is not defined on IsTalls, only Bools.

I could explicitly extract the Bools all the time, but that largely defeats the purpose.

Basically, I want IsTalls to interact with other IsTalls, just like they're Bools, except they won't interact with Bools and IsAlives without an explicit cast.

What's the best way to achieve this.


p.s. I think I've achieved this with numbers by doing in GHC:

{-# LANGUAGE GeneralizedNewtypeDeriving #-}

newtype UserID = UserID Int deriving (Eq, Ord, Num)
newtype GroupID = GroupID Int deriving (Eq, Ord, Num)

(i.e. UserID's and GroupID's shouldn't interact)

but I can't seem to do this with Bools (deriving Bool doesn't work). I'm not even sure the above is the best approach anyway.

like image 598
Clinton Avatar asked May 11 '12 03:05

Clinton


3 Answers

Your options are either to define algebraic data types like

data Height = Tall | Short
data Wiggliness = Alive | Dead

or to define new operators, e.g., &&&, |||, complement and to overload them on the type of your choice. But even with overloading you won't be able to use them with if.

I'm not sure that Boolean operations on height make sense anyway. How do you justify a conclusion that "tall and short equals short" but "tall or short equals tall"?

I suggest you look for different names for your connectives, which you can then overload.

P.S. Haskell is always getting new features, so the best I can say is that if you can overload if I'm not aware of it. To say about Haskell that "such-and-such can't be done" is always dangerous...

like image 27
Norman Ramsey Avatar answered Nov 05 '22 10:11

Norman Ramsey


If you change your data type slightly you can make it an instance of Functor and you can then use fmap to do operations on the Boolean

import Control.Applicative

newtype IsAliveBase a = IsAlive a 
newtype IsTallBase a = IsTall a 

type IsAlive = IsAliveBase Bool
type IsTall = IsTallBase Bool

instance Functor IsAliveBase where
    fmap f (IsAlive b) = IsAlive (f b)

instance Functor IsTallBase where
    fmap f (IsTall b) = IsTall (f b)

switch_height :: IsTall -> IsTall 
switch_height h = not <$> h -- or fmap not h

-- EDIT

for operations like && you can make it an instance of Applicative

instance Applicative IsAliveBase where
    pure = IsAlive
    (IsAlive f) <*> (IsAlive x) = IsAlive (f x)

and then you can do (&&) using liftA2

example:

*Main> let h = IsAlive True
*Main> liftA2 (&&) h h 
IsAlive True

you can read more about this at http://en.wikibooks.org/wiki/Haskell/Applicative_Functors

like image 127
Phyx Avatar answered Nov 05 '22 10:11

Phyx


You can get some way towards this, using newtypes and a class if you import the Prelude hiding the boolean functions you want to use with your IsTall and IsAlive values. You redefine the boolean functions as methods in the class, for which you then make instances for all 3 of the Bool, IsTall, and IsAlive types. If you use GeneralizedNewtypeDeriving you can even get the IsTall and IsAlive instances without having to write the wrapping/unwrapping boilerplate by hand.

Here's an example script I actually tried out in ghci:

{-# LANGUAGE GeneralizedNewtypeDeriving #-}

import Prelude hiding ((&&), (||), not)
import qualified Prelude

class Boolish a where
    (&&) :: a -> a -> a
    (||) :: a -> a -> a
    not :: a -> a

instance Boolish Bool where
    (&&) = (Prelude.&&)
    (||) = (Prelude.||)
    not = Prelude.not

newtype IsTall = IsTall Bool
    deriving (Eq, Ord, Show, Boolish)

newtype IsAlive = IsAlive Bool
    deriving (Eq, Ord, Show, Boolish)

You can now &&, ||, and not values of any of the three types, but not together. And they're separate types, so your function signatures can now restrict which of the 3 they want to accept.

Higher order functions defined in other modules will work fine with this, as in:

*Main> map not [IsTall True, IsTall False]
[IsTall False,IsTall True]

But you won't be able to pass an IsTall to any other function defined elsewhere that expects a Bool, because the other module will still be using the Prelude version of the boolean functions. Language constructs like if ... then ... else ... will still be a problem too (although a comment by hammar on Norman Ramsey's answer says you can fix this with another GHC extension). I'd probably add a toBool method to that class to help uniformly convert back to regular Bools to help mitigate such problems.

like image 23
Ben Avatar answered Nov 05 '22 11:11

Ben