I'm trying to extend the classic GADTs example around eval-ing a Value, but I'm hitting something I don't fully understand.
data Command a where
Base64_ :: Command a
Take_ :: Int -> Command a
-- eval only works with this definition
-- with this uncommented, cmd breaks with:
--
-- Could not deduce: v ~ T.Text
-- from the context: a ~ T.Text
-- bound by a pattern with constructor:
-- VString :: T.Text -> Value T.Text,
-- in an equation for ‘cmd’
-- ‘v’ is a rigid type variable bound by
-- the type signature for:
-- cmd :: forall c a v. Command c -> Value a -> Value v
data Value v where
VString :: T.Text -> Value T.Text
VInt :: Int -> Value Int
VBool :: Bool -> Value Bool
VNot :: Value Bool -> Value Bool
-- cmd only works with this definition
-- with this uncommented, eval breaks with:
--
-- Couldn't match expected type ‘a’ with actual type ‘T.Text’
-- ‘a’ is a rigid type variable bound by
-- the type signature for:
-- eval :: forall a. Value a -> a
-- data Value v where
-- VString :: T.Text -> Value v
-- VInt :: Int -> Value v
-- VBool :: Bool -> Value v
-- VNot :: Value Bool -> Value v
eval :: Value a -> a
eval (VString i) = i
eval (VInt i) = i
eval (VBool b) = b
eval (VNot b) = not $ eval b
cmd :: Command c -> Value a -> Value v
cmd Base64_ (VString s) = VString $ encodeBase64 s
cmd (_) (_) = VInt 3 -- or show error for no match.
Is what I'm trying to do possible? Is there a single GADT definition that would work with both eval and cmd, or am I getting one of the function signatures incorrect?
The type signature:
cmd :: Command c -> Value a -> Value v
says that a Command c of any "type" c takes a Value a of any "type" a and can produce a value Value v of any caller-requested "type" v. But, your Base64_ command doesn't take a Value a of any type, it only takes a Value T.Text, and it doesn't produce a Value v of any type the caller wants, it only produces a Value T.Text.
What you probably want to do is construct your Command c GADT so that the c part determines the permitted input a and actual output v.
One way of doing this would be to use a GADT with multiple type arguments, like:
data Command a v where
Base64_ :: Command T.Text T.Text
IsZero_ :: Command Int Bool
where a indicates the input type, and v indicates the output type for each defined command.
Now, the signature:
cmd :: Command a v -> Value a -> Value v
expresses the idea that a command of a particular type Command a v for concrete values of a and v can be expected to accept a Value a and produce a Value v, and the following definition will work:
cmd :: Command a v -> Value a -> Value v
cmd Base64_ (VString s) = VString $ encodeBase64 s
cmd IsZero_ (VInt x) = VBool $ x == 0
Full example:
{-# LANGUAGE GADTs #-}
import qualified Data.Text as T
import Data.Text.Encoding.Base64
data Command a v where
Base64_ :: Command T.Text T.Text
IsZero_ :: Command Int Bool
data Value v where
VString :: T.Text -> Value T.Text
VInt :: Int -> Value Int
VBool :: Bool -> Value Bool
VNot :: Value Bool -> Value Bool
eval :: Value a -> a
eval (VString i) = i
eval (VInt i) = i
eval (VBool b) = b
eval (VNot b) = not $ eval b
cmd :: Command a v -> Value a -> Value v
cmd Base64_ (VString s) = VString $ encodeBase64 s
cmd IsZero_ (VInt x) = VBool $ x == 0