考虑以下代码:
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)
首先,call
函数没有编译,也不应该编译:在类型Proxy c -> (forall a . c a => a -> Int) -> x -> Int
中无法推断c x
,因此无法将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
。(请注意,这需要ImpdictiveTypes(。我不理解你的用例,所以我不能说是否有比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 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
一般来说,这是不安全的,但在这种特定情况下,它实际上是安全的,因为Zq q
中的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)