在Haskell中使用Forall

Question

Data.Constraint.Forall提供了一些对约束的量化，但是我不知道如何使用它。请考虑以下几点：

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}

module Forall where

import Prelude
import Data.Constraint.Forall

class Monoid (f a) => MonoidalFunctor f a

testfun :: Forall (MonoidalFunctor f) => (a -> f a) -> [a] -> f a
testfun = foldMap

testfun' :: Monoid (f a) => (a -> f a) -> [a] -> f a
testfun' = foldMap

我以为testfun会检查类型，因为Forall (MetaMonoid f)会像forall a. Metamonoid f a一样工作，因为超类约束，这意味着forall a. Monoid (f a)，但事实并非如此。

为什么它不能工作，有什么解决方法吗？我希望避免在我的函数中为不同的MyData类型编写很多约束，比如MyClass (f MyData)，因为我知道任何有用的f都会有任何f MyData的实例。

Answer 1

使用inst

inst :: forall p a. Forall p a :- p a

inst可以证明，如果您有forall a. p a，那么您可以将a设置为任何您喜欢的值，并将p a去掉。

蕴涵(:-)是

newtype a :- b = Sub (a => Dict b)
data Dict a = a => Dict

因此，通过对其进行模式匹配，您可以揭示其中的实例：

testfun :: forall f a. Forall (MonoidalFunctor f) => (a -> f a) -> [a] -> f a
testfun = case inst @(MonoidalFunctor f) @a of Sub Dict -> foldMap

(键入必要的应用程序/签名)，或者您可以使用(\\)

(\\) :: a => (b => r) -> a :- b -> r
testfun = foldMap \\ inst @(MonoidalFunctor f) @a

它是这样的：“给定a为true，并且r的值也需要b为true，然后是一个可以证明b为true的值(给定a )，创建一个r。

(\\) :: (b => c) -> (a :- b) -> (a => c)

它看起来有点像函数组合。

出现这种现象的原因很简单，因为GHC无法推断Forall c意味着它可以为任何a派生c a；毕竟，这就是constraints存在的原因。所以，你必须对它更明确一点。