Переводчик Haskell для языка System T Combinator

Question

В предыдущем вопросе о компиляторе SystemT и работе с бесконечными типами в Haskell я спросил о том, как анализировать лямбда-исчисление SystemT в SystemT Combinators. Я решил использовать простые алгебраические типы данных для кодирования как лямбда-исчисления 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-programming-in-partial.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 дерево, такое, что я получаю какую-то функцию обратно, которая может быть выполнена частично.

Answer 1

Интерпретировать THom гарантированно хорошо типизированным способом вам нужно будет "объяснить" его типы средству проверки типов на Haskell. Я вижу, вы уже рассмотрели версию GADT THom, что было бы обычным способом сделать это объяснение, и это все еще подход, с которым я бы пошел. Если я правильно понимаю, проблема, с которой вы столкнулись, заключается в том, что логика synth был слишком сложным, чтобы доказать, что он всегда будет производить хорошо напечатанный THomи это неудивительно.

Я думаю, что вы можете сохранить свой synth (грубо) как есть, если вы добавляете простой проход, этот тип проверяет полученный нетипизированный THom в печатный GADT, скажем StrongTHom a b, Возврат экзистенциалов кажется рискованным, было бы предпочтительно предоставить ему входящий контекст:

checkTHom :: THom -> TType a -> TType b -> Maybe (StrongTHom a b)

(где TType это форма синглтона в предыдущем ответе). Это просто требует, чтобы вы знали на верхнем уровне, какими будут ваши типы ввода и вывода. Обычно это нормально, потому что для того, чтобы реально использовать результат, вам в конечном итоге нужно будет знать типы, в которых он создается в любом случае. (Возможно, вам придется выдвинуть эту ожидаемую информацию о типе наружу на несколько уровней, пока не будет известен конкретный тип)

Если вы абсолютно должны иметь возможность выводить типы ввода и вывода, то я полагаю, что нет другого выбора, кроме как вернуть экзистенциальный. Это просто означает, что ваша проверка типов будет включать гораздо больше проверок на равенство типов (ср. typeEq ниже) и нетипизированный THom может также потребоваться включить больше информации о типе.

В любом случае THom определенно придется включать любые типы, которые он стирает. Например, в Compose :: THom a b -> THom b c -> THom a c, b стирается и checkTHom придется его реконструировать. Так Compose Необходимо включить достаточно информации, чтобы это было возможно. На данный момент экзистенциальный (SomeType из предыдущего ответа), вероятно, будет хорошо, потому что единственный способ использовать его - развернуть его и передать его рекурсивно.

Для написания этой проверки у меня есть ощущение, что вам понадобится строгая проверка на равенство:

typeEq :: TType a -> TType b -> Maybe (a :~: b)

(где :~: стандартное равенство типов), которое легко написать; Я просто проверяю, знаете ли вы о технике.

Если у вас есть это, то eval :: StrongTHom a b -> a -> b должен пройти как теплое масло. Удачи!

Answer 2

Кроме того, довольно просто выполнить проверку типов во время выполнения, объявив тип всех возможных значений.

data Value
    = VUnit                          -- of type One
    | VPair Value Value              -- of type Pair
    | VFunc (Value -> Interp Value)  -- of type Func
    | VNat Integer                   -- of type Nat

Тогда вы можете очень напрямую использовать свой нетипизированный THom, для соответствующего переводчика монады Interp (может быть, просто Except монада):

eval :: THom -> Value -> Interp Value
eval Id v  = v
eval Unit _ = VUnit
eval Zero VUnit = VNat Zero
eval Succ (VNat n) = VNat (n + 1)
...
eval _ _ = throwE "type error"

Обратите внимание также, что VFunc выше имеет тот же тип, что и кодомен eval, поскольку встроенные функции также могут не работать.