evaluador mutuamente recursivo en Haskell

Question

Actualización: He añadido una respuesta que describe mi solución final (pista: el tipo de datos único Expr no era suficiente).

---

escribir un evaluador para un poco de lenguaje de expresión, pero estoy atascado en el LetRec constructo.

Este es el lenguaje:

type Var = String
type Binds = [(Var, Expr)]

data Expr
  = Var     Var
  | Lam     Var    Expr
  | App     Expr   Expr
  | Con     Int
  | Sub     Expr   Expr
  | If      Expr   Expr  Expr
  | Let     Var    Expr  Expr
  | LetRec  Binds  Expr
  deriving (Show, Eq)

Y esto esta el evaluador hasta ahora:

data Value
  = ValInt   Int
  | ValFun   Env   Var  Expr
  deriving (Show, Eq)

type Env = [(Var, Value)]

eval :: Env -> Expr -> Either String Value
eval env (Var x)       = maybe (throwError  $ x ++ " not found")
                               return
                               (lookup x env)
eval env (Lam x e)     = return $ ValFun env x e
eval env (App e1 e2)   = do
                         v1 <- eval env e1
                         v2 <- eval env e2
                         case v1 of
                           ValFun env1 x e -> eval ((x, v2):env1) e
                           _ -> throwError "First arg to App not a function"
eval _   (Con x)       = return $ ValInt x
eval env (Sub e1 e2)   = do
                         v1 <- eval env e1
                         v2 <- eval env e2
                         case (v1, v2) of
                           (ValInt x, ValInt y) -> return $ ValInt (x - y)
                           _ -> throwError "Both args to Sub must be ints"
eval env (If p t f)    = do 
                         v1 <- eval env p
                         case v1 of
                           ValInt x -> if x /= 0
                                       then eval env t
                                       else eval env f
                           _ -> throwError "First arg of If must be an int"
eval env (Let x e1 e2) = do
                         v1 <- eval env e1
                         eval ((x, v1):env) e2
eval env (LetRec bs e) = do
                         env' <- evalBinds
                         eval env' e
  where
    evalBinds = mfix $ \env' -> do
      env'' <- mapM (\(x, e') -> eval env' e' >>= \v -> return (x, v)) bs
      return $ nub (env'' ++ env)

Esta es mi función de prueba Deseo evaluar:

test3 :: Expr
test3 = LetRec [ ("even", Lam "x" (If (Var "x")
                                      (Var "odd" `App` (Var "x" `Sub` Con 1))
                                      (Con 1)
                                  ))
               , ("odd",  Lam "x" (If (Var "x")
                                      (Var "even" `App` (Var "x" `Sub` Con 1))
                                      (Con 0)
                                  ))
               ]
               (Var "even" `App` Con 5)

---

EDIT:

Sobre la base de la respuesta de Travis y el comentario de Lucas, he actualizado mi código utilizar el MonadFix ejemplo para el error de mÓNADA. El ejemplo anterior funciona bien ahora! Sin embargo, el ejemplo de abajo no funciona correctamente:

test4 :: Expr
test4 = LetRec [ ("x", Con 3)
               , ("y", Var "x")
               ]
               (Con 0)

Al evaluar esto, los bucles de evaluador, y no pasa nada. Supongo que he hecho algo un poco demasiado estricta aquí, pero no estoy seguro de lo que es. Am I violar una de las leyes MonadFix?

Answer 1

Cuando Haskell le da un ataque, que normalmente es una indicación de que usted no ha pensado con claridad sobre un tema central de su problema. En este caso, la cuestión es: ¿qué modelo de evaluación ¿desea utilizar para su idioma? Call-by-valor o de llamada por necesidad?

Su representación de entornos como [(Var,Value)] sugiere que desea utilizar de llamada por valor, ya que cada Expr se evalúa a un Value de inmediato antes de almacenarlos en el medio ambiente. Pero letrec no va bien con eso, y su segundo ejemplo muestra!

Por otra parte, cabe destacar que el modelo de evaluación de la lengua de acogida (Haskell) interferirá con el modelo de evaluación del idioma que desea implementar; De hecho, eso es lo que está haciendo actualmente para uso de sus ejemplos: a pesar de su finalidad, sus Values no se evalúan a forma normal débil cabeza

.

A menos que tenga una imagen clara del modelo de evaluación de su lenguaje de expresión poco, que no avanzará mucho en letrec o en el error de comprobación de instalaciones.

Editar Por ejemplo, una especificación de letrec en una lengua llamada por valor, echar un vistazo a la Manual Ocaml . En el nivel más simple, que sólo permiten lados derechos que son expresiones lambda, es decir, las cosas que son conocidos para ser sintácticamente valores.

Answer 2

Tal vez me falta algo, pero no lo hace el siguiente trabajo?

eval env (LetRec bs ex) = eval env' ex
  where
    env' = env ++ map (\(v, e) -> (v, eval env' e)) bs

