Поиск обитателей типа для просто типизированного лямбда-исчисления

LamInhab.hs

{-# LANGUAGE FlexibleContexts #-}
module LamInhab where
import Data.List (insertBy)
import Control.Monad.State

-- Тип символов
type Symb = String 

infixl 2 :@

-- Терм
data Expr = Var Symb        -- переменная
          | Expr :@ Expr    -- применение (аппликация) терма к терму
          | Lam Symb Expr   -- абстракция терма по переменной
              deriving (Eq) 

-- (c) Kolganov
instance Show Expr where
    showsPrec _ = showsLambdaTerm 0 where
        showsLambdaTerm _ (Var c) = showString c
        showsLambdaTerm d (l :@ m) = showParen (d > 1) $
            showsLambdaTerm (if (d <= 1) then 1 else 2) l.
            showChar ' ' .
            showsLambdaTerm (if (d == 0 || d == 3) then 3 else 2) m
        showsLambdaTerm d m@(Lam c l) = showParen (d < 3) $
            showChar '\\' .
            showsAbstraction m
        showsAbstraction (Lam c l) = showString (c ++ " ") . showsAbstraction l
        showsAbstraction l = showString "-> " . shows l


infixr 3 :->

-- Тип
data Type = 
  TVar Symb        -- переменная типа
  | Type :-> Type   -- стрелочный тип
    deriving (Eq,Show)

-- Контекст
newtype Env = Env [(Symb,Type)]
  deriving (Eq,Show)

-- (c такой версией виснем на монстре (((a->a)->a)->a)->a->a)
-- расширение контекста символом s с типом t
--extendEnv :: Env -> Symb -> Type -> Env
--extendEnv (Env env) s t = Env $ (s,t) : env

instance Ord Type where
  compare (TVar a)  (TVar b)    = compare a b
  compare x        (TVar _)    = GT
  compare (TVar _)  y          = LT
  -- то что ниже, похоже, не важно для наших целей
  compare (a :-> b) (a' :-> b') = 
    let compareArg = compare a a'
        compareRes = compare b b' 
    in if compareArg == EQ 
       then compareRes
       else compareArg

-- новая версия, сохраняющая порядок на типах
extendEnv :: Env -> Symb -> Type -> Env
extendEnv (Env cs) s t = Env $ insertBy cmpTypes (s,t) cs
   where cmpTypes (_,t1) (_,t2) = compare t1 t2
   
   
----------------------------------------
-- Инхабитация

-- свежая переменная при каждом следующем обращении
getFreshVar :: MonadState Integer m => m Expr
getFreshVar = do
  n <- get
  modify (+1)
  return $ Var $ "x" ++ show n
  
-- сужаем окружение до термовых переменных, тип которых возвращает заданную переменную типа
properEnvTypes :: Env -> Type -> Env
properEnvTypes (Env cs) (TVar alpha) = Env $ filter (\(x,t) -> getRetTypeVar t == alpha) cs

-- возвращаемая переменная типа
getRetTypeVar :: Type -> Symb
getRetTypeVar (TVar tv) = tv
getRetTypeVar (_ :-> t2) = getRetTypeVar t2

-- список типов аргументов типа
getArgTypeVars :: Type -> [Type]
getArgTypeVars (TVar _) = []
getArgTypeVars (t1 :-> t2) = t1 : getArgTypeVars t2

-- Инхабитация
inhab :: Env -> Type -> [Expr]
inhab env typ =  evalStateT (inhab' env typ) 1 
  
inhab' :: Env -> Type -> StateT Integer [] Expr
inhab' gamma (t1 :-> t2) = do
  Var x <- getFreshVar
  body <- inhab' (extendEnv gamma x t1) t2
  return $ Lam x $ body
inhab' gamma alpha = do
  let Env propers = properEnvTypes gamma alpha
  (x,tau) <- StateT $ \st -> map (\x -> (x,st)) propers
  foldM (\e t -> fmap (e :@) $ inhab' gamma t) (Var x) (getArgTypeVars tau)

-- Инхабитация комбинаторами
inhab0 :: Type -> [Expr]
inhab0 = inhab (Env [])

{-
> inhab0 (TVar "a")
[]
> inhab0 (TVar "a" :-> TVar "a")
[(\x1 -> x1)]
> inhab0 (TVar "a" :-> TVar "b")
[]
> inhab0 (TVar "a" :-> TVar "a" :-> TVar "a")
[(\x1 x2 -> x2),(\x1 x2 -> x1)]
> inhab0 (TVar "a" :-> TVar "a" :-> TVar "a" :-> TVar "a")
[(\x1 x2 x3 -> x3),(\x1 x2 x3 -> x2),(\x1 x2 x3 -> x1)]
> inhab0 (TVar "a" :-> TVar "b" :-> TVar "a" :-> TVar "a")
[(\x1 x2 x3 -> x3),(\x1 x2 x3 -> x1)]

-- числа Черча
> take 5 $ inhab0 $ (TVar "a" :-> TVar "a") :-> TVar "a" :-> TVar "a"
[(\x1 x2 -> x2),(\x1 x2 -> x1 x2),(\x1 x2 -> x1 (x1 x2)),(\x1 x2 -> x1 (x1 (x1 x2))),(\x1 x2 -> x1 (x1 (x1 (x1 x2))))]

-- вот и первая полу-бяка: до x1 никогда не доберемся
> take 5 $ inhab0 $ (TVar "a" :-> TVar "a") :-> (TVar "a" :-> TVar "a") :-> TVar "a" :-> TVar "a"
[(\x1 x2 x3 -> x3),(\x1 x2 x3 -> x2 x3),(\x1 x2 x3 -> x2 (x2 x3)),(\x1 x2 x3 -> x2 (x2 (x2 x3))),(\x1 x2 x3 -> x2 (x2 (x2 (x2 x3))))]

-- тип бинарных деревьев
> take 6 $ inhab0 $ (TVar "a" :-> TVar "a" :-> TVar "a") :-> TVar "a" :-> TVar "a"
[(\x1 x2 -> x2),(\x1 x2 -> x1 x2 x2),(\x1 x2 -> x1 x2 ((x1 x2) x2)),(\x1 x2 -> x1 x2 ((x1 x2) ((x1 x2) x2))),(\x1 x2 -> x1 x2 ((x1 x2) ((x1 x2) ((x1 x2) x2)))),(\x1 x2 -> x1 x2 ((x1 x2) ((x1 x2) ((x1 x2) ((x1 x2) x2)))))]

-- Тип 3 порядка: количество переменных, по которым абстрагируемся, неограниченно растет
> take 6 $ inhab0 $ ((TVar "a" :-> TVar "a") :-> TVar "a") :-> TVar "a"
[(\x1 -> x1 \x2 -> x2),(\x1 -> x1 \x2 -> x1 \x3 -> x3),(\x1 -> x1 \x2 -> x1 \x3 -> x2),(\x1 -> x1 \x2 -> x1 \x3 -> x1 \x4 -> x4),(\x1 -> x1 \x2 -> x1 \x3 -> x1 \x4 -> x3),(\x1 -> x1 \x2 -> x1 \x3 -> x1 \x4 -> x2)]

-- fmap для монады Cont
> inhab0 $ (TVar "a" :-> TVar "b") :->  ((TVar "a" :-> TVar "c") :-> TVar "d") :-> (TVar "b" :-> TVar "c") :-> TVar "d"
[(\x1 x2 x3 -> x2 \x4 -> x3 (x1 x4))]

-- fmap для монады Sel
> take 3 $ inhab0 $ (TVar "a" :-> TVar "b") :->  ((TVar "a" :-> TVar "c") :-> TVar "a") :-> (TVar "b" :-> TVar "c") :-> TVar "b"
[(\x1 x2 x3 -> x1 (x2 \x4 -> x3 (x1 x4))),(\x1 x2 x3 -> x1 (x2 \x4 -> x3 (x1 (x2 \x5 -> x3 (x1 x5))))),(\x1 x2 x3 -> x1 (x2 \x4 -> x3 (x1 (x2 \x5 -> x3 (x1 x4)))))]

-- после упорядочивания контекста по сложности типа на монстре уже не виснем, 
-- но достижимым остается только одно семейство из огромного богатства
> take 5 $ inhab0 $ (((TVar "a" :-> TVar "a") :-> TVar "a") :-> TVar "a") :-> TVar "a" :-> TVar "a"
[(\x1 x2 -> x2),(\x1 x2 -> x1 \x3 -> x2),(\x1 x2 -> x1 \x3 -> x3 x2),(\x1 x2 -> x1 \x3 -> x3 (x3 x2)),(\x1 x2 -> x1 \x3 -> x3 (x3 (x3 x2)))]
-}