haskell - 部分应用类型与种类 (* -> 约束)

Question

考虑以下代码:

class Foo f
class Bar b

newtype D d = D

call :: Proxy c -> (forall a . c a => a -> Bool) -> x -> Bool
call g x = g x

-- this function is Testable, and can be used by QuickCheck
f :: (Foo (D d), Bar d) => D d -> Bool
f = error ""

//assume the type FConstraint has kind (* -> Constraint)

main = print $ call (Proxy::Proxy FConstraint) (unsafeCoerce f) (D::D 17)

这种奇怪函数的目的是能够使用 QuickCheck 轻松测试多态函数(例如 f ): call将在单态类型的类型列表上进行迭代，并且该列表可以用于多个不同的属性(均采用单个参数)，而无需每次都明确写出类型签名。由于这只出现在测试代码中，我愿意使用 unsafeCoerce (虽然我不确定它会在这一点上做我想做的事。我需要先解决下面的问题)。

我当然愿意接受 call 的更好/替代设计，但这是我关于上面提出的解决方案的问题:我需要一个类型 FConstraint与善 (* -> Constraint)可用于 call 的第一个参数.

这是我尝试过的:

type FConstraint x = (Foo x, Bar ??)
type FConstraint (D d) = (Foo (D d), Bar d)

类型同义词都不起作用，因为我需要对类型进行模式匹配才能获得所有约束，并且还需要部分应用 FConstraint ，这两种类型的同义词都不允许。

我也试过一个类型系列:

type family FConstraint x
type instance FConstraint (D d) = (Foo (D d), Bar d)

但我仍然不能部分应用它(我也不能使用封闭的类型系列)。

因此我需要一种类型 (* -> Constraint)哪一个

模式匹配种类的类型 *

可以部分应用

更新

这是使用以下答案中的想法的几乎可以编译的示例:

