March 2005 - Haskell - Haskell.org

Type of y f = f . f
by Jim Apple 01 Mar '05

01 Mar '05

Is there a type we can give to y f = f . f y id y head y fst are all typeable? Jim Apple

9 12

(no subject)
by Duncan Coutts 01 Mar '05

01 Mar '05

Gtk2Hs - A Haskell GUI library based on the Gtk+ GUI Toolkit. Version 0.9.7.1 is now available from: http://gtk2hs.sourceforge.net/ This release is only needed for Windows users. If you have version 0.9.7 working there is no need to upgrade. Source and binary packages are available for Windows. There are binary packages for Gtk+ 2.4.x and 2.6.x. The binary packages require GHC 6.2.2. You may wish to use Gtk+ 2.6 since it follows the Windows native look and themes whereas Gtk+ 2.4 did not. Installation on Windows is fairly straightforward. There is an installer for Gtk+ on Windows and installing Gtk2Hs just involves unzipping and running a batch file. Instructions are here: http://gtk2hs.sourceforge.net/archives/2005/02/17/installing-on-windows/ For future Gtk2Hs releases we hope to provide an MSI installer to make it even easier. Changes since 0.9.7: * build fixes for Windows * almost all modules now carry LGPL 2.1 license * a couple of extra functions are now bound Other changes and news since the last release announcement: * there is an introductory article by Kenneth Hoste in the first issue of The Monad.Reader: http://www.haskell.org/hawiki/TheMonadReader_2fIssueOne * a complete website redesign * many new screenshots: http://sourceforge.net/project/screenshots.php?group_id=49207 * packages of version 0.9.7 are available for Gentoo and FreeBSD Please report all problems to gtk2hs-users(a)lists.sourceforge.net . Contributions and feedback are also most welcome. Duncan

1 0

First Issue of The Monad.Reader is online.
by Shae Matijs Erisson 01 Mar '05

01 Mar '05

The first issue of The Monad.Reader is available: http://www.haskell.org/hawiki/TheMonadReader_2fIssueOne We'd like to hear what you think: http://www.haskell.org/hawiki/TheMonadReader_2fIssueOne_2fFeedBack -- Shae Matijs Erisson - http://www.ScannedInAvian.com/ - Sockmonster once said: You could switch out the unicycles for badgers, and the game would be the same.

1 0

De-typechecker: converting from a type to a term
by oleg＠pobox.com 01 Mar '05

01 Mar '05

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

1 0