命题(P -> Q) -> Q和P \/ Q是等效的。
在Haskell中有没有办法证明这种等效性？
from :: Either a b -> ((a -> b) -> b)
from x = case x of
Left a -> \f -> f a
Right b -> \f -> b
to :: ((a -> b) -> b) -> Either a b
to = ???
如此
from . to = id和to . from = id？
命题
(P -> Q) -> Q和P \/ Q是等效的。
这在古典逻辑中是正确的，但在建构逻辑中却不是。
在构造逻辑中，我们没有law of excluded middle，也就是说，我们不能以“ P为真或P不为真”开始思考。
我们通常会这样推理：
x :: P），则返回Left x。 nx :: P -> Void函数。然后absurd . nx :: P -> Q（我们可以使任何类型的峰达到峰值，取Q）并用f :: (P -> Q) -> Q)调用给定的absurd . nx以获取类型Q的值。没有类型的一般功能的问题：
lem :: forall p. Either p (p -> Void)
对于某些具体类型，例如Bool有人居住，所以我们可以写作
lemBool :: Either Bool (Bool -> Void)
lemBool = Left True -- arbitrary choice
但同样，通常我们不能。
,不，这是不可能的。考虑特殊情况Q = Void。
Either P Q为Either P Void，与P同构。
iso :: P -> Either P Void
iso = Left
iso_inv :: Either P Void -> P
iso_inv (Left p) = p
iso_inv (Right q) = absurd q
因此，如果我们有一个功能项
impossible :: ((P -> Void) -> Void) -> Either P Void
我们也可以有一个术语
impossible2 :: ((P -> Void) -> Void) -> P
impossible2 = iso_inv . impossible
根据Curry-Howard的对应关系，这将是直觉主义逻辑中的重言式：
((P -> False) -> False) -> P
但是以上是双重否定消除，众所周知，不可能以直觉主义逻辑来证明-因此是矛盾的。 （我们可以用经典逻辑证明这一事实是不相关的。）
（最后的注意：这假设Haskell程序终止。当然，使用无限递归undefined以及类似的避免实际返回结果的方法，我们可以在Haskell中使用任何类型。）>
否，不可能，但这有点微妙。问题在于类型变量a和b被普遍量化。
to :: ((a -> b) -> b) -> Either a b
to f = ...
a和b被普遍量化。调用者选择它们的类型，因此您不能仅创建任何一种类型的值。这意味着您不能在忽略参数Either a b的同时创建类型为f的值。但是使用f也是不可能的。在不知道a和b是什么类型的情况下，您无法创建类型a -> b的值传递给f。当类型被普遍量化时，可用的信息还不够。
至于为什么同构在Haskell中不起作用-您确定这些命题在建设性直觉主义逻辑中是等效的吗？ Haskell没有实现经典的演绎逻辑。
,正如其他人指出的那样，这是不可能的，因为我们没有被排除的中间律。让我更明确地说明这一点。假设我们有
bogus :: ((a -> b) -> b) -> Either a b
，我们设置b ~ Void。然后我们得到
-- chi calls this `impossible2`.
double_neg_elim :: ((a -> Void) -> Void) -> a
bouble_neg_elim f = case bogus f of
Left a -> a
Right v -> absurd v
现在，我们来证明对排除在特定命题上的中间律的双重否定。
nnlem :: forall a. (Either a (a -> Void) -> Void) -> Void
nnlem f = not_not_a not_a
where
not_a :: a -> Void
not_a = f . Left
not_not_a :: (a -> Void) -> Void
not_not_a = f . Right
所以现在
lem :: Either a (a -> Void)
lem = double_neg_elim nnlem
lem显然不存在，因为a可以编码我碰巧选择的任何图灵机配置都将停止的命题。
让我们验证lem是否足够：
bogus :: forall a b. ((a -> b) -> b) -> Either a b
bogus f = case lem @a of
Left a -> Left a
Right na -> Right $ f (absurd . na)
我不知道这在逻辑上是有效的，或者对您等效是什么意思，但是可以在Haskell中编写这样的功能。
要构造一个Either a b，我们需要一个a或一个b值。我们没有任何构造a值的方法，但是我们确实有一个函数返回一个可以调用的b。为此，我们需要提供一个将a转换为b的函数，但是鉴于类型未知，我们最多只能制作一个返回常数b的函数。为了获得该b值，我们无法以其他任何方式构造它，因此这成为循环推理-我们可以通过简单地创建一个 fixpoint
to :: ((a -> b) -> b) -> Either a b
to f = let x = f (\_ -> x) in Right x