haskell - 类型缩减无限循环

Question

我的目标是消除()从条款来看，像这样:

(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类型家庭应该照顾不可约的条款，但我显然遗漏了一些东西。但是什么？

Answer 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)