了解类型系列

Question

我正在学习Type Families并试图理解为什么我在特定情况下没有得到编译时错误.

我的类型系列定义如下:

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,我得到错误以下错误

无法推断(Typ(标签"la")字符串)

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

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，如果你给我 aLabel "la"和 a并且当时String 的范围内有一个实例Typ (Label "la") String，我会给你 a String。但func2不需要在范围内有一个实例就可以知道如果有实例它会做什么。