此图片中F的多种类型？

发布于 2025-02-14 00:01:49 字数 578 浏览 0 评论 0原文

data T a where
  T1 :: Bool -> T Bool
  T2 :: T a

f x y = case x of
  T1 x -> True
  T2   -> y

Simon在f 可以键入t a - ＆gt; a - ＆gt;一个，但我认为返回值必须是一个布尔，因为这是案例表达式分支的明确结果。这是关于Haskell Gadts的。为什么这样？

原文

https://youtu.be/brE_dyedGm0?t=1362

data T a where
  T1 :: Bool -> T Bool
  T2 :: T a

f x y = case x of
  T1 x -> True
  T2   -> y

Simon is saying that f could be typed as T a -> a -> a, but I would think the return value MUST be a Bool since that is an explicit result in a branch of the case expression. This is in regards to Haskell GADTs. Why is this the case?

分享到QQ

分享到微博

如果你对这篇内容有疑问，欢迎到本站社区发帖提问参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

发布评论

需要登录才能够评论，你可以免费注册一个本站的账号。

吖咩 2025-02-21 00:01:49

这是Gadts的重点。在构造函数上匹配可以导致其他类型的信息范围。

让我们看一下GHC检查以下定义时会发生什么：

f :: T a -> a -> a
f x y = case x of
    T1 _ -> True
    T2   -> y

让我们首先查看t2案例，只是为了使其脱离。 y，结果具有相同的类型，t2是多态的，因此您可以声明其类型也是t a。一切都很好。

然后是更棘手的情况。请注意，我删除了case内的名称x的绑定，因为阴影可能会令人困惑，不使用内部值，并且不会更改任何内容解释。当您在GADT构造函数上匹配t1（明确设置类型变量）时，它会在该分支中引入其他约束，从而添加该类型信息。在这种情况下，匹配t1介绍了（a〜bool）约束。这种类型的平等说a和bool相互匹配。因此，具有字体true带有类型bool匹配a在类型签名中匹配。 y不使用，因此该分支与t a - ＆gt; a - ＆gt;。

所以一切都匹配了。 t a - ＆gt; a - ＆gt;是该定义的有效类型。但是正如西蒙所说的那样，这是模棱两可的。 t a - ＆gt;布尔 - ＆gt; bool也是该定义的有效类型。两个都不是另一个更一般的，因此定义没有原理类型。因此，除非提供类型，否则将拒绝该定义，因为推理无法为其选择一种最校正的类型。

This is kind of the whole point of GADTs. Matching on a constructor can cause additional type information to come into scope.

Let's look at what happens when GHC checks the following definition:

f :: T a -> a -> a
f x y = case x of
    T1 _ -> True
    T2   -> y

Let's look at the T2 case first, just to get it out of the way. y and the result have the same type, and T2 is polymorphic, so you can declare its type is also T a. All good.

Then comes the trickier case. Note that I removed the binding of the name x inside the case as the shadowing might be confusing, the inner value isn't used, and it doesn't change anything in the explanation. When you match on a GADT constructor like T1, one that explicitly sets a type variable, it introduces additional constraints inside that branch which add that type information. In this case, matching on T1 introduces a (a ~ Bool) constraint. This type equality says that a and Bool match each other. Therefore the literal True with type Bool matches the a written in the type signature. y isn't used, so the branch is consistent with T a -> a -> a.

So it all matches up. T a -> a -> a is a valid type for that definition. But as Simon is saying, it's ambiguous. T a -> Bool -> Bool is also a valid type for that definition. Neither one is more general than the other, so the definition doesn't have a principle type. So the definition is rejected unless a type is provided, because inference cannot pick a single most-correct type for it.

回复收藏 0 原文

凉城已无爱 2025-02-21 00:01:49

类型t a带有a与bool不同的值永远不会具有表单t1 x（因为那是仅类型t bool）。

因此，在这种情况下，t1 x case中的分支变得无法访问，在类型检查/推理期间可以忽略。

更具体地：GADT允许类型检查器在模式匹配过程中假设类型级方程，并在以后利用此类方程式。当检查

f :: T a -> a -> a
f x y = case x of
  T1 x -> True
  T2   -> y

类型检查器执行以下推理时：

f :: T a -> a -> a
f x y = case x of
  T1 x -> -- assume: a ~ Bool
          True  -- has type Bool, hence it has also type a
  T2   -> -- assume: a~a  (pointless)
          y     -- has type a

多亏了GADTS，案例的两个分支都具有a的类型，因此整个情况表达式具有类型a和函数定义类型检查。

更一般而言，当X :: T A和GADT构造函数定义为k :: ... ...-＆gt; T b然后，当类型检查时，我们可以做出以下假设：

case x of
  K ... ->  -- assume: A ~ B

请注意，a和b可以是涉及类型变量的类型（如a〜中上面的bool），因此允许获得有关它们的有用信息，并以后进行利用。

A value of type T a with a different from Bool can never have the form T1 x (since that has only type T Bool).

Hence, in such case, the T1 x branch in the case becomes inaccessible and can be ignored during type checking/inference.

More concretely: GADTs allow the type checker to assume type-level equations during pattern matching, and exploit such equations later on. When checking

f :: T a -> a -> a
f x y = case x of
  T1 x -> True
  T2   -> y

the type checker performs the following reasoning:

f :: T a -> a -> a
f x y = case x of
  T1 x -> -- assume: a ~ Bool
          True  -- has type Bool, hence it has also type a
  T2   -> -- assume: a~a  (pointless)
          y     -- has type a

Thanks to GADTs, both branches of the case have type a, hence the whole case expression has type a and the function definition type checks.

More generally, when x :: T A and the GADT constructor was defined as K :: ... -> T B then, when type checking we can make the following assumption:

case x of
  K ... ->  -- assume: A ~ B

Note that A and B can be types involving type variables (as in a~Bool above), so that allows one obtain useful information about them and exploit it later on.

回复收藏 0 原文

~没有更多了~