haskell - 了解类型族

Question

我正在学习类型族并试图理解为什么在特定情况下我没有收到编译时错误。

我的类型族定义如下:

type family Typ a b :: Constraint
type instance Typ (Label x) (Label y) = ()

我有两个功能如下:

func1 :: (Typ (Label "la") (Label "lb")) => Label "la" -> Label "lb" -> String
func1  = undefined

func2 :: (Typ (Label "la") String) => Label "la" -> String -> String
func2  = undefined

这两个函数都可以编译。

当我尝试查看 func1 的类型时，我得到正确的签名。但是，当我尝试查看 func2 的类型时，我收到以下错误

Could not deduce (Typ (Label "la") String)

为什么会这样？有人可以帮我理解吗？

Answer 1

我能够用 Label 的定义复制您所描述的内容:

import GHC.TypeLits (Symbol)

data Label (a :: Symbol)

并添加:

type instance Typ (Label x) String = ()

然后提供 func2的类型

编辑

对不起，我误解了这个担忧。我的理解是，检查约束的可满足性将推迟到 func2实际使用，因为可以稍后添加实例。

例如，添加:

func3 = func2 (undefined :: Label "la") ""

导致它在编译时失败。

我理解它的方式是 func2是说，如果你给我一个 Label "la"和 String和 Typ (Label "la") String 的实例当时在范围内，我给你一个 String .但是 func2不需要在范围内有一个实例来知道如果它有它会做什么。