Can I verify whether a given function type signature has a potential implementation?

Question

In case of explicit type annotations Haskell checks whether the inferred type is at least as polymorphic as its signature, or in other words, whether the inferred type is a subtype of the explicit one. Hence, the following functions are ill-typed:

foo :: a -> b
foo x = x

bar :: (a -> b) -> a -> c
bar f x = f x

In my scenario, however, I only have a function signature and need to verify, whether it is "inhabited" by a potential implementation - hopefully, this explanation makes sense at all!

Due to the parametricity property I'd assume that for both foo and bar there don't exist an implementation and consequently, both should be rejected. But I don't know how to conclude this programmatically.

Goal is to sort out all or at least a subset of invalid type signatures like ones above. I am grateful for every hint.

Bemire

You may find djinn-lib and/or djinn-ghc somewhat helpful. See also djinn. See also hedonisticlearning.com/djinn and note that lambdabot known how to use djinn as well. – Classis

Cf. also Given a Haskell type signature, is it possible to generate the code automatically? and How does Djinn work? – Nanci

Answer 1

Goal is to sort out all or at least a subset of invalid type signatures like ones above. I am grateful for every hint.

You might want to have a look at the Curry-Howard correspondence.

Basically, types in functional programs correspond to logical formulas. Just replace -> with implication, (,) with conjunction (AND), and Either with disjunction (OR). Inhabited types are exactly those having a corresponding formula which is a tautology in intuitionistic logic.

There are algorithms which can decide provability in intuitionistic logic (e.g. exploiting cut-elimination in Gentzen's sequents), but the problem is PSPACE-complete, so in general we can't work with very large types. For medium-sized types, though, the cut-elimination algorithm works fine.

If you only want a subset of not-inhabited types, you can restrict to those having a corresponding formula which is NOT a tautology in classical logic. This is correct, since intuitionistic tautologies are also classical ones. Checking whether a formula P is not a classical tautology can be done by asking whether not P is a satisfiable formula. So, the problem is in NP. Not much, but better than PSPACE-complete.

For instance, both the above-mentioned types

a -> b
(a -> b) -> a -> c

are clearly NOT tautologies! Hence they are not inhabited.

Finally, note that in Haskell undefined :: T and let x = x in x :: T for any type T, so technically every type is inhabited. Once one restricts to terminating programs which are free from runtime errors, we get a more meaningful notion of "inhabited", which is the one addressed by the Curry-Howard correspondence.

Dupion

"There are algorithms which can decide provability in intuitionistic logic" Can you provide a reference? Keen to read about how this works; my gut tells me that provability seems like the sort of thing that might be undecidable, so will probably be fertile learning ground for me :) – Xanthe

I was seeking for a quick algorithmic solution and found a whole special field to study. I think to check if something is not a classical tautology is good enough for the time being. Thank you! – Bemire

@BenjaminHodgson Above I am implicitly referring to simple types / propositional intuitionistic logic, where it is decidable. Once you start adding e.g. rank-2 polymorphism, GADTs, etc. things are no longer decidable, I believe. Anyway, for simple types you can take the Gentzen's LJ inference rules (without CUT) and do a proof search bottom-up, trying all the possible rules non-deterministically. Conveniently, going bottom-up, LJ rules only involve subformulas of the goal formula, which are finite, so we either find a proof, or we visit the same state again (allowing us to prune the search) – Dupion

@BenjaminHodgson You can try to play with the rules in this cool online demo. At every step in the bottom-up search, we only have a finite number of choices, and the search space is finite because of the subformula property. So, we either find a proof or revisit a previous state (so we can detect we are running in circles and prune the search branch). – Dupion

@Dupion I checked if fix for strictly evaluated languages ((a -> b) -> a -> b) -> a -> b is not a tautology for a == True and b == False and the result is positive, because the implication ((a -> b) -> a -> b) yields True (considering -> is right associative) and a -> b yields False and True -> False yields False and this means fix is not a tautology. Is there a mistake in my reasoning, because fix is of course inhabited? – Bemire

@ftor fix (and anything that involves general recursion) is disallowed, since otherwise fix id :: T for any T, and all types are inhabited, which is not interesting. Basically, the Curry-Howard correspondence holds in the language without recursion. (some form of recursion could be allowed, e.g. primitive recursion) – Dupion

Answer 2

Here's a recent implementation of that as a GHC plugin that unfortunately requires GHC HEAD currently.

---

It consists of a type class with a single method

class JustDoIt a where
  justDoIt :: a

Such that justDoIt typechecks whenever the plugin can find an inhabitant of its inferred type.

foo :: (r -> Either e a) -> (a -> (r -> Either e b)) -> (r -> Either e (a,b))
foo = justDoIt

For more information, read Joachim Breitner's blogpost, which also mentions a few other options: djinn (already in other comments here), exference, curryhoward for Scala, hezarfen for Idris.

Sundin

As it stands, this isn't really a self-contained answer to the question. Could you summarize some of the important points of the link? In the case of link-rot, there won't be anything helpful for future readers here. – Countermeasure

Thanks for pointing that out. I added a link to the package itself on Hackage, and a short description of what it does. – Sundin