haskell - 刚性类型变量麻烦/可疑

Question

继this q about GADTs之后，我正在尝试构建一个 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并且需要类型正确

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 ？是推断的专用类型sig eval :: forall c. IsTerm Lit c => Lit -> c势在必行？但是c是返回类型，所以它不是RankN(?)

什么可以避免这个错误？我有工作

• class (IsTerm a c) => Eval a c | a -> c where ...这只是复制 IsTerm 中的所有实例头，因此父类(super class)约束仅充当腰带和大括号。 (这就是我试图避免的双重情况。)

• type family ToTerm a ...; class Eval a where eval :: a -> ToTerm a 。但又是 Eval 的实例将 ToTerm 的所有实例加倍，并且还需要具有许多 ~ 的大型上下文ToTerm之间的约束来电。

我可以放弃类(class) IsTerm ，并将所有术语推断放在类 Eval 上。但我试图密切反射(reflect) GADT 风格，以便我可能有许多应用程序“客户端”共享相同的术语定义。

添加: [3 月 14 日]

2011年论文System F with Type Equality Coercions ，第 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 }

Using FC, this problem [of typing the definition of op in the instance D Int] is easily solved: the coercion in the dictionary for F enables the result of op to be cast to type b as required.

• 这个例子看起来和q一样，类为F ，与 FunDep 一起，为 IsTerm和类(class)D是Eval .

• 此示例无法编译:给出与 IsTerm/Eval 相同的拒绝.

Answer 1

If GHC can infer (via the FunDep) that c must be Term Int for = undefined

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

这个怎么样？

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)