1

一般来说，我想知道是否有一种方法可以编写通用折叠来概括应用以下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)。

4

1 回答 1

2

tldr：您需要创建一个不同的函数。

mkT具有以下签名：

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

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

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

mkT只是在运行时比较具体类型a和相等性。b但是你想要的是能够测试是否b等于Maybe xfor some x。这需要的逻辑从根本上更复杂。但这当然仍然是可能的。

下面，mkT1首先将类型b与App模式匹配以了解是否b为某种类型 application g y，然后测试 and 的相等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
于 2020-02-04T14:08:28.333 回答