Can a type statically guarantee that a function to pairs only partially depends on its input?

Question

Consider the type of a function from a's to pairs of b's and c's, a -> (b, c). (I'll use Haskell notation for types and functions, but this isn't a question about Haskell per se.) There are many such functions, including those where both, one, or none of the (b, c) outputs depends on a.

Suppose, in particular, that the first output depends on a, but the second doesn't (for example as in \a -> (a, ())). Is it possible to write a type in polymorphic lambda calculus or Hindley-Milner characterizing all and only such functions -- in other words, the subspace of a -> (b, c) which is isomorphic to (a -> b, c)? In other words, can we define an f :: d (for some type d) such that f (\a -> (a, ())), f (\a -> (a, 1)), ..., are all well typed, but f (\a -> (a, a)), f (\a -> (a, snd a)), ..., all aren't?

Alternatively, is there any way of statically ensuring that an element of a -> (b, c) has this property?

Answer 1

No, it cannot be done in polymorphic lambda calculus or Hindley-Milner. For this, you need a type that talks about the properties of a term-level computation; this is called a dependent type. There are various dependently-typed logics. You could look at Coq or Agda as exemplars of programming languages based on such a logic.

For type-checking to be decidable, you will typically see such an f defined to take a second argument, which is a proof that its first function argument has the property you claim. It is up to the programmer to write a convincing proof of this property before they will be able to apply f fully. Making up some syntax, you'd have something like

f :: (g :: a -> (b, c)) -> ((x :: a) -> (y :: a) -> snd (g x) == snd (g y)) -> ...

Note that here, one may give a name to a function's argument when writing a type; that name may then be referred to in the result type of the function. This is one of the special features that dependent types provide.