具有种类的部分应用类型 (* -> 约束)



考虑以下代码:

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) 

最新更新