[Haskell] De-typechecker: converting from a type to a term

[oleg at pobox.com]

This message presents polymorphic functions that derive a term for a
given type -- for a class of fully polymorphic functions: proper and
improper combinators. This is better understood on an example:

  rtest4 f g = rr (undefined::(b -> c) -> (a -> b) -> a -> c) HNil f g
  *HC> rtest4 (:[]) Just 'x'
  [Just 'x']
  *HC> rtest4 Just Right True
  Just (Right True)

We ask the Haskell typechecker to derive us a function of the
specified type. We get the real function, which we can then apply to
various arguments. The return result does behave like a `composition'
-- which is what the type specifies. Informally, we converted from
`undefined' to defined.

It must be emphasized that no modifications to the Haskell compiler are
needed, and no external programs are relied upon. In particular,
however surprising it may seem, we get by without `eval' -- because
Haskell has reflexive facilities already built-in. 

This message contains the complete code. It can be loaded as it is
into GHCi -- tested on GHCi 6.2.1 or GHCi snapshot 6.3.20041106. It
may take a moment or two to load though. Commenting our tests speeds
up the loading.


This message presents two different converters from a type to a term.
Both derive a program, a term, from its specification, a type -- for
a class of fully polymorphic functions. The first converter has just
been demonstrated.  It is quite limited in that the derived function
must be used `polymorphically' -- distinct type variables must be
instantiated to different types (or, the user should first
instantiate their types and then derive the term). The second
converter is far more useful: it can let us `visualize' what a
function with a particular type may be doing.  For example, it might
not be immediately clear what the function of the type
    (((a -> b -> c) -> (a -> b) -> a -> c) -> 
     (t3 -> t1 -> t2 -> t3) -> t) -> t)

is. The test (which is further down) says

    test9 = reify (undefined::(((a -> b -> c) -> (a -> b) -> a -> c) -> 
			   (t3 -> t1 -> t2 -> t3) -> t) -> t) gamma0

    *HC> test9
    \y -> y (\d h p -> d p (h p)) (\d h p -> d)

that is, the function in question is one of the X combinators. It is
an improper combinator.

A particular application is converting a point-free function into the
pointful form to really understand the former. For example, it might
take time to comprehend the following expression

 pz = (((. head . uncurry zip . splitAt 1 . repeat) . uncurry) .) . (.) . flip

It is derived by Stephan Hohe in 
  http://www.haskell.org/pipermail/haskell-cafe/2005-February/009146.html

Our system says
  test_pz = reify (undefined `asTypeOf` pz) gamma0
  *HC> test_pz
  \h p y -> h y (p y)

So, pz is just the S combinator.

As an example below shows, an attempt to derive a term for a type
a->b expectedly fails. The type error message essentially says that
a |- b is underivable.


Our system solves type habitation for a class of functions with
polymorphic types. From another point of view, the system is a prover
in the implication fragment of intuitionistic logic. Essentially we
turn a _type_ into a logical program -- a set of Horn clauses -- which
we then solve by SLD resolution.  It is gratifying to see that
Haskell typeclasses are up to that task.


The examples above exhibit fully polymorphic types -- those with
*uninstantiated* -- implicitly universally quantified -- type
variables. That is, our typeclasses can reify not only types but also
type schemas. The ability to operate on and compare *unground* types
with *uninstantiated* type variables is often sought but rarely
attained. The contribution of this message is the set of primitives
for nominal equality comparison and deconstruction of unground
types. Earlier these tools were used to implement nested monadic
regions in the type-safe manner without imposing the total order on
the regions. The monadic regions are described in the paper by M. Fluet
and G. Morrisett, ICFP04.

The rest of this message is as follows:

	- equality predicate of type schemas
	- function types as logic programs. Solving type habitation
          by SLD resolution
	- more examples
	- code
           -- class Resolve: SLD resolution

* Equality predicate of type schemas

This is a short remark on the equality predicate of type schemas. In
more detail, this topic will be described elsewhere. 

To obtain the equality, we need the following overlapping instances
extensions

> {-# OPTIONS -fglasgow-exts #-}
> {-# OPTIONS -fallow-undecidable-instances #-}
> {-# OPTIONS -fallow-overlapping-instances #-}
> {-# OPTIONS -fallow-incoherent-instances #-}
>
> module HC where


We must remark that -fallow-overlapping-instances and
-fallow-incoherent-instances extensions are used *exclusively* for the
type equality testing. With these extensions and the following declarations

  class C a where op:: a -> Int
  instance C a where ...
  instance C Bool where ...
  data W  = forall a. W a

the expression
  case W () of W x -> op x 

is well-typed with the "instance C a" chosen. In the context of TypeEq,
that behavior guarantees that a quantified variable is equal only to itself
and nothing else. So, the use of overlapping instances in this code
is well-defined and sound.

The existence of this remarkable feature has been pointed out by Simon
Peyton-Jones, who implemented it.

The code at the end of this message defines nominal equality on
quantified type variables. A quantified variable is equal only to
itself. It is useful to think of such type variables as being
Skolemized. Fortunately, GHC kindly does all the Skolemization for
us. For example,

	*FP> type'eq id id
	HFalse

because the type of the identity function "a->a" means "forall a. a
->a", which, after skolemization, becomes "sk1 -> sk1". The type of
the second `id' in the above equation becomes "sk2 -> sk2" -- thus the
types are not equal. Indeed, if we ask GHC to show us the inferred
type of the above expression

   *FP> :t type'eq id id
   type'eq id id :: forall a a1 b. (TypeEq (a -> a) (a1 -> a1) b) => b

