时间戳

首页 > 解决方案 > 为什么关联类型同义词不暗示约束

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

问题描述

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

例如，为什么以下内容不能编译：

{-# 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 文档似乎没有提到这方面。

标签： haskelltype-families

解决方案

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

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

显然一无所知MyClass，但应该可以sort :: [AssociatedType a] -> [AssociatedType a]在Ord (AssociatedType a)调用范围内使用它。

要获得您似乎正在寻找的行为，您需要一个包装的约束而不是关联的类型。这不能用 来完成-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您也可以使用库中的包装器，而不是自卷包装器：

import Data.Constraint

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

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

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

推荐阅读