在SYB中匹配较高种类的类型

Question

[总的来说，我想知道是否有一种方法可以编写泛型折叠来泛化应用forall类型的函数，例如：

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

给定D的某些数据类型instance 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的Maybe x是否等于x。从根本上讲，这需要更多的逻辑。 但是肯定仍然可能。

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

-- N.B.: You can add constraints on (f x), but you must do the same for b.
mkT1 :: (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