您的重构与 Luke Palmer 的这篇博文密切相关：“Haskell Antipattern: Existential Typeclass”。
我认为我们可以证明您的重构将始终有效。为什么？直观地说，因为如果某种类型Foo包含足够的信息以便我们可以将其变成您的Problem类的实例，我们总是可以编写一个Foo -> Problem函数，将“投影”Foo的相关信息转换为Problem包含所需信息的确切信息。
更正式一点，我们可以草拟一个证明，证明你的重构总是有效的。首先，为了做好准备，以下代码定义了将Problem类实例转换为具体CanonicalProblem类型：
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
class Problem p s a where
initial :: p s a -> s
successor :: p s a -> s -> [(a,s)]
goaltest :: p s a -> s -> Bool
data CanonicalProblem s a = CanonicalProblem {
initial' :: s,
successor' :: s -> [(a,s)],
goaltest' :: s -> Bool
}
instance Problem CanonicalProblem s a where
initial = initial'
successor = successor'
goaltest = goaltest'
canonicalize :: Problem p s a => p s a -> CanonicalProblem s a
canonicalize p = CanonicalProblem {
initial' = initial p,
successor' = successor p,
goaltest' = goaltest p
}
现在我们要证明以下几点：
- 对于任何
Foo这样的类型instance Problem Foo s a，都可以编写一个函数来产生与应用于 any 时canonicalizeFoo :: Foo s a -> CanonicalProblem s a相同的结果。canonicalizeFoo s a
- 可以将使用该类的任何函数重写为使用
Problem该类的等效函数CanonicalProblem。例如，如果你有solve :: Problem p s a => p s a -> r，你可以写一个canonicalSolve :: CanonicalProblem s a -> r相当于solve . canonicalize
我只会草绘证明。在 (1) 的情况下，假设您有一个Foo具有此Problem实例的类型：
instance Problem Foo s a where
initial = initialFoo
successor = successorFoo
goaltest = goaltestFoo
然后给定x :: Foo s a您可以通过替换简单地证明以下内容：
-- definition of canonicalize
canonicalize :: Problem p s a => p s a -> CanonicalProblem s a
canonicalize x = CanonicalProblem {
initial' = initial x,
successor' = successor x,
goaltest' = goaltest x
}
-- specialize to the Problem instance for Foo s a
canonicalize :: Foo s a -> CanonicalProblem s a
canonicalize x = CanonicalProblem {
initial' = initialFoo x,
successor' = successorFoo x,
goaltest' = goaltestFoo x
}
而后者可以直接用来定义我们想要的canonicalizeFoo功能。
在 (2) 的情况下，对于任何函数solve :: Problem p s a => p s a -> r（或涉及Problem约束的类似类型），以及对于任何类型Foo，例如instance Problem Foo s a：
canonicalSolve :: CanonicalProblem s a -> r'通过获取方法的定义并将solve所有出现的Problem方法替换为其CanonicalProblem实例定义来定义。- 证明对于任何
x :: Foo s a,solve x等价于canonicalSolve (canonicalize x)。
(2) 的具体证明需要具体定义solve或相关函数。一般证明可以采用以下两种方式之一：
- 对所有具有
Problem p s a约束的类型进行归纳。
- 证明所有
Problem函数都可以写成函数的一个小子集，证明这个子集有CanonicalProblem等价物，并且一起使用它们的各种方式保持了等价性。