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

Question

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

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

给定 instance Data (D a) 的某些数据类型 D（可能对 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 => ... 的局限性——我的理解是 Maybe a 居住的任何类型的实例 Data 也必须具有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 相等：

-- 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

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

Matching higher-kinded types in SYB

haskell

generic-programming

scrap-your-boilerplate

rank-n-types