Интерпретировать лямбда-му исчисление Париго в Хаскеле

Question

Можно интерпретировать лямбда-исчисление в Haskell:

data Expr = Var String | Lam String Expr | App Expr Expr

data Value a = V a | F (Value a -> Value a)

interpret :: [(String, Value a)] -> Expr -> Value a
interpret env (Var x) = case lookup x env of
  Nothing -> error "undefined variable"
  Just v -> v
interpret env (Lam x e) = F (\v -> interpret ((x, v):env) e)
interpret env (App e1 e2) = case interpret env e1 of
  V _ -> error "not a function"
  F f -> f (interpret env e2)

Как можно расширить вышеприведенный интерпретатор на исчисление лямбда-му? Я предполагаю, что он должен использовать продолжения для интерпретации дополнительных конструкций в этом исчислении. (15) и (16) из статьи Бернарди и Мортгата - это переводы, которые я ожидаю.

Это возможно, поскольку Haskell завершен по Тьюрингу, но как?

Подсказка: см. Комментарий на странице 197 к этой исследовательской работе для интуитивного значения mu binder.

Answer 1

Вот бессмысленная транслитерация правил редукции из статьи, использующая представление @user2407038 (как вы увидите, когда я говорю "бессмысленный", я действительно имею в виду "бессмысленный"):

