haskellgadt

My toy language's evaluator won't type check


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?


Solution

  • 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.