haskell - 类型的总函数 (forall n . Maybe (f n)) -> Maybe (forall n . (f n))

Question

是否可以编写类型的单射函数

hard :: (forall n . Maybe (f n)) -> Maybe (forall n . (f n))

作为total functional program -- 也就是说，不使用 error，undefined、unsafeXXX、bottom、不详尽的模式或任何哪些函数不会终止？

作者:parametricity ，对于任何固定的 f::*->* 唯一的总和居民

(forall n . Maybe (f n))

将采用两种形式之一:

Nothing

Just z
  where
    z :: forall n . f n

不幸的是，任何对也许的case尝试都需要选择n first，因此模式变量内部的类型case 分支在 n 中将不再是多态的。似乎是语言缺少某种执行结构case - 在不实例化的情况下对多态类型进行区分输入。

顺便说一句，编写相反方向的函数很容易:

easy :: Maybe (forall n . (f n)) -> (forall n . Maybe (f n))
easy Nothing  = Nothing
easy (Just x) = Just x

Answer 1

我巧合地得到了它，只是通过尝试创建一个可以传递到您的 easyf 函数的值。如果您需要解释，我就有麻烦了! 请参阅下面的评论。

data A α = A Int
data B f = B (forall α . f α)

a :: forall α . A α
a = A 3

b = B a
f (B (Just -> x)) = x -- f :: B t -> Maybe (forall α. t α)
f' (B x) = Just x -- f' :: B t -> Maybe (t α)

easy :: forall f . Maybe (forall n . (f n)) -> (forall n . Maybe (f n))
easy Nothing = Nothing
easy (Just x) = Just x

easyf :: Maybe (forall n . (A n)) -> (forall n . Maybe (A n))
easyf = easy

-- just a test
g = easyf (f b)



h :: (forall α. t α) -> Maybe (forall α. t α)
h = f . B

unjust :: (forall n . (Maybe (f n))) -> (forall n . f n)
unjust (Just x) = x

hard :: forall f. (forall n . (Maybe (f n))) -> Maybe (forall n . (f n))
hard xj@(Just _) = g (unjust xj) where
    g :: (forall n . f n) -> Maybe (forall n . (f n))
    g = h
hard Nothing = Nothing

编辑1

把上面的垃圾拿出来，

mkJust :: (forall α. t α) -> Maybe (forall α. t α)
mkJust = Just

unjust :: (forall n . (Maybe (f n))) -> (forall n . f n)
unjust (Just x) = x

hard :: forall f. (forall n . (Maybe (f n))) -> Maybe (forall n . (f n))
hard xj@(Just _) = mkJust (unjust xj)
hard Nothing = Nothing