Исходя из этого q о GADT , я пытаюсь построить EDSL (для примера в статье), но без GADT.У меня есть кое-что, что позволяет избежать дублирования типов данных для AST;но вместо этого кажется удвоение кода.Поэтому я попытался урезать код, из-за чего у меня возникли проблемы ...
Вместо GADT, подобного этому
data Term a where
Lit :: Int -> Term Int
Inc :: Term Int -> Term Int
IsZ :: Term Int -> Term Bool
-- etc
объявляет каждый конструктор как отдельный тип данных
data Lit = Lit Int deriving (Show, Read)
data Inc a = Inc a deriving (Show, Read)
data IsZ a = IsZ a deriving (Show, Read)
-- etc
Затем пользователь EDSL может ввести и show условия
aTerm = IsZ (Inc (Lit 5))
illtypedTerm = Inc (IsZ (Lit 5)) -- accepted OK and can show
-- but can't eval [good!]
Затем, чтобы понять, что все они Term s и должны быть хорошо напечатаны
data Term a = ToTerm { fromTerm :: a} deriving (Show, Eq)
class IsTerm a c | a -> c
instance IsTerm Lit (Term Int)
-- etc
FunDep захватывает тип возврата из исходного GADT.Тогда eval может использовать этот Term тип
class Eval a
where eval :: (IsTerm a c) => a -> c
-- hmm this makes 'c' a rigid tyvar
instance Eval Lit where
eval (Lit i) = -- undefined -- accepted OK, infers :: Term Int
ToTerm i -- rejected
Уравнение eval (Lit i) = undefined (закомментировано) компилируется нормально, и GHC выводит eval (Lit 5) :: Term Int.Но если я поставлю = ToTerm i:
* Couldn't match expected type `c' with actual type `Term Int'
`c' is a rigid type variable bound by
the type signature for:
eval :: forall c. IsTerm Lit c => Lit -> c
* Relevant bindings include
eval :: Lit -> c
Если GHC может сделать вывод (через FunDep), что c должно быть Term Int для = undefined, почему нельзя для = ToTerm i?Является ли специализированный тип сигнала, который он выводит eval :: forall c. IsTerm Lit c => Lit -> c Impredicative?Но c - это тип возвращаемого значения, поэтому это не RankN (?)
Что позволяет избежать этой ошибки?У меня действительно работает
class (IsTerm a c) => Eval a c | a -> c where ..., это просто дублирует все головки экземпляров из IsTerm, поэтому ограничение суперкласса действует только как пояс и фигурные скобки.(Это удвоение, которое я пытался избежать.)
type family ToTerm a ...; class Eval a where eval :: a -> ToTerm a.Но опять же экземпляры для Eval удваивают все экземпляры для ToTerm, и, кроме того, нужны большие контексты со многими ~ ограничениями между ToTerm вызовами.
Я мог быпросто отбросьте класс IsTerm и поместите все Термины в класс Eval.Но я пытался отразить стиль GADT таким образом, чтобы у многих клиентов приложений было одно и то же определение термина.
Addit: [14 марта]
В документе 2011 года Система F с приведениями к равенству типов , раздел 2.3, приведен этот пример (при обсуждении функциональных зависимостей)
class F a b | a -> b
instance F Int Bool
class D a where { op :: F a b => a -> b }
instance D Int where { op _ = True }
При использовании FC эта проблема [при наборе текстаопределение op в экземпляре D Int] легко решается: приведение в словаре для F позволяет приводить результат op к типу b по мере необходимости.
Этот пример похож на q, с классом F, с FunDep, равным IsTerm, и классом D, равным Eval.
*, 1086 * * 1087.* Этот пример не компилируется: выдает тот же отказ, что и IsTerm/Eval.