Total function of type (forall n . Maybe (f n)) -> Maybe (forall n . (f n))

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 d开发者_如何学Goon'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

---

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

---

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 :)

---

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.

---

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. ;-)