类型的总函数(forall n.可能(fn)) - >可能(forall n.(fn))

Question

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

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

作为一个总的功能性程序 -即,是不使用error, undefined,unsafeXXX,bottom,非穷尽性的图案,或者其不终止任何功能？

通过参数,对于任何固定f :: *->*的唯一总居民

(forall n . Maybe (f n))

将采取以下两种形式之一:

Nothing

Just z
  where
    z :: forall n . f n

不幸的是,任何case对Maybe遗嘱的尝试都需要n 先选择,因此案例分支中的模式变量的类型将不再是多态的n.看起来这种语言缺少某种构造,用于case在不实例化类型的情况下对多态类型执行 -discrimination .

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

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

Answer 1

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

\n\n

data A \xce\xb1 = A Int\ndata B f = B (forall \xce\xb1 . f \xce\xb1)\n\na :: forall \xce\xb1 . A \xce\xb1\na = A 3\n\nb = B a\nf (B (Just -> x)) = x -- f :: B t -> Maybe (forall \xce\xb1. t \xce\xb1)\nf' (B x) = Just x -- f' :: B t -> Maybe (t \xce\xb1)\n\neasy :: forall f . Maybe (forall n . (f n)) -> (forall n . Maybe (f n))\neasy Nothing = Nothing\neasy (Just x) = Just x\n\neasyf :: Maybe (forall n . (A n)) -> (forall n . Maybe (A n))\neasyf = easy\n\n-- just a test\ng = easyf (f b)\n\n\n\nh :: (forall \xce\xb1. t \xce\xb1) -> Maybe (forall \xce\xb1. t \xce\xb1)\nh = f . B\n\nunjust :: (forall n . (Maybe (f n))) -> (forall n . f n)\nunjust (Just x) = x\n\nhard :: forall f. (forall n . (Maybe (f n))) -> Maybe (forall n . (f n))\nhard xj@(Just _) = g (unjust xj) where\n    g :: (forall n . f n) -> Maybe (forall n . (f n))\n    g = h\nhard Nothing = Nothing\n

\n\n

编辑1

\n\n

把上面的垃圾拿出来，

\n\n

mkJust :: (forall \xce\xb1. t \xce\xb1) -> Maybe (forall \xce\xb1. t \xce\xb1)\nmkJust = Just\n\nunjust :: (forall n . (Maybe (f n))) -> (forall n . f n)\nunjust (Just x) = x\n\nhard :: forall f. (forall n . (Maybe (f n))) -> Maybe (forall n . (f n))\nhard xj@(Just _) = mkJust (unjust xj)\nhard Nothing = Nothing\n

\n