Para su versión actualizada: ¿Qué pasa con el siguiente enfoque? Funciona como desee en el caso de test, y no tirar errores en expresiones LetRec:

data Value
  = ValInt Int
  | ValFun EnvWithError Var Expr
  deriving (Show, Eq)

type Env = [(Var, Value)]
type EnvWithError = [(Var, Either String Value)]

eval :: Env -> Expr -> Either String Value
eval = eval' . map (second Right)
  where
    eval' :: EnvWithError -> Expr -> Either String Value
    eval' env (Var x)        = maybe (throwError  $ x ++ " not found")
                                     (join . return)
                                     (lookup x env)
    eval' env (Lam x e)      = return $ ValFun env x e
    eval' env (App e1 e2)    = do
                               v1 <- eval' env e1
                               v2 <- eval' env e2
                               case v1 of
                                 ValFun env1 x e -> eval' ((x, Right v2):env1) e
                                 _ -> throwError "First arg to App not a function"
    eval' _   (Con x)        = return $ ValInt x
    eval' env (Sub e1 e2)    = do
                               v1 <- eval' env e1
                               v2 <- eval' env e2
                               case (v1, v2) of
                                 (ValInt x, ValInt y) -> return $ ValInt (x - y)
                                 _ -> throwError "Both args to Sub must be ints"
    eval' env (If p t f)     = do 
                               v1 <- eval' env p
                               case v1 of
                                 ValInt x -> if x /= 0
                                             then eval' env t
                                             else eval' env f
                                 _ -> throwError "First arg of If must be an int"
    eval' env (Let x e1 e2)  = do
                               v1 <- eval' env e1
                               eval' ((x, Right v1):env) e2
    eval' env (LetRec bs ex) = eval' env' ex
      where
        env' = env ++ map (\(v, e) -> (v, eval' env' e)) bs

Answer 3

contestar a mi propia pregunta; Quería compartir la solución final se me ocurrió.

señaló , no lo hice de verdad pensar en el impacto que tiene el orden de evaluación.

En un lenguaje estricto (llamada por valor), una expresión que ya es un valor (forma normal débil cabeza) es diferente de una expresión que todavía necesita algún tipo de evaluación. Una vez que esta distinción codificado en mi tipo de datos, todo cayó en su lugar:

type Var = String
type Binds = [(Var, Val)]

data Val
  = Con Int
  | Lam Var Expr
  deriving (Show, Eq)

data Expr
  = Val Val
  | Var Var
  | App Expr Expr
  | Sub Expr Expr
  | If Expr Expr Expr
  | Let Var Expr Expr
  | LetRec Binds Expr
  deriving (Show, Eq)

La única diferencia con mi mi tipo de datos Expr original, es que saqué dos constructores (Con y Lam) en su propio tipo de datos Val. El tipo de datos Expr tiene un nuevo Val constructor, esto representa el hecho de que un valor es también una expresión válida.

Con los valores en su propio tipo de datos, que puede ser manipulado por separado de otra expresión, por ejemplo, los enlaces de letrec sólo puede contener valores, no hay otras expresiones.

Esta distinción también se hace en otros lenguajes como C estrictas, donde sólo funciones y constantes se pueden definir en el ámbito global.

completa código de la función evaluadora actualizada.