@@ Line 1: / Line 1: @@
-== Untypechecking ==
-Converting from a type to a term.
-<pre>
-[Haskell] De-typechecker: converting from a type to a term
-oleg at pobox.com oleg at pobox.com
-Tue Mar 1 03:13:08 EST 2005
-  * Next message: [Haskell] Re: Type of y f = f . f
-  * Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]
------------------------------------------------------------------------------------------------------
-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
-</pre>
-[[Category:Idioms]]

Difference between revisions of "Untypechecking"

Revision as of 14:50, 6 February 2021

Navigation menu

Search