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?

Brunhilda

I can't get the proof to be air tight and I'm not good at these type level proofs, but my gut instinct is that you would have to solve the Halting Problem either at the value level or the type level to make this work. – Zimmermann

@DanielWagner understood, but I have an (indexed state monad) interface that delivers a -> (b, c), and there is no way around that, given that I have programs that depend on the state alongside programs that don't, I need them to interact with each other in a single interface, and I need (or would very much like) to be able to statically tell when a program's value depends non-trivially on the current state. – Brunhilda

@SimonC One option would be to implement lift :: (a -> b, c) -> a -> (b, c), then have clients call lift when they want to use one of these values that depends only trivially on the current state. – Lachrymose

@DanielWagner Letting m = (\a -> (1, a), 1), suppose we lift m and sequence the result with \_ b -> (snd b, fst b). Then the resulting program has type a -> (a, Int), but the Int value doesn't depend on a. But we can't go back to (a -> a, Int), so we can't tell that our result is the same in the relevant respects as m. This is the sort of thing that happens often in state-ful programs -- a dependency on a state is discharged by a concrete value. – Brunhilda

@SimonC Yes, you must remain in the (a -> b, c) world until the very last moment. – Lachrymose

@DanielWagner Adding a comment here since I have realized what I need is weaker than what this question sets out. It would work if the f in question accepted arguments x which in turn could, in principle, accept () as an input. But I don't wish to monomorphize x, i.e., restrict it to only accepting () as an input. Is it possible to characterize f such that f x is well typed iff x () is well typed -- without in fact applying x to () (which in Haskell and HM will monomorphize x)? – Brunhilda

Off the cuff, I don't see why f :: (() -> a) -> {- whatever; perhaps () again -} wouldn't be that type. But I suspect you should open a fresh question with a bit more context about what you're trying to achieve and why. – Lachrymose

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.

Lachrymose