问题描述
在下面的代码中，我想重写 g。如果可能，f 为 h 。可能有些情况 h 没有类的实例，但我想在可能的时候重写。我收到一条错误消息，提示这是可以实现的，但我不确定我需要更改哪些内容。
以下是一些示例代码：
{ - ＃LANGUAGE TypeFamilies＃ - }
main = return（）
data D a
f :: a - > D a
f =未定义
类型系列T a
类别G a其中
g :: D（T a） - > a
class H a其中
h :: T a - > a
{ - ＃RULES
myruleforall x。 g（fx）= hx
＃ - }
这是错误： p>
•无法从上下文中使用'h'
导致（H a）：G a
在trickyrewrite.hs：19：3-34
处由RULEmyrule绑定可能的修正：将（H a）添加到RULEmyrule
的上下文中•在表达式中：hx
当检查转换规则myrule时
请注意可能的修正： 添加（H a）到RULEmyrule 的上下文中。这看起来好像会完成这项工作，但我不知道如何实际做到这一点。在规则中甚至没有提到 a ，所以我不知道如果添加 H a code> a 不会引用任何内容。
如果它有什么区别，我控制的唯一代码是类 H 。我无法更改 G 。我的代码当然比这更复杂，但是如果我能看到一个如何得到这个简化示例工作的工作示例，我应该能够计算出我的代码。
我已经在下面尝试了@亚历克的建议，但它似乎不起作用，重写规则不是' t被触发。以下是我试过的代码：
{ - ＃LANGUAGE TypeFamilies＃ - }
{ - ＃LANGUAGE TypeApplications＃ - }
模块Main其中
main =（（g（f（2 :: Int）））:: Char）`seq` return（）
data D a
{ - ＃INLINE [1] f＃ - }
f :: a - > D a
f =未定义
类型系列T a
类型实例T Char = Int
{ - ＃INLINE [1] g'＃ - }
g'::（G a）=> D（T a） - > a
g'=未定义的
类G a其中
g :: D（T a） - > a
g = g'
实例G Char
class H a其中
h :: T a - > a
{ - ＃RULES
myruleforall（x :: H a => T a）。 g'（fx）= h @ax
＃ - }
forall 中的变量进行签名。就像 { - ＃RULESmyruleforall（x :: H a => T a）。 g（fx）= hx＃ - }
现在， T 可能不是内射的。幸运的是，我认为通过允许我们通知GHC类型变量 a 来解决这个问题 x 中的 T a 与 h ：
$ b $
{ - ＃LANGUAGE TypeFamilies，TypeApplications，AllowAmbiguousTypes＃ - }
...
{ - ＃RULESmyruleforall（x :: H a => T a）。 g（fx）= h @ax＃ - }
我们不需要启用 ScopedTypeVariables （即使我们依靠它来确保 a s是相同的），因为它在默认情况下处于重写状态规则。
In the following code, I want to rewrite g . f as h when possible. There may be cases h hasn't got the instance of class, but I'd like to do the rewrite when it's possible. I'm getting an error message suggesting this is achievable but I'm not sure exactly what I need to change.
Here is some sample code:
{-# LANGUAGE TypeFamilies #-}
main = return ()
data D a
f :: a -> D a
f = undefined
type family T a
class G a where
g :: D (T a) -> a
class H a where
h :: T a -> a
{-# RULES
"myrule" forall x. g (f x) = h x
#-}
An this is the error:
• Could not deduce (H a) arising from a use of ‘h’
from the context: G a
bound by the RULE "myrule" at trickyrewrite.hs:19:3-34
Possible fix: add (H a) to the context of the RULE "myrule"
• In the expression: h x
When checking the transformation rule "myrule"
Note the possible fix: add (H a) to the context of the RULE "myrule". This seems like it will do the job, but I'm not sure how to actually do this. a isn't even mentioned in the rule, so I'm not sure how adding H a will help when a doesn't refer to anything.
If it makes any difference, the only code I control is the class H. I can't change G. My code is of course more complex than this, but if I can see a worked example of how to get this simplified example working I should be able to work out my code I think.
Failed attempt:
I've tried @Alec's suggestion below but it doesn't seem to work, the rewrite rule isn't being triggered. Here's the code I tried:
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeApplications #-}
module Main where
main = ((g (f (2 :: Int))) :: Char) `seq` return ()
data D a
{-# INLINE [1] f #-}
f :: a -> D a
f = undefined
type family T a
type instance T Char = Int
{-# INLINE [1] g' #-}
g' :: (G a) => D (T a) -> a
g' = undefined
class G a where
g :: D (T a) -> a
g = g'
instance G Char
class H a where
h :: T a -> a
{-# RULES
"myrule" forall (x :: H a => T a). g' (f x) = h @a x
#-}
Normally, one can add type signatures to the variables in the forall. Something like
{-# RULES "myrule" forall (x :: H a => T a). g (f x) = h x #-}
Now, that doesn't quite work in this case because T may not be injective. Fortunately, I think TypeApplications gives us a way out of this problem by allowing us to inform GHC that the type variable a in the type T a of x is the same as the one in h:
{-# LANGUAGE TypeFamilies, TypeApplications, AllowAmbiguousTypes #-}
...
{-# RULES "myrule" forall (x :: H a => T a). g (f x) = h @a x #-}
We don't need to enable ScopedTypeVariables (even if we are relying on it to make sure the as are the same) because it is on by default in rewrite rules.
这篇关于添加上下文来重写规则的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！