# Difference between revisions of "Untypechecking"

Jump to navigation
Jump to search

DonStewart (talk | contribs) (Use [[]] instead of {{}}. Must be tired.) |
Tomjaguarpaw (talk | contribs) (Deleting page that hasn't been updated for over 10 years) |
||

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]] |