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 see comments below.easyf
function. I'm in trouble if you need an explanation though!!
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 forall
s 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
orJust z
wherez :: 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 forall
s 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. ;-)
精彩评论