受约束元素类型的构造函数 Class/Functor？

Question

这是一个常见问题解答 -- for example this answer；或 'Partial Type Constructors' [Jones, Morris, Eisenberg 2020] 中的第 3.2 节 'A Constraint for Well-Formed Applications'。而常见的答案是你做不到。我想我有点做到了。（但它并不漂亮。）

data Set a = NilSet | ConsSet a (Set a)    deriving (Eq, Show, Read)
mySet = ConsSet 'a' $ ConsSet 'b' $ ConsSet 'A' NilSet

我的 Set 类型不应该有重复的元素。所以如果我fmap toUpper mySet，我想避免两个'A'。然后考虑

添加： 回应评论。（下面保留原代码，供参考。）

@Carl [the restriction in the Language Report] applies only to constraints on exactly the type u.

是的，我什至没有尝试“完全输入 u”，因为我认为它会被禁止。但是......我现在可以处理@Fyodor 关于是否可能存在一些剩余限制的问题：

我需要的最少语言扩展是 MultiParamTypeClasses, FlexibleInstances——我对此很放心；他们是 long-standing/stable/well-tried。我什至不需要 FunctionalDependencies。这也适用于拥抱模式。

class Functorish2 f  where
  fmapish2 :: (FConstr2 f a b) => (a -> b) -> f a -> f b    -- huh? compiles ok
instance Functorish2 f  where                               -- needs FlexibleInstances
  fmapish2 = fmapish3

class FConstr2 f a b  where fmapish3 :: (a -> b) -> f a -> f b

-- IOW same signature as fmap. This gives me a free hand.

instance (Eq b) => FConstr2 Set a b  where                  -- needs FlexibleInstances
  fmapish3 f NilSet = NilSet
  fmapish3 f (ConsSet x xs) = uqCons (f x) (fmapish3 f xs)
    where uqCons fx xss | fElem fx xss = xss
                        | otherwise    = ConsSet fx xss
          fElem fx (ConsSet y ys) = fx == y || fElem fx ys
          fElem fx NilSet         = False

确实 fmapish2 toUpper mySet 消除了重复项。更现实地说，Set 实现将使用 BST 或哈希图或类似的东西，因此对元素的约束会比 Eq b 更复杂。尽管如此，似乎我可以对 Set.

的元素添加任何约束

还是有陷阱？这是我可以滥用导致类型不安全的错误吗？据推测，语言报告限制（下一段）不想让 fmapish2 的多态性低于 class 头部所指示的。

令人惊讶的是我标记为“啊？”的那一行。根据 2010 年语言报告第 4.3.1 节 'Class Declarations' 对方法签名的约束“cxi 可能仅约束 w-bar；在特别是，cxi 可能不会约束 u。” -- u 是来自 class 头部的 tyvar(s)。（顺便说一句，Set 上的 deriving (Eq) 不是必需的。）

第二个惊喜是，这不仅适用于 GHC (8.10.2, 7.10)，也适用于 Hugs (2006)。

（来自原始问题的代码。）

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

import Data.Char                                          -- toUpper

class Functorish f  where
  fmapish :: (FConstr (f b)) => (a -> b) -> f a -> f b    -- huh? compiles ok

class FConstr fb  where fMerge :: fb -> fb -> fb

instance Functorish Set  where
  fmapish f NilSet         = NilSet
  fmapish f (ConsSet x xs) = fMerge (ConsSet (f x) NilSet) (fmapish f xs)

instance (Eq a) => FConstr (Set a)  where            
  fMerge (ConsSet x NilSet) yss | fElem x yss = yss
                                | otherwise   = ConsSet x yss
        where fElem x (ConsSet y ys) = x == y || fElem x ys
              fElem x NilSet         = False

Answer 1

Functorish2 class 没有做任何有用的事情。您可以直接使用 fmapish3 来实现相同的目的。签名是

fmapish2 :: (Functorish2 f, FConstr2 f a b) => (a -> b) -> f a -> f b

但是因为你给了 every f :: Type -> Type 一个实例 Functorish2 f，这实际上并没有限制任何东西，你确实可以再写一次

fmapish :: FConstr2 f a b => (a -> b) -> f a -> f b
fmapish = fmapish2

IOW，你所有的问题（在 2021-08-04 01:10:56Z 的编辑版本中）都是关于 MultiParamTypeClasses 是否足以表达受约束的函子。我会回答，有点。他们可以表达任何给定情况的约束，尽管我希望总是随身携带三个 f、a 和 b 会很快变得尴尬。

在实践中，实例可能倾向于具有以下形式

instance (FDomCstr a, FCodomCstr b) => FConstr2 F a b where
  ...

所以也许实际上这样布局会更好：

{-# LANGUAGE ConstraintKinds, TypeFamilies #-}

import Data.Kind (Type, Constraint)

class CFunctor f where
  type DomCstr f a :: Constraint
  type DomCstr f a = ()
  type CodomCstr f b :: Constraint
  type CodomCstr f b = ()
  cfmap :: (DomCstr f a, CodomCstr f b) => (a -> b) -> f a -> f b

instance CFunctor Set where
  type CodomCstr Set a = Ord a
  cfmapish3 f NilSet = NilSet
  cfmapish3 f (ConsSet x xs) = ...

Answer 2

The surprise is the line I've marked "huh?". According to the 2010 Language Report Section 4.3.1 'Class Declarations' constraints on method signatures "The cxi may constrain only w-bar; in particular, the cxi may not constrain u." -- the u being the tyvar(s) from the class head. (BTW the deriving (Eq) on Set isn't essential.)

将我的评论变成答案，我认为相关的 GHC 扩展称为 ConstrainedClassMethods，由 MultiParamTypeClasses 隐含。

例如，这段代码无法编译：

class Test a where
  test :: Eq a => a -> a -> Bool

你会得到错误：

Test.hs:2:3: error:
    • Constraint ‘Eq a’ in the type of ‘test’
        constrains only the class type variables
      Enable ConstrainedClassMethods to allow it
    • When checking the class method:
        test :: forall a. (Test a, Eq a) => a -> a -> Bool
      In the class declaration for ‘Test’
  |
2 |   test :: Eq a => a -> a -> Bool
  |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

如果启用 ConstraintClassMethods 则它会编译。

在你的例子中 ConstraintedClassMethods 是由 MultiParamTypeClasses 暗示的，这也修复了这个测试示例中的错误。

但即使没有它，它也会编译，因为 FConstr2 f a b 约束不仅仅约束实例头中提到的变量。从链接的 GHC 指南中查看此示例，特别是 op5:

class C a where
  op3 :: Eq a => a -> a    -- Rejected: constrains class variable only
  op4 :: D b => a -> b     -- Accepted: constrains a locally-quantified variable `b`
  op5 :: D (a,b) => a -> b -- Accepted: constrains a locally-quantified variable `b`

所以约束FConstr2 f a b也会被接受，因为它约束了局部量化变量a和b.

受约束元素类型的构造函数 Class/Functor？

Constructor Class/Functor for a constrained element type?

haskell

functor

typeclass