类型的总函数 (forall n . Maybe (fn)) ->也许（forall n . (fn)）

发布于 2024-12-09 01:22:44 字数 979 浏览 0 评论 0原文

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

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

为总功能程序——也就是说，没有使用错误， undefined、unsafeXXX、bottom、不详尽的模式或任何不终止的函数？

通过参数化，对于任何固定的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

原文

Is it possible to write an injective function of type

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

as a total functional program -- that is, without using error,
undefined, unsafeXXX, bottom, inexhaustive patterns, or any
functions which don't terminate?

By parametricity, for any fixed f :: *->* the only total
inhabitants of

(forall n . Maybe (f n))

will take one of two forms:

Nothing

Just z
  where
    z :: forall n . f n

Unfortunately any attempt to case on the Maybe will require
choosing n first, so the types of the pattern variables inside the
case branches will no longer be polymorphic in n. It seems like the
language is missing some sort of construct for performing
case-discrimination on a polymorphic type without instantiating the
type.

By the way, writing a function in the opposite direction is easy:

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

分享到QQ

分享到微博

如果你对这篇内容有疑问，欢迎到本站社区发帖提问参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

发布评论

需要登录才能够评论，你可以免费注册一个本站的账号。

谜泪 2024-12-16 01:22:44

~~我碰巧得到了它，只是通过尝试创建一个可以传递到您的 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

~~I coincidentally got it, just by playing trying to create a value that I could pass into your easyf function. I'm in trouble if you need an explanation though!!~~ see comments below.

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

edit 1

taking out the junk from above,

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

回复收藏 0 原文

以往的大感动 2024-12-16 01:22:44

我证明这是不可能的[呃，不，我没有；见下文] in Agda：

module Proof where

open import Data.Empty
open import Data.Maybe
open import Data.Bool
open import Data.Product

open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

Type : Set₁
Type = Σ ({A : Set} {F : A → Set} → (∀ n → Maybe (F n)) → Maybe (∀ n → F n)) (λ f → ∀ {A} {F : A → Set} x y → f {F = F} x ≡ f y → (∀ i → x i ≡ y i))

helper : (b : Bool) → Maybe (T b)
helper true = just _
helper false = nothing

proof : ¬ Type
proof (f , pf) with inspect (f helper)
proof (f , pf) | just x with-≡ eq = x false
proof (f , pf) | nothing with-≡ eq with f {F = T} (λ _ → nothing) | pf helper (λ _ → nothing)
proof (f , pf) | nothing with-≡ eq | just x | q = x false
proof (f , pf) | nothing with-≡ eq | nothing | q with q eq true
proof (f , pf) | nothing with-≡ eq | nothing | q | ()

当然，这不是一个完美的反驳，因为它是用不同的语言写的，但我认为它匹配得相当好。

我首先将 Type 定义为所需函数的类型，并证明该函数是单射的（Σ x P 可以视为存在主义说法“存在一个 x 使得 P(x)” ）。因为我们讨论的是一个带有函数的单射函数（haskell 的 forall 可以被视为类型级函数，这就是它在 Agda 中的编码方式），所以我使用逐点相等（∀ i → xi ≡ y i) 因为 Agda 的逻辑不允许我直接证明 x ≡ y。

除此之外，我只是通过提供布尔值的反例来反驳这种类型。

编辑：我刚刚想到该类型涉及从某种类型 A 到某种类型的函数 F ，因此我的证明与您可以编写的内容并不完全对应哈斯克尔。我现在很忙，但稍后可能会尝试解决这个问题。

编辑2：我的证明无效，因为我没有考虑参数性。我可以对布尔值进行模式匹配，但不能对集合进行模式匹配，并且我无法在 Agda 中证明这一点。我会再考虑一下这个问题:)

