haskell - 为什么关联类型同义词不暗示约束

Question

为什么在签名中使用关联类型同义词不暗示相应的约束？

例如为什么不编译以下内容:

{-# LANGUAGE TypeApplications, ScopedTypeVariables, TypeFamilies, AllowAmbiguousTypes #-}

class MyClass a where
  type AssociatedType a 
  bar :: Int

foo :: forall a. AssociatedType a -> Int
foo _ = bar @a

ghc 8.6.5 出现以下错误:

error:
    * No instance for (MyClass a) arising from a use of `bar'
      Possible fix:
        add (MyClass a) to the context of
          the type signature for:
            foo :: forall a. AssociatedType a -> Int
    * In the expression: bar @a
      In an equation for `foo': foo _ = bar @a
  |
8 | foo _ = bar @a
  |         ^^^^^^

GHC 文档好像没有提到这方面。

Answer 1

如果它暗示了约束，那么任何人以任何方式使用关联值的值都需要在范围内有约束。例如，

sort :: Ord a => [a] -> [a]

显然对 MyClass 一无所知，但如果您有 Ord (AssociatedType a) 在 calling 范围内。

要获得您似乎正在寻找的行为，您需要一个包装约束而不是关联类型。这不能用 -XTypeFamilies 完成，但可以用 -XGADTs 完成:

{-# LANGUAGE GADTs #-}

class MyClass a where
  bar :: Int

data MyClassWitness a where
  MyClassWitness :: MyClass a => MyClassWitness a

foo :: ∀ a. MyClassWitness a -> Int
foo MyClassWitness = bar @a

除了自卷包装外，您还可以使用 constraints library 中的包装。 :

import Data.Constraint

foo :: ∀ a . Dict (MyClass a) -> Int
foo Dict = bar @a

在这两种情况下，重要的是您实际上是在 GADT 构造函数上进行模式匹配，因为只有这样才能真正将约束带入范围。这将不工作:

foo :: ∀ a . Dict (MyClass a) -> Int
foo _ = bar @a