刚性类型可变故障/可疑难以预测

Question

在关于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!]

然后发现他们都是Terms，需要正确输入

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（注释掉）编译为OK，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？专用类型sig是否推断为eval :: forall c. IsTerm Lit c => Lit -> c命令式？但是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风格保持一致，以便让许多应用程序“客户端”共享相同的Term定义。

附加： [3月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相同，其中class为class F，FunDep为being IsTerm和class D为Eval。

• 该示例未编译：给出与相同的拒绝IsTerm/Eval。

Answer 1

如果 GHC 可以（通过 FunDep）推断 c 必须是 Term Int for = undefined

不可以。如果您尝试undefined :: Term Int，您将得到相同的刚性类型变量错误。如果您使用键入的孔，= _undefined您会看到它正在推断undefined :: c。我不知道为什么，但函数依赖似乎只在应用于 eval时使用Lit，而不是在定义时使用。

那这个呢？

class IsTerm a where
  type TermType a :: *
instance IsTerm Lit where
  type TermType Lit = Int
instance IsTerm a => IsTerm (Inc a) where
  type TermType (Inc a) = TermType a

class IsTerm a => Eval a   
  where eval :: a -> Term (TermType a) 

instance Eval Lit  where    
         eval (Lit i) = ToTerm i

-- needs UndecidableInstances
instance (Eval a, Num (TermType a)) => Eval (Inc a)  where    
         eval (Inc i) = ToTerm (fromTerm (eval i) + 1)