Компилятор SystemT и работа с бесконечными типами в Haskell

Question

Я слежу за этим сообщением в блоге: http://semantic-domain.blogspot.com/2012/12/total-functional-programming-in-partial.html

Здесь показана небольшая программа компилятора OCaml для System T (простой тотальный функциональный язык).

Весь конвейер принимает синтаксис OCaml (через метапрограммирование Camlp4), преобразует их в OCaml AST, который переводится в SystemT Lambda Calculus (см.: module Term) и, наконец, SystemT Combinator Calculus (см.: module Goedel). Последний шаг также обернут метапрограммированием OCaml Ast.expr тип.

Я пытаюсь перевести его на Haskell без использования Template Haskell.

Для формы SystemT Combinator я написал ее как

{-# LANGUAGE GADTs #-}

data TNat = Zero | Succ TNat

data THom a b where
  Id :: THom a a
  Unit :: THom a ()
  ZeroH :: THom () TNat
  SuccH :: THom TNat TNat
  Compose :: THom a b -> THom b c -> THom a c
  Pair :: THom a b -> THom a c -> THom a (b, c)
  Fst :: THom (a, b) a
  Snd :: THom (a, b) b
  Curry :: THom (a, b) c -> THom a (b -> c)
  Eval :: THom ((a -> b), a) b -- (A = B) * A -> B
  Iter :: THom a b -> THom (a, b) b -> THom (a, TNat) b

Обратите внимание, что Compose это прямая композиция, которая отличается от (.),

Во время перевода SystemT Lambda Calculus в SystemT Combinator Calculus, Elaborate.synth Функция пытается преобразовать переменные лямбда-исчисления SystemT в серии составных проекционных выражений (связанных с индексами Де Брюджина). Это потому, что исчисление комбинатора не имеет переменных / имен переменных. Это сделано с Elaborate.lookup который использует Quote.find функция.

Проблема в том, что с моим кодированием исчисления комбинатора как GADT THom a b, Переводя Quote.find функция:

  let rec find x  = function
    | [] -> raise Not_found
    | (x', t) :: ctx' when x = x' -> <:expr< Goedel.snd >> 
    | (x', t) :: ctx' -> <:expr< Goedel.compose Goedel.fst $find x ctx'$ >>

В Хаскелл:

find :: TVar -> Context -> _
find tvar [] = error "Not Found"
find tvar ((tvar', ttype):ctx)
  | tvar == tvar' = Snd
  | otherwise     = Compose Fst (find tvar ctx)

В результате возникает ошибка бесконечного типа.

• Occurs check: cannot construct the infinite type: a ~ (a, c)
  Expected type: THom (a, c) c
    Actual type: THom ((a, c), c) c

Проблема связана с тем, что использование Compose а также Fst а также Snd от THom a b GADT может привести к бесконечным вариациям сигнатуры типа.

В статье нет этой проблемы, потому что она использует Ast.expr OCaml вещь, чтобы обернуть основные выражения.

Я не уверен, как решить в Haskell. Должен ли я использовать экзистенциально квантифицированный тип, как

data TExpr = forall a b. TExpr (THom a b)

Или какой-то тип уровня Fix адаптировать проблему бесконечного типа. Однако я не уверен, как это меняет find или же lookup функции.

Answer 1

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

Подход в оригинальном посте

Перевод оригинального поста требует шаблона Haskell и пристрастия; find вернет Q.Exp представляя некоторые Hom a b, избегая этой проблемы так же, как оригинальный пост. Как и в оригинальном посте, ошибка типа в исходном коде будет обнаружена при проверке типов при выводе всех функций Template Haskell. Таким образом, ошибки типов по-прежнему обнаруживаются до времени выполнения, но вам все равно нужно будет написать тесты, чтобы найти случаи, когда ваши макросы выводят некорректные выражения. Можно дать более сильные гарантии за счет значительного увеличения сложности.

Зависимая типизация /GADT на входе и выходе

Если вы хотите отклониться от поста, одной из альтернатив является повсеместное использование "зависимой типизации" и ввод данных с зависимой типизацией. Я свободно использую этот термин, чтобы включать в себя как фактически зависимо типизированные языки, так и реальный зависимый Haskell (когда он приземляется), а также способы фальсифицировать зависимую типизацию в Haskell сегодня (через GADT, синглтоны и тому подобное). Тем не менее, вы теряете возможность писать свой собственный тестер типов и выбирать, какую систему типов использовать; как правило, в итоге вы встраиваете простейшее лямбда-исчисление и можете имитировать полиморфизм с помощью полиморфных функций Haskell, которые могут генерировать термины для заданного типа. Это проще в зависимо-типизированных языках, но возможно вообще в Haskell.

Но, честно говоря, на этом пути проще использовать абстрактный синтаксис высшего порядка и функции Haskell, например:

data Exp a where
  Abs :: (Exp a -> Exp b) -> Exp (a -> b)
  App :: Exp (a -> b) -> Exp a -> Exp b
  Var :: String -> Exp a —- only use for free variables
exampleId :: Exp (a -> a)
exampleId = Abs (\x -> x)

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

От нетипизированных до типизированных терминов

Третий вариант - это ввод с зависимой типизацией, и все же заставить вашу программу преобразовывать слабо типизированный ввод в строго типизированный вывод. В этом случае ваш проверщик типов в целом преобразует термины некоторого типа Expr в терминах GADT TExp gamma t, Hom a bили такой. Поскольку вы не знаете статически, что gamma а также t (или же a а также b), вам действительно нужно какое-то экзистенциальное.

Но простой экзистенциальный объект слишком слаб: чтобы создать более крупное, хорошо типизированное выражение, вам нужно проверить, что производимые типы позволяют это. Например, чтобы построить TExpr содержащий Compose выражение из двух меньших TExpr, вам нужно проверить (во время выполнения), что их типы совпадают. А с простым экзистенциальным вы не можете. Поэтому вам нужно иметь представление типов также на уровне значений.

Более того, экзистенциалы надоедают иметь дело (как обычно), так как вы никогда не сможете раскрыть скрытые переменные типа в вашем возвращаемом типе или спроецировать их (в отличие от зависимых записей / сигма-типов). Я, честно говоря, не совсем уверен, что это в конечном итоге можно заставить работать. Вот возможный частичный набросок на Хаскелле, вплоть до одного случая find,

data Type t where
  VNat :: Type Nat
  VString :: Type String
  VArrow :: Type a -> Type b -> Type (a -> b)
  VPair :: Type a -> Type b -> Type (a, b) 
  VUnit :: Type ()
data SomeType = forall t. SomeType (Type t)
data SomeHom = forall a b. SomeHom (Type a) (Type b) (THom a b)

type Context = [(TVar, SomeType)] 
getType :: Context -> SomeType
getType [] = SomeType VUnit 
getType ((_, SomeType ttyp) :: gamma) =  
   case getType gamma of
       SomeType ctxT -> SomeType (VPair ttyp
find :: TVar -> Context -> SomeHom 
find tvar ((tvar’, ttyp) :: gamma)
   | tvar == tvar’ =
       case (ttyp, getType gamma) of
         (SomeType t, SomeType ctxT) ->
          SomeHom (VPair t ctxT) t Fst