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

Question

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

Answer 1

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

Answer 2

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

Answer 3

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.