双向加法约束
最近关于 Reddit 的一个问题引发了关于如何产生约束函数的讨论
type AddUp :: Nat -> Nat -> Nat -> Constraint
-- given
data Nat = Z | S Nat
type family m + n where
'Z + n = n
'S m + n = 'S (m + n)
以至于
AddUp m n o意味着m + n = o.- 任何关于
m、n和/ 或 的可用类型信息o都将尽可能地流向其他人。
最棘手的部分是＃2，和那最棘手的部分是，如果我们知道，例如，m ~ 'S x和n ~ 'S ('S y)，那么我们就应该从推断AddUp m n o这o ~ 'S ('S ('S z))对于一些z。
使用不连贯的实例很容易做到这一点，如下/u/Tarmen所示：
class AddUp m n o
instance {-# INCOHERENT #-} n ~ o => AddUp 'Z n o
instance {-# INCOHERENT #-} m ~ o => AddUp m 'Z o
instance {-# INCOHERENT #-} (o ~ 'S po, AddUp m n po) => AddUp ('S m) n o
instance {-# INCOHERENT #-} (o ~ 'S po, AddUp m n po) => AddUp m ('S n) o
instance {-# INCOHERENT #-} (m ~ 'Z, n ~ 'Z) => AddUp m n 'Z
不连贯实例的这种特殊使用是完全安全的，但不连贯实例通常是一种相当阴暗的语言特征。有可能避免它们吗？
回答
是的，我们可以做到！诀窍是通过匹配产生了一堆的等式约束m，并n在我们都能方式并行。这是一个天真的第一次尝试：
type AddUp m n o = (Bar m n o, Bar n m o, Baz m n o)
type family Bar m n o where
Bar 'Z n o = n ~ o
Bar ('S m) n o = (o ~ 'S (Pred o), AddUp m n (Pred o))
type family Baz m n o :: Constraint where
Baz m n 'Z = (m ~ 'Z, n ~ 'Z)
Baz _ _ _ = ()
type family Pred n where
Pred ('S n) = n
这确实有效，但它有一个大问题：编译需要指数级（或更糟）的时间和空间！有什么问题？考虑一下AddUp ('S m) ('S n) o，让我们暂时忽略Baz。这产生Bar ('S m) ('S n) o和Bar ('S n) ('S m) o。第一个减少到(o ~ S (Pred o), AddUp m (S n) (Pred o))而第二个减少到(o ~ S (Pred o), AddUp n (S m) (Pred o))。展开AddUp，我们看到一个产生，除其他外Bar (S n) m (Pred o)，，而另一个产生，除其他外，Bar (S m) n (Pred o)。当这些反过来减少时，它们产生（除其他外）AddUp n m (Pred o)和AddUp m n (Pred o)，它们是等价的。
我们怎样才能解决这个问题？我们需要Bar分成两个类型家族，其中第二个类型家族在匹配方面受到更多限制。
type AddUp m n o = (Bar m n o, Barf n m o, Baz m n o)
type family Bar m n o where
Bar 'Z n o = n ~ o
Bar ('S m) n o = (o ~ 'S (Pred o), AddUp m n (Pred o))
-- A version of Bar that refrains from matching on the second argument.
-- This is necessary to avoid exponential constraint size.
type family Barf m n o where
Barf 'Z n o = n ~ o
Barf ('S m) n o = (o ~ 'S (Pred o), Barf m n (Pred o), Baz m n (Pred o))
-- These are the same
type family Baz m n o :: Constraint where
Baz m n 'Z = (m ~ 'Z, n ~ 'Z)
Baz _ _ _ = ()
type family Pred n where
Pred ('S n) = n
我相信这个版本只需要多项式时间（至少是二次的），而不是指数。或者，一旦所有的统一工作等都考虑在内，可能会从更糟的情况以指数顺序减少它。在实践中，它比使用不连贯实例的版本慢得多，但比天真的版本快得多。