I proved it impossible [err, no I didn't; see below] in Agda:

module Proof where

open import Data.Empty
open import Data.Maybe
open import Data.Bool
open import Data.Product

open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

Type : Set₁
Type = Σ ({A : Set} {F : A → Set} → (∀ n → Maybe (F n)) → Maybe (∀ n → F n)) (λ f → ∀ {A} {F : A → Set} x y → f {F = F} x ≡ f y → (∀ i → x i ≡ y i))

helper : (b : Bool) → Maybe (T b)
helper true = just _
helper false = nothing

proof : ¬ Type
proof (f , pf) with inspect (f helper)
proof (f , pf) | just x with-≡ eq = x false
proof (f , pf) | nothing with-≡ eq with f {F = T} (λ _ → nothing) | pf helper (λ _ → nothing)
proof (f , pf) | nothing with-≡ eq | just x | q = x false
proof (f , pf) | nothing with-≡ eq | nothing | q with q eq true
proof (f , pf) | nothing with-≡ eq | nothing | q | ()

Of course, this isn't a perfect disproof, as it's in a different language, but I think it matches up fairly well.

I started by defining Type as your desired function's type, along with a proof that the function is injective (Σ x P can be seen as an existential saying "there exists an x such that P(x)"). Because we're talking about an injective function that takes a function (haskell's forall can be seen as a type-level function, and that's how it's encoded in Agda), I use point-wise equality (the ∀ i → x i ≡ y i) because Agda's logic won't let me prove that x ≡ y directly.

Other than that, I just disproved the type by providing a counterexample on the booleans.

Edit: it just occurred to me that the type involves a function F from some type A to a type, so my proof doesn't correspond exactly to what you could write in Haskell. I'm busy now but might try to fix that later.

Edit 2: my proof is invalid because I'm not taking parametricity into account. I can pattern match on booleans but not on sets, and I can't prove that in Agda. I'll think about the problem some more :)

回复收藏 0 原文

水晶透心 2024-12-16 01:22:44

如果您查看每个计算值在运行时可能具有的所有可能的计算依赖项，这很容易理解：

类型为 (forall n . Maybe (fn)) 的表达式一种类型的计算结果为 Nothing，另一种类型的计算结果为 Just。因此，它是一个采用类型作为参数的函数。

hard :: (forall n . Maybe (f n)) -> Maybe (forall n . f n)
-- problem statement rewritten with computational dependencies in mind:
hard' :: (N -> Maybe (fN)) -> Maybe (N -> fN)

该 Maybe (N -> fN) 类型的结果值（无论是 Nothing 还是 Just）取决于 的值>N（n 的类型）。

所以，答案是不。

That is easy to understand, if you look at all possible computational dependencies each computed value might have at runtime:

An expression of the type (forall n . Maybe (f n)) could evaluate to a Nothing for one type and a Just for another type. It is therefore a function that takes a type as parameter.

hard :: (forall n . Maybe (f n)) -> Maybe (forall n . f n)
-- problem statement rewritten with computational dependencies in mind:
hard' :: (N -> Maybe (fN)) -> Maybe (N -> fN)

The resulting value of that Maybe (N -> fN) type (whether it is Nothing or Just) depends on the value of N (the type of n).

So, the answer is no.

回复收藏 0 原文

太阳哥哥 2024-12-16 01:22:44

这个问题可以简化为以下一个：我们可以编写一个按以下方式移动 forall 的函数吗？

suicidal :: f (forall n. n) -> forall n. f n

毕竟，如果我们能做到这一点，那么剩下的事情就很容易使用一些命令类型了：（

hard' :: Maybe (f (forall n. n)) -> Maybe (forall n. f n)
hard' Nothing = Nothing
hard' (Just x) = Just (suicidal x)

hard :: (forall n. Maybe (f n)) -> Maybe (forall n. f n)
hard x = hard' x -- instantiate 'n' at type 'forall n. n', thank goodness for impredicativity!

如果你想在 GHC 中尝试这个，一定要定义一个新类型，

newtype Forall f = Forall { unForall :: forall n. f n }

因为否则 GHC 喜欢浮动 forall 到箭头前面然后把你搞砸了。）

但是我们是否可以写自杀的答案很明确：不，我们不能！至少，不是通过 f 参数化的方式。解决方案必须看起来像这样：

suicidal x = /\ n. {- ... -}

...然后我们必须遍历 f 的“结构”，找到存在类型函数的“位置”，并将它们应用到我们现在可用的n。关于 hard 的原始问题的答案是相同的：我们可以为任何特定的 f 编写 hard，但不能对所有参数进行参数化f。

顺便说一句，我不相信你所说的参数化是完全正确的：

根据参数性，对于任何固定的 f :: *->* ，(forall n . Maybe (fn)) 的唯一总居民将采用两个之一形式：Nothing 或 Just z 其中 z :: forall n 。 fn.

实际上，我认为你得到的是居民（观察上相当于）两种形式之一：

/\ n. Nothing
/\ n. Just z

...上面的 z 是不是多态的：它具有特定类型f n。（注意：那里没有隐藏的forall。）也就是说，后一种形式的可能项取决于f！这就是为什么我们不能以 f 为参数编写函数的原因。

编辑：顺便说一句，如果我们允许自己有一个 f 的 Functor 实例，那么事情当然会更容易。

notSuicidal :: (forall a b. (a -> b) -> (f a -> f b)) -> f (forall n. n) -> forall n. f n
notSuicidal fmap structure = /\ n. fmap (\v -> v [n]) structure

...但这是作弊，尤其是因为我不知道如何将其转换为 Haskell。 ;-)

The question can be reduced to the following one: can we write a function that moves foralls in the following way?

suicidal :: f (forall n. n) -> forall n. f n

After all, if we can do that, then the rest is easy with a few impredicative types:

hard' :: Maybe (f (forall n. n)) -> Maybe (forall n. f n)
hard' Nothing = Nothing
hard' (Just x) = Just (suicidal x)

hard :: (forall n. Maybe (f n)) -> Maybe (forall n. f n)
hard x = hard' x -- instantiate 'n' at type 'forall n. n', thank goodness for impredicativity!

(If you want to try this in GHC, be sure to define a newtype like

newtype Forall f = Forall { unForall :: forall n. f n }

since otherwise GHC likes to float foralls to the front of arrows and screw you over.)

But the answer to whether we can write suicidal is clear: No, we can't! At least, not in a way that's parametric over f. The solution would have to look something like this:

suicidal x = /\ n. {- ... -}

...and then we'd have to walk over the "structure" of f, finding "places" where there were type functions, and applying them to the n we now have available. The answer for the original question about hard turns out to be the same: we can write hard for any particular f, but not parametrically over all f.

By the way, I'm not convinced that what you said about parametricity is quite right:

By parametricity, for any fixed f :: *->* the only total inhabitants of (forall n . Maybe (f n)) will take one of two forms: Nothing or Just z where z :: forall n . f n.

Actually, I think what you get is that the inhabitants are (observationally equivalent to) one of two forms:

/\ n. Nothing
/\ n. Just z

...where the z above is not polymorphic: it has the particular type f n. (Note: no hidden foralls there.) That is, the possible terms of the latter form depend on f! This is why we can't write the function parametrically with respect to f.

edit: By the way, if we allow ourselves a Functor instance for f, then things are of course easier.

notSuicidal :: (forall a b. (a -> b) -> (f a -> f b)) -> f (forall n. n) -> forall n. f n
notSuicidal fmap structure = /\ n. fmap (\v -> v [n]) structure

...but that's cheating, not least because I have no idea how to translate that to Haskell. ;-)

回复收藏 0 原文

~没有更多了~