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?

CodePudding user response：

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