we can see the Skolemization very clearly.

OTH,
   *FP> let f x = (x,x) in case f id of (u,v) -> type'eq u v
   HTrue
because
   *FP> :t let f x = (x,x) in case f id of (u,v) -> type'eq u v
   let f x ...  :: forall a b. (TypeEq (a -> a) (a -> a) b) => b

that is, the types of both `id' are unified (yet they remain unground)

* Two type-to-term reifiers

As we have mentioned, we introduce two type reifiers. The first one converts
a type to the following term:

> data Term = Var Int | L Int Term | A Term Term -- deriving Show

The custom Show instance is at the end of this message. The second reifier
converts a type to a true Haskell term. The difference between the reifiers
is akin to the difference between a homogeneous list and a heterogeneous
list (HList). The former reifier is far easier to explain. 

* Function types as logic programs. Solving type habitation by SLD resolution

To solve the type habitation problem -- to find a term (proof) for a
proposition expressed as a type -- we use SLD resolution. It may be
helpful to think of the whole process as converting a type
(proposition) into a Horn-clause logical program, and solving that
program using a Prolog-style evaluator. Here are a few examples of
types and the corresponding logical programs.

The type a->b->a after applying the implication elimination rule twice
yields the following program:

	t2t(a, var(1)).
        t2t(b, var(2)).
        ?- t2t(a,X), Term = lambda(1,(lambda(2,X))).
        % solution: lambda(1, lambda(2, var(1))), or \x y -> x

The type "(b -> c) -> (a -> b) -> a -> c"  (of the composition function)
corresponds to the following program:

	t2t(c,app(var(1),X)) :- t2t(b,X).
	t2t(b,app(var(2),X)) :- t2t(a,X).
        t2t(a,var(3)).
        ?- t2t(c,X), Term = lambda(1,lambda(2,lambda(3,X))).
        % solution:
        % lambda(1, lambda(2, lambda(3, app(var(1), app(var(2), var(3))))))
        % or \x y z -> x (y z)


The type of one of the X combinators [1] (which is an improper combinator)
	forall t a b c t1 t2 t3.
        (((a -> b -> c) -> (a -> b) -> a -> c) -> (t3 -> t1 -> t2 -> t3) -> t) 
	-> t

corresponds to the logical program

	t2t(t, app(app(var(1),X),Y)) :- t2t(u1,X), t2t(u2,Y).

        % u1 denotes (a -> b -> c) -> (a -> b) -> a -> c
        t2t(u1,X) :- t2t(c,Y), X = lambda(3,lambda(4,lambda(5,Y))).
        t2t(c,app(app(var(3),X),Y)) :- t2t(a,X), t2t(b,Y).
        t2t(b,app(var(4),X)) :- t2t(a,X).
        t2t(a,var(5)).

        % u2 denotes t3 -> t1 -> t2 -> t3
        t2t(u2,X) :- t2t(t3,Y), X = lambda(6,lambda(7,lambda(8,Y))).
        t2t(t3,var(6)).
        t2t(t1,var(7)).
        t2t(t2,var(8)).

        ?- t2t(t,X), Term = lambda(1,X).

The solution to the latter is, when printed nicely,
    \f -> f (\a b c -> (a c) (b c)) (\x y z -> x)


We construct such programs and solve them with the ordinary SLD resolution
-- only using Haskell typeclasses rather than Prolog.

[1] Jeroen Fokker, The Systematic Construction of a One-combinator Basis for
Lambda-Terms.
Formal Aspects of Computing 4 (1992), pp. 776-780.
http://www.cs.uu.nl/people/jeroen/article/combinat/combinat.ps


* More examples

The reification function takes, as one argument, an environment -- or
the initial assumption. Oftentimes it is this:

> gamma0 = G HNil 0 

Other environments may be used to reify *open* terms.

We start with a few simple examples:

> test1 = let term = \x y -> x in reify term gamma0
> test2 = let term = \x y -> y in reify term gamma0
> test3 = let term = \f x y -> f x in reify term gamma0
>
> -- \f x y -> f y x
> test4 = reify (__::(t -> t1 -> t2) -> t1 -> t -> t2) gamma0
>
> -- \f g a b -> f (g a b) 
> test5 = let term = (.) (.) (.) in reify (undefined `asTypeOf` term) gamma0
>
> pz = (((. head . uncurry zip . splitAt 1 . repeat) . uncurry) .) . (.) . flip
> test_pz = reify (undefined `asTypeOf` pz) gamma0
>
> -- \f g h x y -> f (g x) (h y)
> test7 = let term = ((flip . ((.) .)) .) . (.) in reify term gamma0

More complex are improper combinators:

> -- \f -> f (\x -> x)
> test6 = reify (__::((a->a)->b) -> b) gamma0
>
> -- X combinators
> {-- commented out to speed up loading
> test8 = let term = \a b c d -> c d (a (\x -> d))
>	  in reify (undefined `asTypeOf` term) gamma0
> 
> test9 = reify (undefined::(((a -> b -> c) -> (a -> b) -> a -> c) -> 
>			     (t3 -> t1 -> t2 -> t3) -> t) -> t) gamma0
> --}

Other terms to try:
   ((((.) . (.)) . (.)) . (.))
   ((flip .) . (((flip .) .) . (((.) . (.)) . (((.) . (.)) .))))
   reify const gamma0
   reify (.) gamma0
   reify (asTypeOf __ (.)) gamma0

> term1B = reify (undefined:: t4 -> (t3 -> t4 -> t5 -> t1) -> t6 -> t3 -> 
>		   (t4 -> t -> t -> t5 -> t1 -> t2) -> t -> t5 -> t2) gamma0

The type a->b however is not inhabitable: If we uncomment the following,

> --test_not_derivable = reify (__::a -> b) gamma0

we get the type error:
    No instances for (Resolve (Gamma (:*: (T2T (:*: a HNil)) HNil)) assum',
		      HLookup rt HNil (:*: rt assum))
      arising from use of `reify' at ...