{-# LANGUAGE DataKinds, KindSignatures, GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}

import Control.Monad.Writer
import Control.Applicative
import Data.Monoid

data TermType = Named | Unnamed

type Var = String
type MuVar = String

data Expr (n :: TermType) where
  Var :: Var -> Expr Unnamed
  Lam :: Var -> Expr Unnamed -> Expr Unnamed
  App :: Expr Unnamed -> Expr Unnamed -> Expr Unnamed
  Freeze :: MuVar -> Expr Unnamed -> Expr Named
  Mu :: MuVar -> Expr Named -> Expr Unnamed
deriving instance Show (Expr n)

substU :: Var -> Expr Unnamed -> Expr n -> Expr n
substU x e = go
  where
    go :: Expr n -> Expr n
    go (Var y) = if y == x then e else Var y
    go (Lam y e) = Lam y $ if y == x then e else go e
    go (App f e) = App (go f) (go e)
    go (Freeze alpha e) = Freeze alpha (go e)
    go (Mu alpha u) = Mu alpha (go u)

renameN :: MuVar -> MuVar -> Expr n -> Expr n
renameN beta alpha = go
  where
    go :: Expr n -> Expr n
    go (Var x) = Var x
    go (Lam x e) = Lam x (go e)
    go (App f e) = App (go f) (go e)
    go (Freeze gamma e) = Freeze (if gamma == beta then alpha else gamma) (go e)
    go (Mu gamma u) = Mu gamma $ if gamma == beta then u else go u

appN :: MuVar -> Expr Unnamed -> Expr n -> Expr n
appN beta v = go
  where
    go :: Expr n -> Expr n
    go (Var x) = Var x
    go (Lam x e) = Lam x (go e)
    go (App f e) = App (go f) (go e)
    go (Freeze alpha w) = Freeze alpha $ if alpha == beta then App (go w) v else go w
    go (Mu alpha u) = Mu alpha $ if alpha /= beta then go u else u

reduceTo :: a -> Writer Any a
reduceTo x = tell (Any True) >> return x

reduce0 :: Expr n -> Writer Any (Expr n)
reduce0 (App (Lam x u) v) = reduceTo $ substU x v u
reduce0 (App (Mu beta u) v) = reduceTo $ Mu beta $ appN beta v u
reduce0 (Freeze alpha (Mu beta u)) = reduceTo $ renameN beta alpha u
reduce0 e = return e

reduce1 :: Expr n -> Writer Any (Expr n)
reduce1 (Var x) = return $ Var x
reduce1 (Lam x e) = reduce0 =<< (Lam x <$> reduce1 e)
reduce1 (App f e) = reduce0 =<< (App <$> reduce1 f <*> reduce1 e)
reduce1 (Freeze alpha e) = reduce0 =<< (Freeze alpha <$> reduce1 e)
reduce1 (Mu alpha u) = reduce0 =<< (Mu alpha <$> reduce1 u)

reduce :: Expr n -> Expr n
reduce e = case runWriter (reduce1 e) of
    (e', Any changed) -> if changed then reduce e' else e

Это "работает" на примере из бумаги: с

example 0 = App (App t (Var "x")) (Var "y")
  where
    t = Lam "x" $ Lam "y" $ Mu "delta" $ Freeze "phi" $ App (Var "x") (Var "y")   
example n = App (example (n-1)) (Var ("z_" ++ show n))

Я могу уменьшить example n до ожидаемого результата:

*Main> reduce (example 10)
Mu "delta" (Freeze "phi" (App (Var "x") (Var "y")))

Причина, по которой я пишу пугающие цитаты вокруг "работ" выше, заключается в том, что у меня нет интуиции относительно исчисления λμ, поэтому я не знаю, что оно должно делать.

Answer 2

Примечание: это только частичный ответ, так как я не уверен, как расширить интерпретатор.

Это похоже на хороший вариант использования DataKinds. Expr Тип данных индексируется по типу с именем или без имени. Обычные лямбда-конструкции производят только именованные термины.

{-# LANGUAGE GADTs, DataKinds, KindSignatures #-} 

data TermType = Named | Unnamed 

type Var = String
type MuVar = String 

data Expr (n :: TermType) where 
  Var :: Var -> Expr Unnamed
  Lam :: Var -> Expr Unnamed -> Expr Unnamed
  App :: Expr Unnamed -> Expr Unnamed -> Expr Unnamed 

и дополнительный Mu а также Name конструкции могут манипулировать TermType,

  ...
  Name :: MuVar -> Expr Unnamed -> Expr Named 
  Mu :: MuVar -> Expr Named -> Expr Unnamed

Answer 3

Как насчет чего-то вроде ниже. У меня нет хорошей идеи о том, как пройти Value a, но, по крайней мере, я вижу, это оценивает example n в MuV,

import Data.Maybe

type Var = String
type MuVar = String

data Expr = Var Var
          | Lam Var Expr
          | App Expr Expr
          | Mu MuVar MuVar Expr
          deriving Show

data Value a = ConV a
             | LamV (Value a -> Value a)
             | MuV (Value a -> Value a)

type Env a = [(Var, Value a)]
type MuEnv a = [(MuVar, Value a -> Value a)]

varScopeErr :: Var -> Value a
varScopeErr v = error $ unwords ["Out of scope λ variable:", show v]

appErr :: Value a
appErr = error "Trying to apply a non-lambda"

muVarScopeErr :: MuVar -> (Value a -> Value a)
muVarScopeErr alpha = id

app :: Value a -> Value a -> Value a
app (LamV f) x = f x
app (MuV f) x = MuV $ \y -> f x `app` y
app _ _ = appErr

eval :: Env a -> MuEnv a -> Expr -> Value a
eval env menv (Var v) = fromMaybe (varScopeErr v) $ lookup v env
eval env menv (Lam v e) = LamV $ \x -> eval ((v, x):env) menv e
eval env menv (Mu alpha beta e) = MuV $ \u ->
  let menv' = (alpha, (`app` u)):menv
      wrap = fromMaybe (muVarScopeErr beta) $ lookup beta menv'
  in wrap (eval env menv' e)
eval env menv (App f e) = eval env menv f `app` eval env menv e

example 0 = App (App t (Var "v")) (Var "w")
  where
    t = Lam "x" $ Lam "y" $ Mu "delta" "phi" $ App (Var "x") (Var "y")
example n = App (example (n-1)) (Var ("z_" ++ show n))