{-# LANGUAGE RankNTypes, ScopedTypeVariables, ConstraintKinds, TypeOperators,
             MultiParamTypeClasses, DataKinds, PolyKinds, FlexibleInstances,
             UndecidableInstances, FlexibleContexts, TypeFamilies,
             FunctionalDependencies #-}

import Control.Monad
import Data.Proxy
import GHC.Prim
import GHC.TypeLits
import Test.QuickCheck
import Test.Framework
import Test.Framework.Providers.QuickCheck2
import Unsafe.Coerce

newtype Zq q = Zq Integer deriving (Show, Eq)

instance (KnownNat q) => Arbitrary (Zq q) where
  arbitrary = liftM (\i -> Zq $ (i `mod` (natVal (Proxy::Proxy q)))) arbitrary

instance (KnownNat q) => Num (Zq q) where
  (Zq a) + (Zq b) = Zq $ (a + b) `mod` (natVal (Proxy::Proxy q))
  (Zq a) * (Zq b) = Zq $ (a * b) `mod` (natVal (Proxy::Proxy q))
  negate (Zq 0) = (Zq 0)
  negate (Zq a) = Zq $ (natVal (Proxy::Proxy q)) - a
  fromInteger x = Zq $ x `mod` (natVal (Proxy::Proxy q))

f :: (KnownNat q) => Zq q -> Zq q
f x = x + 1

finv :: (KnownNat q) => Zq q -> Zq q
finv x = x - 1

prop_f :: forall q . (KnownNat q) => Zq q -> Bool
prop_f x = (finv . f) x == x

call :: (c x) => Proxy (c :: * -> Constraint) -> 
        (forall a . c a => a -> Bool) -> 
        x -> 
        Bool
call _ f = f

class UnZq zq q | zq -> q
instance UnZq (Zq q) q

class FConstraint x
instance (KnownNat q, UnZq zq q) => FConstraint zq

main = defaultMain $ [testProperty "zq_f_id" $ property $
         (call (Proxy::Proxy FConstraint) $ unsafeCoerce prop_f :: Zq 3 -> Bool)]

我收到错误:

Could not deduce (KnownNat q0) arising from a use of ‘prop_f’
from the context (FConstraint a)

我希望这是一个简单的范围界定问题...

这是用例的更多代码:

type MyTypes = '[ Zq 3, Zq 5, Zq 7, Zq 11 ] 

class TypesToProps xs c where
  tmap :: Proxy xs -> Proxy c -> (forall a . c a => a -> Bool) -> [Property]

instance TypesToProps '[] c where
  tmap _ _ _ = []

instance (c x, TypesToProps xs c, Arbitrary x, Show x)
    => TypesToProps (x ': xs) c where
  tmap _ c f = (property (call c f :: x -> Bool)) : (tmap (Proxy::Proxy xs) c f)

-- results in same error as the `main` above
main = defaultMain $ map (testProperty "zq_f_id") $ 
         tmap (Proxy::Proxy MyTypes) 
              (Proxy::Proxy FConstraint) 
              (unsafeCoerce prop_f)

Answer 1

首先，您的 call函数不编译，也不应该编译:无法推断 c x在类型 Proxy c -> (forall a . c a => a -> Int) -> x -> Int所以你不能通过 x至 f .

接下来，您使用 unsafeCoerce在这里无效。如果看unsafeCoerce的类型你在哪里使用过它:

withCall 
  :: (forall d . (Foo (D d), Bar d) => D d -> Bool) 
  -> (forall a . FConstraint a => a -> Int)
withCall = unsafeCoerce

你投 D d到任何类型和 Bool至 Int . (请注意，这需要 ImpredictiveTypes)。我不明白你的用例，所以我不能说是否有比 unsafeCoerce 更好的解决方案，但我可以说你正在做的事情可能会在你的脸上爆炸。

写实 FConstraint相当简单:

class UnD x (y :: Nat) | x -> y 
instance UnD (D x) x 

class FConstraint x
instance (Foo x, Bar t, UnD x t) => FConstraint x

完整代码:

{-# LANGUAGE 
    UndecidableInstances
  , ImpredicativeTypes
  , MultiParamTypeClasses
  , FunctionalDependencies 
  #-}

import Unsafe.Coerce 
import GHC.Exts (Constraint)
import Data.Proxy 
import GHC.TypeLits 

class Foo f
class Bar (b :: Nat)

data D (d :: Nat) = D

call :: Proxy (c :: * -> Constraint) -> (forall a . c a => a -> Int) -> x -> Int
call = undefined

f :: (Foo (D d), Bar d) => D d -> Bool
f = error ""

withCall :: (forall d . (Foo (D d), Bar d) => D d -> Bool) -> (forall a . FConstraint a => a -> Int)
withCall = unsafeCoerce

class UnD x (y :: Nat) | x -> y 
instance UnD (D x) x 

class FConstraint x
instance (Foo x, Bar t, UnD x t) => FConstraint x

main = print $ call (Proxy :: Proxy FConstraint) (withCall f) (D :: D 17)

为了响应您的更新，立即显而易见的事情是重构您的 TypesToProps类(class):

class TypesToProps xs (c :: k -> Constraint) (t :: k -> *) where
  tmap :: Proxy xs -> Proxy c -> Proxy t -> (forall a . c a => t a -> Bool) -> [Property]

instance TypesToProps '[] c t where
  tmap _ _ _ _ = []

instance (c x, TypesToProps xs c t, Arbitrary (t x), Show (t x)) => TypesToProps (x ': xs) c t where
  tmap _ c t f = property (f :: t x -> Bool) : tmap (Proxy :: Proxy xs) c t f

main = defaultMain $ map (testProperty "zq_f_id") $ 
  tmap (Proxy :: Proxy '[3, 5, 7, 11]) 
       (Proxy :: Proxy KnownNat) 
       (Proxy :: Proxy Zq)
       prop_f

这可能不够通用，但它不需要使用 unsafeCoerce .

当你写 unsafeCoerce prop_f ，类型检查器要求 KnownNat q约束在它可以做任何事情之前得到满足。您必须保留对结果类型的约束 - 这与您正在做的事情根本不兼容 - 或者首先删除约束。

您可以将约束存储为数据(对于多态函数，这就是它们在内部存储的方式):

data Dict p where 
  Dict :: p => Dict p 

我们可以使用此数据类型删除约束:

anyDict :: Dict p 
anyDict = unsafeCoerce (Dict :: Dict (Eq ()))

prop_f' :: forall q . Zq q -> Bool
prop_f' q = case anyDict :: Dict (KnownNat q) of Dict -> prop_f q 

通常这将是不安全的，但在这种特定情况下它实际上是安全的，因为 q在 Zq q是一个幻影参数，并使用任何涉及 Zq您需要挑选混凝土 q无论如何，这将消除类约束。

然后你可以写

class TypesToProps xs where
  tmap :: Proxy xs -> (forall a . a -> Bool) -> [Property]

instance TypesToProps '[] where
  tmap _ _ = []

instance (TypesToProps xs, Arbitrary x, Show x) => TypesToProps (x ': xs) where
  tmap _ f = property (f :: x -> Bool) : tmap (Proxy :: Proxy xs) f where

注意函数 forall a . a -> Bool无人居住，因此您只能使用 unsafe 生成该类型的值职能。这意味着不可能使用 tmap 用脚射击自己。独自的;除非您使用不安全的函数，否则您将永远无法实例化 tmap .最后:

main = defaultMain $ map (testProperty "zq_f_id") $ 
  tmap (Proxy :: Proxy '[Zq 3, Zq 5, Zq 7, Zq 11]) 
       (unsafeCoerce prop_f' :: forall a . a -> Bool)