类型缩减无限循环答案

【问题标题】：Type reduction infinite loop类型缩减无限循环
【发布时间】：2016-09-08 16:37:09
【问题描述】：

我的目标是从术语中删除()，如下所示：

(a, b)       -> (a, b)
((), b)      -> b
(a, ((), b)) -> (a, b)
...

这是代码：

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module Simplify where

import Data.Type.Bool
import Data.Type.Equality

type family Simplify x where
  Simplify (op () x) = Simplify x
  Simplify (op x ()) = Simplify x
  Simplify (op x y)  = If (x == Simplify x && y == Simplify y)
                          (op x y)
                          (Simplify (op (Simplify x) (Simplify y)))
  Simplify x         = x

但是，尝试一下：

:kind! Simplify (String, Int)

...导致类型检查器中的无限循环。我在想If 类型家族应该处理不可约的条款，但我显然遗漏了一些东西。但是什么？

【问题讨论】：

您似乎假设类型级计算是惰性的，因此除非需要，否则不会评估 If 的第二个分支。我认为这种假设是没有根据的。
顺便说一句：在op 上进行多态可能是错误的。例如，Simplify (Either () Int) 可能不应该简化为 Int。
(String, (), Int) 上的行为应该是什么？到目前为止，建议的两种解决方案都将其减少到Int。不知道能不能得到(String, Int)。
@gallais：没关系，术语只能是（嵌套）元组。

标签： haskell infinite-loop typechecking type-families

【解决方案1】：

类型族评估并不懒惰，因此If c t f 将评估所有c、t 和f。（事实上，类型族评估顺序现在根本没有真正定义。）所以难怪你最终会陷入无限循环——你总是评估Simplify (op (Simplify x) (Simplify y))，即使那是Simplify (op x y)！

您可以通过将递归和简化分开来避免这种情况，如下所示：

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module Simplify where

import Data.Type.Bool
import Data.Type.Equality

type family Simplify1 x where
  Simplify1 (op () x) = x
  Simplify1 (op x ()) = x
  Simplify1 (op x y)  = op (Simplify1 x) (Simplify1 y)
  Simplify1 x         = x

type family SimplifyFix x x' where
  SimplifyFix x x  = x
  SimplifyFix x x' = SimplifyFix x' (Simplify1 x')

type Simplify x = SimplifyFix x (Simplify1 x)

想法是：

Simplify1 做了一步简化。
SimplifyFix 接受x 及其一步化简x'，检查它们是否相等，如果不相等，则进行另一步化简（从而找到Simplify1 的不动点）。
Simplify 只是从 SimplifyFix 链开始，调用 Simplify1。

由于类型族模式匹配是惰性的，SimplifyFix 正确地延迟评估，防止无限循环。

确实：

*Simplify> :kind! Simplify (String, Int)
Simplify (String, Int) :: *
= (String, Int)

*Simplify> :kind! Simplify (String, ((), (Int, ())))
Simplify (String, ((), (Int, ()))) :: *
= ([Char], Int)

【讨论】：

哇，我也在写一个答案......并且想出了 exactly 第二个测试用例的相同选择。对于它的价值，我认为我的答案稍微简单一些，尽管可能不太普遍：Simplify1 ((), y) = y; Simplify1 (x, ()) = x; Simplify1 other = other; Simplify (x, y) = Simplify1 (Simplify x, Simplify y); Simplify other = other。
@DanielWagner 我的意思是，您必须将()s 嵌套至少两层才能进行真正的测试，对吧？ :-) 很高兴比较您的解决方案！
还有一个有趣的魔法：:kind! forall a. Simplify1 (a, ()) = a。这需要一些真正的聪明，因为它必须注意Simplify1 的前两个子句会给出相同的答案！
@DanielWagner：……这让我很困惑。我真的觉得这根本不应该工作！
@DanielWagner，它可能重用了一些用于检查开放类型族的相同 RHS 逻辑。有点出乎意料，我想知道它在哪里喊着“惊喜！”并崩溃，但绝对很酷。

【解决方案2】：

我想我会提到，鉴于简化具有折叠的结构，因此没有必要构建这种复杂的解决方案，其中涉及一次又一次地重新遍历表达式的固定点。

这样就可以了：

{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE UndecidableInstances #-}
module Simplify where

type family Simplify x where
  Simplify (op a b) = Op op (Simplify a) (Simplify b)
  Simplify x        = x

type family Op op a b where
  Op op () b = b
  Op op a () = a
  Op op a b  = op a b

【讨论】：