Этот ответ должен быть немного высокоуровневым, потому что есть три совершенно разных семейства возможных вариантов решения этой проблемы. То, что вы делаете, кажется ближе к третьему, но упорядоченность подходов возрастает.
Подход в оригинальном посте
Перевод оригинального поста требует шаблона Haskell и пристрастия; find вернул бы Q.Exp, представляющий некоторую Hom a b, избегая этой проблемы, как и в оригинальном сообщении. Как и в оригинальном посте, ошибка типа в исходном коде будет обнаружена при проверке типов при выводе всех функций Template Haskell. Таким образом, ошибки типа по-прежнему обнаруживаются до времени выполнения, но вам все равно нужно будет написать tests , чтобы найти случаи, когда ваши макросы выводят некорректные выражения. Можно дать более сильные гарантии ценой значительного увеличения сложности.
Зависимая типизация / GADT на входе и выходе
Если вы хотите отклониться от поста, одной из альтернатив является повсеместное использование «зависимой типизации» и создание зависимой типизации input . Я свободно использую этот термин, чтобы включать в себя как фактически зависимо типизированные языки, так и реальный зависимый 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