How to reconstruct Haskell expression from type

Question

I'm writing a program that for given type signature reconstructs Haskell expression of this type, eg.: for a -> b -> a it returns \x -> \_ -> x. I've read about the theory behind this problem and I know that there is this Howard-Curry isomorphism. I imagine my program to parse input and represent it as terms. Then I would fire SLD-resolution that would tell me if it is possible to construct the term of given type (for Pierce's for instance it is not possible). What I don't already know is how to actually create Haskell expression during this resolution. I've seen the code of djinn but it is a bit complicated, and I want to grasp some general idea of how this works.

Answer 1

If you use Curry-Howard to connect a subset of Haskell to some intuitionistic logic, it should be very easy to extract a Haskell program from a proof term. Essentially, the proof terms should already have the very same structure as Haskell programs, but just use different constructor names. I think you can even use the same algebraic data type for both proof terms and Haskell terms if you translate the constructor names in your head as appropriate. For example:

type Name = String

data Type                  -- aka. Formula
  = Function Type Type     -- aka. Implication
  | TypeVar Name           -- aka. PropositionalVar

data Term                  -- aka. Proof
  = Lambda Name Type Term  -- aka. ImplicationIntroduction
  | Apply Term Term        -- aka. ImplicationElimination
  | TermVar Name           -- aka. Start / Identity / Axiom / Copy

You will have to use a context of variables in scope (aka. hypotheses you can assume).

type TypingContext = Map Name Type -- aka. Hypotheses

Given types like this, you "just" have to write a function:

termOf :: Type -> TypingContext -> Maybe Term

But maybe as a first step, it would be better to write the inverse function first, as an exercise:

typeOf :: Term -> TypingContext -> Maybe Type

The basic structure of these two function should be similar: Pattern match on the thing you have, decide which typing rules (aka. proof rules) are applicable, call yourself recursively to construct a partial result, finish the partial result by wrapping in the constructor that corresponds to the typing rule (aka. proof rule). A difference is that typeOf can just walk through the whole term and figure everything out, while termOf probably has to guess and backtrack if guesses don't work out. So probably, you actually want the list monad for termOf.

The benefit of writing typeOf first is:

1. It should be easier because terms tend to contain more information than types, so termOf can use that extra information while typeOf needs to create that extra information.
2. There is more help available because many people implement typeOf as an exercise but few people implement termOf as an exercise.