刚性类型变量故障/怀疑不可信度

问题描述 投票：7回答：3

继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!]

然后要抓住他们都是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（注释掉）编译好，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 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，把所有的Term-inference放在课堂上Eval。但我试图密切反映GADT风格，以便我可能有许多应用程序'客户'共享相同的Term定义。

Addit：[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 }

使用FC，这个问题[在op实例中输入D Int的定义]很容易解决：F字典中的强制使得op的结果可以根据需要转换为b类型。

  • 这个例子似乎与q相同，类F，FunDep，IsTerm和类D是Eval。
  • 此示例不编译：给出与IsTerm/Eval相同的拒绝。
haskell types type-inference gadt
3个回答
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)
0
投票

请注意，IsTerm约束是方法eval，而不是Eval上的超类约束 - 它不可能存在，因为c的返回类型eval不是类的参数。

然后，孤立地考虑instance Eval Lit是误导。考虑Inc的实例，以及IsTerm的实例：

instance ( {-# tba #-} ) => Eval (Inc a)  where
  eval (Inc i) = ToTerm $ 1 + fromTerm (eval i)

instance (IsTerm a (Term int)) => IsTerm (Inc a) (Term Int)

那tba约束应包括什么？

  • 方法体对eval进行递归调用，因此需要Eval a。
  • 方法体的1 + ... eval ...需要eval来返回Int，但Eval约束不提供（因为它没有提到返回类型）。
  • 可以约束IsTerm a (Term Int)提供吗？不：IsTerm（充其量）由Eval暗示，而不是相反。

因此，如果没有大量重复，它可以挂在一起的唯一方法是：

  • 编译器看到了对eval的递归调用;神奇地为它添加了IsTerm a c1约束;为IsTerm找到适用的a实例;然后发现IsTerm实例产生了c1 ~ Term Int。
  • 但如果它只是裸a，那么就无法知道哪个实例。所以将约束保留为Wanted等待将eval应用于(Inc x)一段时间x？

相比之下，在Inc的GADT定义中，其论证需要是Term Int。这是阻止EDSL用户输入错误术语的紧身衣：

  Inc :: Term Int -> Term Int

至于instance Eval Lit的具体拒绝信息，我认为Hugs的措辞更加清晰：

- Inferred type is not general enough
*** Expression    : eval
*** Expected type : (Eval Lit, IsTerm Lit a) => Lit -> a
*** Inferred type : (Eval Lit, IsTerm Lit (Term Int)) => Lit -> Term Int

“预期类型”是方法的签名，实例头被替换。要检查类型不够“通用”的方法体，需要：

  1. 将方法的约束视为检查方法体的一部分;
  2. 看到该约束的类具有FunDep，并且它改进了参数类型的返回类型;
  3. 为IsTerm的实例找到适用的Eval实例（以及对该实例的任何约束的实例，递归地）;
  4. 通过FunDep改善c到Term int。

步骤3.特别是期望太多：适用的实例可能在一个单独的模块中声明，该模块不在范围内;通常（与此示例不同），它可能需要一个类型方案的实例/可用实例可能更具体或更通用/无法选择直到类型更精细。

但我确实有一个突出的问题：

  • 如果方法体的类型比通过替换实例头中的推断更具体，那么会出现什么问题？
  • Hugs消息中的推断类型更具体，但也带有约束，因此它们必须被释放才能接受程序。
  • 如果eval的调用者期望更通用的类型，则更具体的结果可以替代。
0
投票

我正在发布另一个答案，因为它是一个非常惊喜/一个罕见的野兽：代码编译在拥抱和工作;但不在GHC（8.6.4）下编译。除非有人在这里看到我出错了并且可以修复它。

首先考虑2011年论文中的Addit：示例。这仅在Hugs中实现（WinHugs的最新版本2006年9月）

class F a b | a -> b
instance F Int Bool

class D a where { op :: (F a b) => a -> b } 
instance (TypeCast Bool b') => D Int where { op _ = typeCast True }

除了instance D Int之外，该代码与论文相同。我添加了一个TypeCast约束（并调用它的方法），这看起来很奇怪，因为类型变量b'不会在任何地方使用。

我已经尝试了各种方法来在GHC中编译：

  • TypeCast大约等于GHC的~约束，这不是Hugs的特征;但将其更改为~将不会让GHC接受该代码。
  • 我尝试了各种类型的注释，包括ScopedTypeVariables。纳达。

有关更多详细信息，请参阅Trac #16430，包括TypeCast的定义 - 这完全是标准的。

那么原始q的代码就像这样（仅限拥抱）

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

instance (TypeCast (Term Int) c') => Eval Lit  where
         eval (Lit i) = typeCast (ToTerm i)       -- rejected without typeCast

instance (Eval a, IsTerm a (Term Int), TypeCast (Term Int) c')
         => Eval (Inc a)  where
         eval (Inc i) = typeCast (ToTerm $ 1 + fromTerm (eval i))
instance (Eval a, IsTerm a (Term Int), TypeCast (Term Bool) c') 
         => Eval (IsZ a)  where
         eval (IsZ i) = typeCast (ToTerm $ 0 == fromTerm (eval i))

eval aTerm（见上面的q）现在返回(ToTerm False);正如预期的那样，eval illtypedTerm给出了拒绝消息。

所有这些实例都将TypeCast表示为悬空类型变量（如果“feature”是正确的单词）。我是否已经实现了重复代码的任何保存，而不是使Eval成为一个具有两个参数的类，而这些参数只是从IsTerm重复，这是有争议的。

最新问题
© www.soinside.com 2019 - 2024. All rights reserved.