My Weblog

Blog about programming and math

GADT Exercise

Wikibooks has one of the excellent explanation of Generalized Algebraic Datatypes. More on Haskell Wiki. Before going into the GADT there is a exercise “Despite our goal, it may still be instructional to implement the eval function; do this.”

Starting point:
data Expr = I Int
        | B Bool           -- boolean constants
        | Add Expr Expr
        | Mul Expr Expr
        | Eq  Expr Expr    -- equality test
 
eval :: Expr -> Maybe (Either Int Bool)
-- Your implementation here.

I tried to implement it and many thanks to ski and clahey ( #haskell ) for suggesting me how to solve this problem. My implementation and if there is any error or suggestion then please let me know.

module GData where

data Expr = I Int
        | B Bool           -- boolean constants
        | Add Expr Expr
        | Mul Expr Expr
        | Eq  Expr Expr    -- equality test
        deriving ( Show )


eval :: Expr -> Maybe ( Either Int Bool )
eval ( I n )  = Just ( Left n )
eval ( B b )  = Just ( Right b )
eval ( Add e1 e2 ) = case ( eval e1 , eval e2 ) of
                   ( Just ( Left a ) , Just ( Left b ) ) -> Just ( Left ( a + b ) )
                   ( Just ( Right b ) , _ ) -> Nothing
                   ( _ , Just ( Right b ) ) -> Nothing


eval ( Mul e1 e2 ) = case ( eval e1 , eval e2 ) of
                  ( Just ( Left a ) , Just ( Left b ) ) -> Just ( Left ( a * b ) )
                  ( Just ( Right b ) , _ ) -> Nothing
                  ( _ , Just ( Right b ) ) -> Nothing

eval ( Eq e1 e2 ) = case ( eval e1 , eval e2 ) of
                       ( Just ( Left a )  , Just ( Left b ) )  -> Just ( Right ( a == b ) )
                       ( Just ( Right a ) , Just ( Right b ) ) -> Just ( Right ( a == b ) ) -- this will for single expression like B True `Eq` B True
                       ( _ , _ ) -> Nothing  -- No comparision between Int and Bool 

--main :: IO ()
--main = print.eval $ ( ( I 5 `Add` I 1 ) `Mul` I 7 :: Expr )  `Eq` ( ( I 5 `Add` I 1 ) `Mul` I 7 :: Expr )  

*GData> eval $ ( ( I 5 `Add` I 1 ) `Mul` I 7 :: Expr )  `Eq` ( ( I 5 `Add` I 1 ) `Mul` I 7 :: Expr ) 
Just (Right True)
*GData> eval $ ( ( I 5 `Add` I 1 ) `Mul` I 7 :: Expr )  
Just (Left 42)
*GData> eval $ B True `Eq` I 1
Nothing
*GData> eval $ B True `Eq` B False
Just (Right False)
*GData> eval $ B True `Eq` B True
Just (Right True)

Added GADT. The Eq constructor is bit different from wikibooks. The expression Eq :: Expr Int -> Expr Int -> Expr Bool will simply reject the valid case B True `Eq` B True or B True `Eq` B False so adding the constraint on Eq constructors elements and it should be member of Eq class ( Hopefully I have explained it correctly ).

{-#LANGUAGE GADTs, EmptyDataDecls, KindSignatures #-}
module GData where
data Expr :: * -> * where 
  I :: Int -> Expr Int 
  B :: Bool -> Expr Bool
  Add :: Expr Int -> Expr Int -> Expr Int 
  Mul :: Expr Int -> Expr Int -> Expr Int
  Eq :: Eq a => Expr a -> Expr a  -> Expr Bool

eval :: Expr a -> a 
eval ( I n ) = n 
eval ( B b ) = b
eval ( Add e1 e2 ) = eval e1 + eval e2 
eval ( Mul e1 e2 ) = eval e1 * eval e2 
eval ( Eq e1 e2 ) = eval e1 == eval e2

*GData> :r
[1 of 1] Compiling GData            ( GData.hs, interpreted )
Ok, modules loaded: GData.
*GData> eval $ ( ( I 5 `Add` I 1 ) `Mul` I 7 :: Expr Int )  `Eq` ( ( I 5 `Add` I 1 ) `Mul` I 7 :: Expr Int )
True
*GData> eval $ ( ( I 5 `Add` I 1 ) `Mul` I 7 :: Expr Int )  
42
*GData> eval $ B True `Eq` B True
True
*GData> eval $ B True `Eq` I 5

<interactive>:25:20:
    Couldn't match type `Int' with `Bool'
    Expected type: Expr Bool
      Actual type: Expr Int
    In the return type of a call of `I'
    In the second argument of `Eq', namely `I 5'
    In the second argument of `($)', namely `B True `Eq` I 5'
Advertisements

December 7, 2012 - Posted by | Haskell, Programming

No comments yet.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: