使用具有等式约束的 Data.Constraint.Forall答案

【问题标题】：Using Data.Constraint.Forall with equality constraints使用具有等式约束的 Data.Constraint.Forall
【发布时间】：2015-01-21 20:59:57
【问题描述】：

假设我有一个这样的函数：

{-# LANGUAGE ScopedTypeVariables #-}

class C a where

foo :: forall f a b. (C (f a), C (f b)) => f a -> f b
foo = _

现在，如果我想将a 和b 的范围移动到foo 类型中typeclass 约束的右侧（比如说，因为我想使用foo 来实现一个typeclass 方法需要在a 和b 中是多态的），它可以使用Data.Constraint.Forall 完成一些工作：

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ConstraintKinds, TypeOperators #-}
import Data.Constraint
import Data.Constraint.Forall

foo' :: forall f. (ForallF C f) => forall a b. f a -> f b
foo' = helper
  where
    helper :: forall a b. f a -> f b
    helper = case (instF :: ForallF C f :- C (f a)) of
        Sub Dict -> case (instF :: ForallF C f :- C (f b)) of
            Sub Dict -> foo

现在，我的问题是，假设我将函数更改为涉及类型等式的函数：

{-# LANGUAGE TypeFamilies, ScopedTypeVariables #-}

type family F a :: * -> *

bar :: forall f g a b. (F (f a) ~ g a, F (f b) ~ g b) => f a -> f b
bar = _

有没有办法让上述技术适应这种情况？

这是我尝试过的：

{-# LANGUAGE TypeFamilies, ScopedTypeVariables #-}
{-# LANGUAGE ConstraintKinds, TypeOperators #-}
import Data.Constraint
import Data.Constraint.Forall

type F'Eq f g x = F (f x) ~ g x

bar' :: forall f g. (Forall (F'Eq f g)) => forall a b. f a -> f b
bar' = helper
  where
    helper :: forall a b. f a -> f b
    helper = case (inst :: Forall (F'Eq f g) :- F'Eq f g a) of
        Sub Dict -> case (inst :: Forall (F'Eq f g) :- F'Eq f g b) of
            Sub Dict -> bar

但是（不出所料）这会因为不饱和类型的同义词而失败：

类型同义词‘F'Eq’应该有3个参数，但已经给了2个

在表达式类型签名中：Forall (F'Eq f g) :- F'Eq f g a

在表达式中：(inst :: Forall (F'Eq f g) :- F'Eq f g a)

【问题讨论】：

标签： haskell typeclass type-families

【解决方案1】：

你可以使用一个类：

{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, FlexibleContexts #-}

class (F (f x) ~ g x) => F'Eq f g x
instance (F (f x) ~ g x) => F'Eq f g x

bar' :: forall f g. (Forall (F'Eq f g)) => forall a b. f a -> f b
bar' = helper
  where
    helper :: forall a b. f a -> f b
    helper = case (inst :: Forall (F'Eq f g) :- F'Eq f g a) of
        Sub Dict -> case (inst :: Forall (F'Eq f g) :- F'Eq f g b) of
            Sub Dict -> bar

【讨论】：