在海上青焙坊中匹配高级类型

Question

一般来说，我想知道是否有一种方法可以编写一个通用折叠来概括应用forall类型的函数，例如：

f :: forall a. Data (D a) => D a -> b

给定某些数据类型Dinstance Data (D a)(可能对a有约束(。具体来说，考虑一些简单的东西，如False `mkQ` isJust，或者一般地，对更高种类的数据类型的构造函数进行查询。同样，请考虑仅影响一种特定高级类型的转换mkT (const Nothing)。

如果没有显式类型签名，它们会失败并带有No instance for Typeable a0，这可能是单态限制在起作用。很公平。但是，如果我们添加显式类型签名：

t :: GenericT
t = mkT (const Nothing :: forall a. Data a => Maybe a -> Maybe a)
q :: GenericQ Bool
q = False `mkQ` (isJust :: forall a. Data a => Maybe a -> Bool)

相反，我们被告知外部签名的forall类型是模棱两可的：

Could not deduce (Typeable a0)
arising from a use of ‘mkT’
from the context: Data a
bound by the type signature for:
t :: GenericT
The type variable ‘a0’ is ambiguous

我无法理解这一点。如果我真的正确地理解a0是t :: forall a0. Data a0 => a0 -> a0中的变量，它怎么会比说mkT not更模糊呢？如果有的话，我希望mkT抱怨，因为它是与isJust互动的人。此外，这些功能比混凝土类型的分支更具多态性。

我很想知道这是否是证明内部约束isJust :: Data a => ...的限制——我的理解是，任何类型的实例Data居住Maybe a也必须具有Data a才能被实例约束instance Data a => Data (Maybe a)有效。

Answer 1

TLDR：你需要创建一个不同的函数。

mkT具有以下签名：

mkT :: (Typeable a, Typeable b) => (a -> a) -> (b -> b)

并且您想将其应用于(forall x. Maybe x -> Maybe x)类型的多态函数。这是不可能的：没有办法在(a -> a)中实例化a来获取(forall x. Maybe x -> Maybe x)。

这不仅仅是类型系统的限制，mkT的实现也不支持这样的实例化。

mkT只是比较具体类型a和运行时的相等性b。但是你想要的是能够测试b是否等于某些x的Maybe x。这需要的逻辑从根本上说是更多的。但这肯定仍然是可能的。

下面，mkT1首先将类型b与App模式进行匹配，以了解b是否是某种类型应用程序g y，然后测试g和f的相等性：

{-# LANGUAGE ScopedTypeVariables, RankNTypes, TypeApplications, GADTs #-}
import Type.Reflection
-- N.B.: You can add constraints on (f x), but you must do the same for b.
mkT1 :: forall f b. (Typeable f, Typeable b) => (forall x. f x -> f x) -> (b -> b)
mkT1 h =
case typeRep @b of
App g y ->
case eqTypeRep g (typeRep @f) of
Just HRefl -> h
_ -> id
_ -> id

---

带有mkQ1的可编译示例：

{-# LANGUAGE ScopedTypeVariables, RankNTypes, TypeApplications, GADTs #-}
import Type.Reflection
mkT1 :: forall f b. (Typeable f, Typeable b) => (forall x. f x -> f x) -> (b -> b)
mkT1 h =
case typeRep @b of
App g y ->
case eqTypeRep g (typeRep @f) of
Just HRefl -> h
_ -> id
_ -> id
mkQ1 :: forall f b q. (Typeable f, Typeable b) => (forall x. f x -> q) -> (b -> q) -> (b -> q)
mkQ1 h =
case typeRep @b of
App g y ->
case eqTypeRep g (typeRep @f) of
Just HRefl -> const h
_ -> id
_ -> id
f :: Maybe x -> String
f _ = "matches"
main :: IO ()
main = do
print (mkQ1 f (_ -> "doesn't match") (Just 3 :: Maybe Int))  -- matches
print (mkQ1 f (_ -> "doesn't match") (3 :: Int))             -- doesn't match