22

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
4
  • 1
    Please accept my apologies for deleting an earlier version of this question (which was open for no more than four minutes). I had oversimplified it so much that I inadvertently created a trivial solution.
    – Adam
    Oct 11, 2011 at 0:18
  • When I was adding type witnesses to darcs I had to use a lot of types like these. The lesson there was that returning a type like Maybe (forall n. f n) just doesn't work well in Haskell. What does work well, is to make a wrapper type using existential types to hold on to your type. Have you tried that? The only other thing I can suggest would be doing the equivalent but using CPS. Oct 24, 2011 at 4:24
  • 1
    Jason, the code above actually isn't what I'm working on -- rather, it's the smallest program I could find that exhibited the problem. I think your comment that this "just doesn't work well in Haskell" is correct, and the fact that nobody's been able to answer the question is evidence to that effect. I've sketched a proposal on how to fix this language deficiency here: megacz.com/thoughts/parametric-case.html
    – Adam
    Oct 26, 2011 at 19:56
  • Actually, Jason's problem is a different one, which is that Maybe (forall n. f n) is an impredicative type which GHC doesn't have good support for. But if you use the newtype trick to make things go through, you STILL run into Adam's problem. Jun 13, 2016 at 2:29

4 Answers 4

4

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
9
  • 3
    Gato, your "unjust" function has an inexhaustive pattern match (try compiling with -fwarn-incomplete-patterns) and therefore does not qualify as total functional programming (for example, Coq would reject your program). I know this sounds picky, but if the only way to do something is via inexhaustive matching that's a pretty good sign that "something is missing" from Haskell.
    – Adam
    Oct 11, 2011 at 7:11
  • fair enough; it'd never cause a problem since the Just is matched before, but you're right, the only implementation would be unjust Nothing = undefined. Oct 11, 2011 at 7:15
  • No worries. For what it's worth I currently have two hack-arounds for this situation, and one of them is basically the same as what you wrote. The other one takes advantage of some weird properties of System FC coercions.
    – Adam
    Oct 11, 2011 at 7:19
  • 5
    @Adam - I don't agree that an inexhaustive pattern match automatically disqualifies a program from being total. In particular, if it can be proven that the non-total function can only be called with appropriate arguments, then the overall program is total.
    – John L
    Oct 11, 2011 at 7:42
  • 6
    @John the question very clearly said no "inexhaustive pattern matching". I'm using the definition of "total" adopted by Coq and Constructive Type Theory; if you want to use another definition that's up to you.
    – Adam
    Oct 11, 2011 at 17:48
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 :)

2
  • pumpkin, thanks for trying. I have a sneaking suspicion that the function I'm asking for might be inconsistent with dependent type theories (like Agda or Coq), which is why the question is specific to Haskell.
    – Adam
    Oct 13, 2011 at 18:32
  • The issue is really that parametricity limits what I can do with the parameter, but Agda provides no way to prove anything about that :(
    – copumpkin
    Oct 14, 2011 at 2:51
1

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.

4
  • 1
    comonad, you write "An expression of the type (forall n . Maybe (f n)) could evaluate to a Nothing for one type and a Just for another type.", but this is in fact false. The reason why it is false is called "parametricity". Take a look at Phil Wadler's excellent paper "theorems for free".
    – Adam
    Oct 21, 2011 at 20:23
  • And what about this? Does this differ because of the context? Data.Typeable.gcast(return()) :: (forall n.Typeable n,Monad f=>Maybe(f n)) ( see haskell.org/ghc/docs/latest/html/libraries/base/… )
    – comonad
    Oct 24, 2011 at 19:07
  • @comonad, I think Adam had mentioned that the typeclass constraints will make that expression somehow fundamentally different ... hopefully he'll provide that explanation here. Oct 30, 2011 at 3:22
  • I'll read that excellent paper next weekend. For the implementation of such a type-system, I can think of an explicit typeclass-dependency instead of type-dependency, too. I thought, both systems would somehow be equal, But so far, I didn't read (or write) any proof or paper about it. I think, one system is used in Haskell-Core with the big lambdas, which I guessed (probably wrong) to be about type-variables.
    – comonad
    Nov 2, 2011 at 22:43
0

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

5
  • 1
    sorry I haven't read it all, but when you say "reduced", I think you must write suicidal in terms of hard, not the other way around. Oct 11, 2011 at 19:18
  • 1
    @gatoigrado You're almost certainly right. I always get the order of "x reduces to y" wrong. What I mean in plain English is that, if we can implement suicidal, then we can implement hard. I agree that claiming you can't implement suicidal does not therefore imply that you can't implement hard -- but suicidal feels like the core of the problem that makes implementing hard hard to me. Oct 12, 2011 at 2:47
  • yeah, I don't really remember it either, I just informally think: you can probably solve some easy problem P by calling a SAT solver, so the thing being called is the harder problem. Oct 12, 2011 at 6:33
  • @Daniel, no, you have the reduction backwards. If you can write suicidal then you can certainly write hard. But just because you can write hard does not mean you can write suicidial!
    – Adam
    Oct 12, 2011 at 19:59
  • Mathematicians solve problems by reducing them to already solved problems. They even solve easy problems by reducing them to hard-but-already-solved problems. To prove that a problem is unsolveable they reduce the solvability-in-question to an already-proven-as-(un-)solvable problem by (backwards-)implication. That means that they reduce from any unsolvable problem to the problem in question to prove that the latter has to be unsolvable, too (because otherwise that unsolvable one would have to be solvable, too).
    – comonad
    Oct 20, 2011 at 20:35

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.