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

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

Подход в исходном посте

Для перевода исходного поста требуется Template 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, вам нужно проверить (во время выполнения), что их типы совпадают. А с простым экзистенциалом нельзя. Поэтому вам нужно иметь представление типов также на уровне значений.

Более того, экзистенциалы раздражают (как обычно), поскольку вы никогда не можете раскрыть переменные скрытого типа в возвращаемом типе или спроецировать их (в отличие от зависимых записей/сигма-типов). Я, честно говоря, не совсем уверен, что это может в конечном итоге заставить работать. Вот возможный частичный набросок на Haskell, до одного случая 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