Here's the code
{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts #-}
{-# LANGUAGE GADTs, TypeFamilies #-}
{-# LANGUAGE ScopedTypeVariables, OverloadedStrings #-}
module Lib where
import Control.Applicative
import Control.Monad.Except
import Control.Monad.State
import Data.Text
type Var = Text
type Store a = [(Var, Expr a)]
-- type EvalMonad a = ExceptT Text (State (Store a))
class (Num a, Eq a, Ord a) => Divisible a where
divide :: a -> a -> a
instance Divisible Int where divide = div
instance Divisible Float where divide = (/)
data Expr a where
BoolConst :: Bool -> Expr Bool
NumberConst :: (Divisible n) => n -> Expr n
SquanchyString :: Text -> Expr Text
SquanchyVar :: Text -> Expr Text
Not :: Expr Bool -> Expr Bool
Xor :: Expr Bool -> Expr Bool -> Expr Bool
Equals :: (Eq a) => Expr a -> Expr a -> Expr Bool
GreaterThan :: (Eq a) => Expr a -> Expr a -> Expr Bool
Add :: (Divisible n) => Expr n -> Expr n -> Expr n
eval :: Expr a -> ExceptT Text (State (Store a)) a
eval (BoolConst a) = return a
eval (NumberConst a) = return a
eval (SquanchyString s) = return s
eval (SquanchyVar v) = extractValue v
eval (Not b) = not <$> eval b
eval (Xor a b) = do
orRes :: Bool <- (||) <$> eval a <*> eval b
andRes :: Bool <- (&&) <$> eval a <*> eval b
let notRes = not andRes
return $ orRes && notRes
eval (Equals a b) = do -- This stanza is where the problem gets revealed
res :: Bool <- equals a b
return res
-- eval (GreaterThan a b) = (>) <$> eval a <*> eval b
eval (Add a b) = ( ) <$> eval a <*> eval b
eval _ = undefined
equals :: (Eq n) => Expr n -> Expr n -> ExceptT Text (State (Store n)) Bool
equals a b = do
eOne <- eval a
eTwo <- eval b
return $ eOne == eTwo
extractValue :: Text -> ExceptT Text (State (Store a)) a
extractValue v = do
store :: Store a <- lift get
case (lookup v store) of
Just i -> eval i
Nothing -> throwError "doh"
Here's the error
• Could not deduce: a1 ~ Bool
from the context: a ~ Bool
bound by a pattern with constructor:
Equals :: forall a. Expr a -> Expr a -> Expr Bool,
in an equation for ‘eval’
at /home/michael/git/brokensquanchy/src/Lib.hs:65:7-16
‘a1’ is a rigid type variable bound by
a pattern with constructor:
Equals :: forall a. Expr a -> Expr a -> Expr Bool,
in an equation for ‘eval’
at /home/michael/git/brokensquanchy/src/Lib.hs:65:7-16
Expected type: ExceptT Text (State (Store a)) Bool
Actual type: ExceptT Text (State (Store a1)) Bool
• In a stmt of a 'do' block: res :: Bool <- equals a b
In the expression:
do res :: Bool <- equals a b
return res
In an equation for ‘eval’:
eval (Equals a b)
= do res :: Bool <- equals a b
return res
• Relevant bindings include
b :: Expr a1
(bound at /home/michael/git/brokensquanchy/src/Lib.hs:65:16)
a :: Expr a1
(bound at /home/michael/git/brokensquanchy/src/Lib.hs:65:14)
|
66 | res :: Bool <- equals a b
I'm hoping the answer is to include missing type information, but I'm not really sure. Any ideas?
Update: I improved my code, prompted by chepner's comment. But I still get the same error.
Why does ghc think a and a1 are different? How can I convince it otherwise?
CodePudding user response：
The type of your store is broken. In particular, the return type of eval is:
ExceptT Text (State (Store a)) a
while the return type of equals is:
ExceptT Text (State (Store n)) Bool
These types can only unify (as they must, for the case eval (Equals a b) = ...) if a and n are both Bool, i.e., only if you are comparing the equality of two booleans, and that's clearly not what you want.
More generally, the type of your store Store a indirectly forces all expressions in your language to have the same type, even in programs that don't use any variables (because the a is part of the monad's type, and that type needs to stay the same throughout your program), so you've accidentally written an evaluator that can either evaluate Bool expressions or evaluate Text expressions or evaluate numeric expressions, but can never handle expressions of different types in a single program.
In your current language, you only support Text variables (via SquanchyVar), so a quick way to fix this is to change every occurrence of Store a or Store n to Store Text, and modify extractValue to always return a Text value. So, the following typechecks:
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE OverloadedStrings #-}
module Lib where
import Control.Applicative
import Control.Monad.Except
import Control.Monad.State
import Data.Text
type Var = Text
type Store a = [(Var, Expr a)]
-- type EvalMonad a = ExceptT Text (State (Store a))
class (Num a, Eq a, Ord a) => Divisible a where
divide :: a -> a -> a
instance Divisible Int where divide = div
instance Divisible Float where divide = (/)
data Expr a where
BoolConst :: Bool -> Expr Bool
NumberConst :: (Divisible n) => n -> Expr n
SquanchyString :: Text -> Expr Text
SquanchyVar :: Text -> Expr Text
Not :: Expr Bool -> Expr Bool
And :: Expr Bool -> Expr Bool -> Expr Bool
Or :: Expr Bool -> Expr Bool -> Expr Bool
Xor :: Expr Bool -> Expr Bool -> Expr Bool
Equals :: (Eq a) => Expr a -> Expr a -> Expr Bool
GreaterThan :: (Eq a) => Expr a -> Expr a -> Expr Bool
LessThan :: (Eq a) => Expr a -> Expr a -> Expr Bool
Div :: (Divisible n) => Expr n -> Expr n -> Expr n
Mul :: (Divisible n) => Expr n -> Expr n -> Expr n
Sub :: (Divisible n) => Expr n -> Expr n -> Expr n
Add :: (Divisible n) => Expr n -> Expr n -> Expr n
eval :: Expr a -> ExceptT Text (State (Store Text)) a
eval (BoolConst a) = return a
eval (NumberConst a) = return a
eval (SquanchyString s) = return s
eval (SquanchyVar v) = extractValue v
eval (Not b) = not <$> eval b
eval (And a b) = (&&) <$> eval a <*> eval b
eval (Or a b) = (||) <$> eval a <*> eval b
eval (Xor a b) = do
orRes :: Bool <- (||) <$> eval a <*> eval b
andRes :: Bool <- (&&) <$> eval a <*> eval b
let notRes = not andRes
return $ orRes && notRes
eval (Equals a b) = do -- This stanza is where the problem gets revealed
res :: Bool <- equals a b
return res
-- eval (GreaterThan a b) = (>) <$> eval a <*> eval b
-- eval (LessThan a b) = (<) <$> eval a <*> eval b
eval (Div a b) = divide <$> eval a <*> eval b
eval (Mul a b) = (*) <$> eval a <*> eval b
eval (Add a b) = ( ) <$> eval a <*> eval b
eval (Sub a b) = (-) <$> eval a <*> eval b
eval _ = undefined
equals :: (Eq n) => Expr n -> Expr n -> ExceptT Text (State (Store Text)) Bool
equals a b = do
eOne <- eval a
eTwo <- eval b
return $ eOne == eTwo
extractValue :: Text -> ExceptT Text (State (Store Text)) Text
extractValue v = do
store :: Store a <- lift get
case (lookup v store) of
Just i -> eval i
Nothing -> throwError "doh"
Fixing your language to support variables with multiple types is significantly more complicated.
CodePudding user response：
Those are not the same a. The a inside the Equals constructor is different from the a that is generic parameter of eval.
Imagine this:
eval (Equals (SquanchyVar "foo") (SquanchyVar "bar"))
Here, the a inside the Equals constructor is Text (because that's the type of SquanchyVar), but the a that is generic parameter of eval is Bool (because that is the type of Equals). So they're different.
But a deeper problem is that your eval can only ever return one type. Because its result type a is also mentioned in the monad type ExceptT Text (State (Store a)) under which eval works, it means that in order to be in the same monad, any nested calls to eval must always return the same type as the outer eval that calls them.
But wait! Does your monad actually need to mention a? Let's see where it's actually used. Looks like the only use site is in extractValue. And look: it doesn't actually extract value of any type, it's only ever expected to work with Text.
So that's the solution: just make your monad ExceptT Text (State (Store Text)) instead of ExceptT Text (State (Store a)).
eval :: Expr a -> ExceptT Text (State (Store Text)) a
...
equals :: (Eq n) => Expr n -> Expr n -> ExceptT Text (State (Store Text)) Bool
...
extractValue :: Text -> ExceptT Text (State (Store Text)) Text