В предыдущем вопросе Компилятор SystemT и работа с Бесконечными типами в Haskell Я спросил о том, как анализировать лямбда-исчисление SystemT в комбинаторах SystemT.Я решил использовать простые алгебраические типы данных для кодирования как лямбда-исчисления SystemT, так и исчисления SystemT Combinator (основываясь на комментарии: Компилятор SystemT и работа с бесконечными типами в Haskell ).
SystemTCombinator.hs:
module SystemTCombinator where
data THom = Id
| Unit
| Zero
| Succ
| Compose THom THom
| Pair THom THom
| Fst
| Snd
| Curry THom
| Eval
| Iter THom THom
deriving (Show)
SystemTLambda.hs:
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE TypeSynonymInstances #-}
module SystemTLambda where
import Control.Monad.Catch
import Data.Either (fromRight)
import qualified SystemTCombinator as SystemTC
type TVar = String
data TType = One | Prod TType TType | Arrow TType TType | Nat deriving (Eq)
instance Show TType where
show ttype = case ttype of
One -> "'Unit"
Nat -> "'Nat"
Prod ttype1 ttype2 ->
"(" ++ show ttype1 ++ " * " ++ show ttype2 ++ ")"
Arrow ttype1@(Arrow _ _) ttype2 ->
"(" ++ show ttype1 ++ ") -> " ++ show ttype2
Arrow ttype1 ttype2 -> show ttype1 ++ " -> " ++ show ttype2
data TTerm = Var TVar
| Let TVar TTerm TTerm
| Lam TVar TTerm
| App TTerm TTerm
| Unit
| Pair TTerm TTerm
| Fst TTerm
| Snd TTerm
| Zero
| Succ TTerm
| Iter TTerm TTerm TVar TTerm
| Annot TTerm TType
deriving (Show)
-- a context is a list of hypotheses/judgements
type TContext = [(TVar, TType)]
-- our exceptions for SystemT
data TException = TypeCheckException String
| BindingException String
deriving (Show)
instance Exception TException
newtype Parser a = Parser { run :: TContext -> Either SomeException a }
instance Functor Parser where
fmap f xs = Parser $ \ctx ->
either Left (\v -> Right $ f v) $ run xs ctx
instance Applicative Parser where
pure a = Parser $ \ctx -> Right a
fs <*> xs = Parser $ \ctx ->
either Left (\f -> fmap f $ run xs ctx) (run fs ctx)
instance Monad Parser where
xs >>= f = Parser $ \ctx ->
either Left (\v -> run (f v) ctx) $ run xs ctx
instance MonadThrow Parser where
throwM e = Parser (const $ Left $ toException e)
instance MonadCatch Parser where
catch p f = Parser $ \ctx ->
either
(\e -> case fromException e of
Just e' -> run (f e') ctx -- this handles the exception
Nothing -> Left e) -- this propagates it upwards
Right
$ run p ctx
withHypothesis :: (TVar, TType) -> Parser a -> Parser a
withHypothesis hyp cmd = Parser $ \ctx -> run cmd (hyp : ctx)
tvarToHom :: TVar -> Parser (SystemTC.THom, TType)
tvarToHom var = Parser $ \ctx ->
case foldr transform Nothing ctx of
Just x -> Right x
Nothing -> throwM $ BindingException ("unbound variable " ++ show var)
where
transform (var', varType) homAndType =
if var == var'
then Just (SystemTC.Snd, varType)
else homAndType >>= (\(varHom, varType) -> Just (SystemTC.Compose SystemTC.Fst varHom, varType))
check :: TTerm -> TType -> Parser SystemTC.THom
-- check a lambda
check (Lam var bodyTerm) (Arrow varType bodyType) =
withHypothesis (var, varType) $
check bodyTerm bodyType >>= (\bodyHom -> return $ SystemTC.Curry bodyHom)
check (Lam _ _ ) ttype = throwM
$ TypeCheckException ("expected function type, got '" ++ show ttype ++ "'")
-- check unit
check Unit One = return SystemTC.Unit
check Unit ttype =
throwM $ TypeCheckException ("expected unit type, got '" ++ show ttype ++ "'")
-- check products
check (Pair term1 term2) (Prod ttype1 ttype2) = do
hom1 <- check term1 ttype1
hom2 <- check term2 ttype2
return $ SystemTC.Pair hom1 hom2
check (Pair _ _ ) ttype = throwM
$ TypeCheckException ("expected product type, got '" ++ show ttype ++ "'")
-- check primitive recursion
check (Iter baseTerm inductTerm tvar numTerm) ttype = do
baseHom <- check baseTerm ttype
inductHom <- withHypothesis (tvar, ttype) (check inductTerm ttype)
numHom <- check numTerm Nat
return $ SystemTC.Compose (SystemTC.Pair SystemTC.Id numHom)
(SystemTC.Iter baseHom inductHom)
-- check let bindings
check (Let var valueTerm exprTerm) exprType = do
(valueHom, valueType) <- synth valueTerm
exprHom <- withHypothesis (var, valueType) (check exprTerm exprType)
return $ SystemTC.Compose (SystemTC.Pair SystemTC.Id valueHom) exprHom
check tterm ttype = do
(thom, ttype') <- synth tterm
if ttype == ttype'
then return thom
else throwM $ TypeCheckException
( "expected type '"
++ show ttype
++ "', inferred type '"
++ show ttype'
++ "'"
)
synth :: TTerm -> Parser (SystemTC.THom, TType)
synth (Var tvar) = tvarToHom tvar
synth (Let var valueTerm exprTerm) = do
(valueHom, valueType) <- synth valueTerm
(exprHom, exprType) <- withHypothesis (var, valueType) (synth exprTerm)
return (SystemTC.Compose (SystemTC.Pair SystemTC.Id valueHom) exprHom, exprType)
synth (App functionTerm valueTerm) = do
(functionHom, functionType) <- synth functionTerm
case functionType of
Arrow headType bodyType -> do
valueHom <- check valueTerm headType
return (SystemTC.Compose (SystemTC.Pair functionHom valueHom) SystemTC.Eval, bodyType)
_ -> throwM $ TypeCheckException ("expected function, got '" ++ show functionType ++ "'")
synth (Fst pairTerm) = do
(pairHom, pairType) <- synth pairTerm
case pairType of
Prod fstType sndType -> return (SystemTC.Compose pairHom SystemTC.Fst, fstType)
_ -> throwM $ TypeCheckException ("expected product, got '" ++ show pairType ++ "'")
synth (Snd pairTerm) = do
(pairHom, pairType) <- synth pairTerm
case pairType of
Prod fstType sndType -> return (SystemTC.Compose pairHom SystemTC.Snd, sndType)
_ -> throwM $ TypeCheckException ("expected product, got '" ++ show pairType ++ "'")
synth Zero = return (SystemTC.Compose SystemTC.Unit SystemTC.Zero, Nat)
synth (Succ numTerm) = do
numHom <- check numTerm Nat
return (SystemTC.Compose numHom SystemTC.Succ, Nat)
synth (Annot term ttype) = do
hom <- check term ttype
return (hom, ttype)
synth _ = throwM $ TypeCheckException "unknown synthesis"
Я использую вышеуказанную проверку двунаправленного типа для анализа SystemTLambda.TTerm в SystemTCombinator.THom.
systemTLambda :: TTerm
systemTLambda =
Let "sum"
(Annot
(Lam "x" $ Lam "y" $
Iter (Var "y") (Succ $ Var "n") "n" (Var "x"))
(Arrow Nat $ Arrow Nat Nat))
(App
(App
(Var "sum")
(Succ $ Succ Zero))
(Succ $ Succ $ Succ Zero))
systemTCombinator :: Either SomeException (SystemTC.THom, SystemTC.TType)
systemTCombinator = fromRight Unit $ run (synth result) []
Выражение комбинатора:
Compose (Pair Id (Curry (Curry (Compose (Pair Id (Compose Fst Snd)) (Iter Snd (Compose Snd Succ)))))) (Compose (Pair (Compose (Pair Snd (Compose (Compose (Compose Unit Zero) Succ) Succ)) Eval) (Compose (Compose (Compose (Compose Unit Zero) Succ) Succ) Succ)) Eval)
Проблема, с которой я столкнулся сейчас, состоит в том, как интерпретировать это выражение комбинатора.Я знаю, что все выражения комбинатора должны интерпретироваться как функция.Проблема в том, что я не знаю типы ввода и вывода этой функции, и я ожидаю, что функция «интерпретатора» будет частичной, то есть если она попытается что-то неправильно интерпретировать, это должно привести к RuntimeException, потому чтоВыражение комбинатора нетипизировано, возможно использование некорректных выражений комбинатора.Однако моя программа проверки типов должна гарантировать, что после достижения интерпретатора комбинаторы уже будут хорошо набраны.
Согласно исходному сообщению в блоге, http://semantic -domain.blogspot.com / 2012/12 / total-functional-program-in-part.html комбинаторы имеют все функциональные эквиваленты.Что-то вроде:
evaluate Id = id
evaluate Unit = const ()
evaluate Zero = \() -> Z
evaluate (Succ n) = S n
evaluate (Compose f g) = (evaluate g) . (evaluate f)
evaluate (Pair l r) = (evaluate l, evaluate r)
evaluate Fst = fst
evaluate Snd = snd
evaluate (Curry h) = curry (evaluate h)
evaluate Eval = \(f, v) -> f v
evaluate (Iter base recurse) = \(a, n) ->
case n of
Z -> evaluate base a
S n -> evaluate recurse (a, evaluate (Iter base recurse) (a, n))
Но, очевидно, это не работает.Кажется, должен быть какой-то способ интерпретации дерева THom, чтобы я мог получить какую-то функцию обратно, которая может быть выполнена частично.