That is, a |- rt is unprovable.

* Code

** Preliminaries

An abbreviated notation for undefined, which shall occur very often

> __ = __

Heterogeneous lists

> data HTrue 
> data HFalse 
> instance Show HTrue  where show _ = "HTrue"
> instance Show HFalse where show _ = "HFalse"

> data HNil = HNil deriving Show
> data HCons a b = HCons a b deriving Show

> -- Syntax sugar from the HList library. Thanks to Ralf Laemmel
> infixr 2 :*:
> infixr 2 .*.
> type e :*: l = HCons e l
> a .*. b = HCons a b

Environment: hs are hypotheses: an HList of T2T, each of which states one
assumption: an association of a type to a term

> data Gamma hs = G hs Int deriving Show
> newtype T2T t = T2T Term deriving Show

Converting an implication to a type list of assumptions in inverse order

> class I2L t tl | t -> tl where
>     i2l :: t -> tl
>     i2l = undefined -- it's a type-level function
>
> instance (IsFunction t flag, I2L' flag t tl)
>     => I2L t tl
>
> class I2L' flag t tl | flag t -> tl
>
> instance I2L' HFalse t (t :*: HNil)
>
> instance (I2L x tlx, I2L y tly, HAppend tly (tlx :*: HNil) tl)
>     => I2L' HTrue (x->y) tl
>
> ti1 = i2l (__::a->b->c)
> ti2 = i2l (__::(a->b)->a->b)
> ti3 = i2l (__::(a -> b -> c) -> (a -> b) -> a -> c)


The main reification class

> class Reify t gamma where
>     reify :: t -> gamma -> Term
>
> instance (IsFunction t flag, I2L' flag t (rt :*: at),
> 	    AddHyp gamma at gamma',
> 	    Resolve gamma' ((rt :*: HNil) :*: HNil))
>     => Reify t gamma where
>     reify t gamma = let (varlist, gamma') = add'hyp gamma (__::at) []
> 		      in foldr (\ (Var v) s -> L v s ) 
> 			     (resolve gamma' (((__::rt) .*. HNil) .*. HNil) [])
> 			     varlist

Label top-level assumptions with variables

> class AddHyp gamma tl gamma' | gamma tl -> gamma' where
>     add'hyp :: gamma -> tl -> [Term] -> ([Term],gamma')
>
> instance AddHyp gamma HNil gamma where
>     add'hyp g _ varlist = (varlist,g)
>
> instance AddHyp (Gamma ((T2T t) :*: hs)) r gamma
>     => AddHyp (Gamma hs) (t :*: r) gamma where
>     add'hyp (G hs varcount) _ varlist = 
> 	let v   = (Var varcount)
> 	    hs' = ((T2T v)::T2T t) .*. hs
> 	in add'hyp (G hs' (varcount + 1)) (__::r) (v:varlist)


** The SLD resolution algorithm

> class Resolve gamma goals where
>     resolve :: gamma -> goals -> [Term] -> Term
>
> instance Resolve gamma HNil where
>     resolve _ _ pt = foldr1 (flip A) pt
>
> instance (HLookup g hs (g :*: assum),
> 	    HReverse assum assum',
> 	    Resolve (Gamma hs) assum',
> 	    Resolve (Gamma hs) gr)
>     => Resolve (Gamma hs) ((g :*: HNil) :*: gr) where
>     resolve gamma@(G hs _) _ pt = 
> 	let T2T t1 = hlookup (__::g) hs
> 	in resolve gamma (__::gr) ((resolve gamma (__::assum') [t1]) : pt)
>
> instance (AddHyp (Gamma hs) (gc :*: gcr) gamma',
> 	    AddHyp (Gamma ((T2T gc) :*: hs)) gcr gamma',
> 	    Resolve gamma' ((g :*: HNil) :*: HNil),
> 	    Resolve (Gamma hs) gr)
>     => Resolve (Gamma hs) ((g :*: gc :*: gcr) :*: gr) where
>     resolve gamma@(G hs _) _ pt =
> 	let t1 = let (varlist, gamma'::gamma') = 
> 			 add'hyp gamma (__::(gc :*: gcr)) []
> 		 in foldr (\ (Var v) s -> L v s ) 
> 		          (resolve gamma' (((__::g) .*. HNil) .*. HNil) [])
> 			  varlist
> 	in resolve gamma (__::gr) (t1 : pt)

Lookup in the `associative' type-indexed list

> class HLookup t l w | t l -> w where
>     hlookup :: t -> l -> T2T w
>
> instance (TypeEq t t' flag, HLookup' flag t ((T2T (t' :*: at)) :*: r) w)
>     => HLookup t ((T2T (t' :*: at)) :*: r) w where
>     hlookup = hlookup' (undefined::flag)
>
> class HLookup' flag t l rt | flag t l -> rt where
>     hlookup' :: flag -> t -> l -> T2T rt
>
> instance HLookup' HTrue t ((T2T (t :*: at)) :*: r) (t :*: at) where
>     hlookup' _ _ (HCons t _) = t
>
> instance HLookup t r w => HLookup' HFalse t ((T2T t') :*: r) w where
>     hlookup' _ t (HCons _ r) = hlookup t r



> class HAppend l1 l2 l | l1 l2 -> l where
>     happend :: l1 -> l2 -> l
> instance HAppend HNil l2 l2 where 
>     happend _ l2 = l2
> instance HAppend l1 l2 l => HAppend (a :*: l1) l2 (a :*: l) where
>     happend (HCons a l1) l2 = a .*. (happend l1 l2)

> class HReverse l1 l2 | l1 -> l2
> instance HReverse HNil HNil
> instance (HReverse l1 l1', HAppend l1' (a :*: HNil) l2)
>     => HReverse (a :*: l1) l2


** Show Terms in a nice way

> instance Show Term where
>     show (Var i) =
> 	case divMod i 26 of
> 			 (0,i) -> simple_var i
> 			 (j,i) -> simple_var i ++ (show j)
> 	  where simple_var i = ["yphdcbaeijklmnofqrstuvwxgz" !! i]
>     show (A e v@(Var i)) = show e ++ " " ++ show v
>     show (A e1 e2) = show e1 ++ " " ++ "(" ++ show e2 ++ ")"
>     show (L i e) = show' [i] e
> 	where show' vars (L j e) = show' (j:vars) e
> 	      show' vars e = "\\" ++ unwords (map (show.Var) $ reverse vars) ++
> 			     " -> " ++ show e


* The second reifier: from types to bona fide Haskell terms

The second reifier is a `lifted' version of the first one. Wherever we
used regular Haskell lists before, we use HLists now.

> newtype T2TT tl t = T2TT t deriving Show
>
> class RR t gamma where
>     rr :: t -> gamma -> t
>
> instance (IsFunction t flag, RR' flag t gamma)
>     => RR t gamma where
>     rr = rr' (__::flag)
>
> class RR' flag t gamma where
>     rr' :: flag -> t -> gamma -> t
>
> instance (IsFunction x flagx, I2L' flagx x tlx, 
> 	    IsFunction y flagy, RR' flagy y ((T2TT tlx x) :*: gamma))
>     => RR' HTrue (x->y) gamma where
>     rr' _ _ gamma = \ (v::x) -> rr' (__::flagy) (__::y)
> 		                    (((T2TT v)::T2TT tlx x) .*. gamma)
>
> instance (RResolve gamma ((t :*: HNil) :*: HNil) HNil t)
>     => RR' HFalse t gamma where
>     rr' _ _ gamma = rresolve gamma (((__::t) .*. HNil) .*. HNil) HNil
>
>
> class RResolve gamma goals tl t | gamma goals tl -> t where
>     rresolve :: gamma -> goals -> tl -> t
>
> instance RResolve gamma HNil (t :*: HNil) t where
>     rresolve _ _ (HCons t HNil) = t -- foldr1 (flip A) pt
>
> instance RResolve gamma HNil (t1 :*: tr) (t->r)
>     => RResolve gamma HNil (t :*: t1 :*: tr) r where
>     rresolve g _ (HCons t r) = (rresolve g HNil r) t
>
> instance (RHLookup g gamma (T2TT (g :*: assum) g'),
> 	    HReverse assum assum',
> 	    RResolve gamma assum' (g' :*: HNil) ra,
> 	    RResolve gamma gr (ra :*: pt) t)
>     => RResolve gamma ((g :*: HNil) :*: gr) pt t where
>     rresolve gamma _ pt = 
> 	let T2TT t1 = rhlookup (__::g) gamma
> 	    ra :: ra = rresolve gamma (__::assum') (t1 .*. HNil)
> 	in rresolve gamma (__::gr) (ra .*. pt)
> -- the instance for improper combinators is left as an exercise to the reader

> -- Lookup in the `associative' type-indexed list
> class RHLookup t l w | t l -> w where
>     rhlookup :: t -> l -> w
>
> instance (TypeEq t t' flag,RHLookup' flag t ((T2TT (t' :*: at) tt') :*: r) w)
>     => RHLookup t ((T2TT (t' :*: at) tt') :*: r) w where
>     rhlookup = rhlookup' (__::flag)
>
> class RHLookup' flag t l w | flag t l -> w where
>     rhlookup' :: flag -> t -> l -> w
>
> instance RHLookup' HTrue t ((T2TT (t :*: at) tt) :*: r) 
>                            (T2TT (t :*: at) tt) where
>     rhlookup' _ _ (HCons t _) = t
>
> instance RHLookup t r w => RHLookup' HFalse t ((T2TT tl' t') :*: r) w where
>     rhlookup' _ t (HCons _ r) = rhlookup t r


A few tests:

> rtest1 = let f (x::a) (y::b) ::a = rr undefined HNil x y
> 	 in f 1 2
> rtest2 = let f x y = rr (undefined::a->b->b) HNil x y
> 	 in f 1 2
>
> -- \f x y -> f x :: forall t t1 t2. (t -> t1) -> t -> t2 -> t1
> rtest3 = let t f x y = rr (undefined::(t -> t1) -> t -> t2 -> t1) HNil f x y
> 	 in t Just 1 'c'
>
> rtest4 f g = rr (undefined::(b -> c) -> (a -> b) -> a -> c) HNil f g
> -- *HC> rtest4 (:[]) (\x -> (True,x)) 10
> -- [(True,10)]
> -- must be truly polymorphic!	     


* Equality and deconstruction of type schemas

> class IsFunction a b | a -> b
> instance TypeCast f HTrue => IsFunction (x->y) f
> instance TypeCast f HFalse => IsFunction a f
>
> -- literally lifted from the HList library
> class TypeCast   a b   | a -> b, b->a   where typeCast   :: a -> b
> class TypeCast'  t a b | t a -> b, t b -> a where typeCast'  :: t->a->b
> class TypeCast'' t a b | t a -> b, t b -> a where typeCast'' :: t->a->b
> instance TypeCast'  () a b => TypeCast a b where typeCast x = typeCast' () x
> instance TypeCast'' t a b => TypeCast' t a b where typeCast' = typeCast''
> instance TypeCast'' () a a where typeCast'' _ x  = x
>
> class TypeEq' () x y b => TypeEq x y b | x y -> b
>     where type'eq :: x -> y -> b
> 	    type'eq _ _ = undefined::b
> class TypeEq' q x y b | q x y -> b
> class TypeEq'' q x y b | q x y -> b
> instance TypeEq' () x y b => TypeEq x y b
> instance TypeCast b HTrue => TypeEq' () x x b
> instance TypeEq'' q x y b => TypeEq' q x y b
> instance TypeEq'' () x y HFalse