- Haskell - Haskell.org

FACS'05 Call for Papers
by Luis Barbosa 02 Mar '05

02 Mar '05

[apologies if you receive multiple copies] --------------------------------------------- CALL FOR PAPERS FACS'05 II International Workshop on Formal Aspects of Component Software Macao October 24-25, 2005 www.iist.unu.edu/facs05/ --------------------------------------------- IMPORTANT DATES: Submission: Jul 15, 2005 Notification: Sep 15, 2005 Final Version: Sep 30, 2005 Workshop: Oct 24-25, 2005 INVITED SPEAKERS: * Farhad Arbab (CWI and LIACS, Leiden University) * Paolo Ciancarini (Università di Bologna) * Edmund Clarke (Carnegie Mellon University) AIMS AND SCOPE The objective of FACS'2005 is to bring together researchers in the areas of component software and formal methods to promote a deep understanding of this paradigm and its applications. The Workshop will also be interested in defining the common aspects of components and component-based development. It is expected that formal paper presentations be followed by lively debate in a stimulating atmosphere. Possible topics include, but are not limited to: * formal models for software components and component interaction * design and verification methods for component software * component composition and deployment: models, calculi, languages * component testing * specification of extra-functional properties in component software * certification of components and software architectures * component software vs object orientation * components for real-time, safety-critical, secure and/or embedded systems * experience reports and case studies in component software Further information is available at the web site: www.iist.unu.edu/facs05/ BACKGROUND: Component-based software emerged as a promising paradigm to deal with the ever increasing need for mastering systems' complexity, their evolution and reuse, and driving software engineering into sound production and engineering standards. Soon, however, it became a popular technology long before consensual definitions and principles, let alone formal foundations, have been put forward. Issues like mathematical models for components, their interaction and composition, or rigourous approaches to verification, deployment, testing and certification remain open research questions and challenging opportunities for formal methods. Moreover, new challenges are raised by applications to non conventional areas, such as safety-critical, mobile, and/or embedded systems. FACS'05 is the second in a series of workshops, founded by the International Institute for Software Technology of the United Nations University. The first FACS workshop was held in Pisa, Italy, in September 2003, collocated with FM'03. ORGANIZATION: UNU-IIST (Macao) PROGRAM COMMITTEE: Farhad Arbab (CWI, The Netherlands) Luis Barbosa (PC Chair, Universidade do Minho, Portugal) Marcello Bonsangue (LIACS-Leiden University, The Netherlands) Christiano Braga (Universidade Federal Fluminense, Brazil) Manfred Broy (Technical University of Munich, Germany) Calos Canal (Universidad de Malaga, Spain) João Faria (Universidade do Porto, Portugal) Jose Fiadeiro (University of Leicester, United Kingdom) Susanne Graf (VERIMAG, France) Mathai Joseph (Tata Consultancy Services Limited, India) Atsushi Igarashi (Kyoto University, Japan) Kung-Kiu Lau (The University of Manchester, United Kingdom) Zhiming Liu (PC Chair, UNU-IIST, Macao) Antónia Lopes (University of Lisbon, Portugal) Markus Lumpe (Iowa State University, USA) Tom Maibaum (McMaster University, Canada) Sun Meng (National University of Singapore, Singapore) Ugo Montanari (University of Pisa, Italy) David Naumann (Stevens Institute of Technology, USA) Anders Ravn (Aalborg University, Denmark) Bernhard Schätz (Technical University of Munich, Germany) Carolyn Talcott (SRI International, USA) ORGANISING COMMITTEE: He Jifeng, UNU-IIST, Macao (OC chair) Antonio Cerone, UNU-IIST, Macao Bernhard Aichernig, UNU-IIST, Macao Chan Iok Sam , UNU-IIST, Macao Xiaoshan Li, Univ. Macao RELATED EVENTS: ICTAC'05 will be held in Hanoi, Vietnam, the week before. SUBMISSION AND PUBLICATION: Submissions to the workshop will be judged on the basis of originality, relevance, technical soundness and presentation quality. Papers should be written in English and not exceed 15 pages in ENTCS format. Publication of the workshop proceedings in Electronic Notes in Theoretical Computer Science, Elsevier, is anticipated.

1 0

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

02 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

Building a dynamic loadable Parsec parser
by Adam Turoff 28 Feb '05

28 Feb '05

Hi, I've got a little parser written using Parsec that I want to link into some C code. I start by compiling the Haskell sources like so: ghc -ffi -fglasgow-exts -main-is My_Init -c parse.hs When linking parse.o and parse_stub.o against my (additional) glue code, I get the following errors: Main.o(.text+0xc): undefined reference to `__stginit_ZCMain' Main.o(.text+0x14): undefined reference to `__stginit_ZCMain' Main.o(.text+0x20): undefined reference to `ZCMain_main_closure' Main.o(.text+0x24): undefined reference to `ZCMain_main_closure' I'm trying to build a .so that I can load into another process (via Tcl, actually). If I define a main function in my C glue code, these errors go away. But I can't have a main function in this .so. So, two questions: - is it possible to compile and link these .o files into a .so (on Solaris, using ghc 6.2.2)? - what do I need to do to create an entry point for this Haskell code that _isn't_ called main()? Thanks, -- Adam

2 1

postgresql foreign function call segfaults
by Edwin Eyan Moragas 28 Feb '05

28 Feb '05

Hi Group, i'm trying to complete an haskell pgsql interface. all compiles well when using ghc's generated executable but it segfaults when i do a pqexec. -- PGresult *PQexec(PGconn *conn, const char *query); foreign import ccall "libpq-fe.h PQexec" pqexec::X_PGconn->CString->IO X_PGresult here's the offending code: create conn=do putStrLn "creating table products" putStrLn ("\t"++screate) q<- newCString screate -- segmentation fault here! rs<- pqexec conn q stat<- pqcmdstatus rs stats<-peekCString stat putStrLn ("\tstatus is: "++ show stats) ra<- pqcmdtuples rs ras<-peekCString ra putStrLn ("\trows affected is: "++ show ras) screate= "CREATE TABLE products (" ++ "product_no integer," ++ "name text," ++ "price numeric" ++")" i'm using pgsql 7.4, gcc 3.3.4, ghc 6.2.2 i tried compiling with -fvia-C and it doesn't finish compiling. i'm asking this question in the fear that i have done something wrong. i have posted my code the code, makefile and generated .hc file here: http://www.eyan.org/haskell/ -- kind regards, eyan http://www.eyan.org

1 0

Call for Tutorials - ICTAC05
by Bernhard K. Aichernig 28 Feb '05

28 Feb '05

Call for Tutorials - ICTAC05 INTERNATIONAL COLLOQUIUM ON THEORETICAL ASPECTS OF COMPUTING Hanoi, Vietnam - 17--21 October, 2005 http://www.iist.unu.edu/ictac05 ===================== BACKGROUND AND OBJECTIVES ICTAC is an International Colloquium on Theoretical Aspects of Computing founded by the International Institute for Software Technology of the United Nations University (UNU-IIST). The aim of the colloquium is to bring together practitioners and researchers from academia, industry and government to present research results, and exchange experience, ideas, and solutions for their problems in theoretical aspects of computing.The colloquium is aimed particularly, but not exclusively, at participants from developing countries. We believe that this will help developing countries to strengthen their research, teaching and development in computer science and engineering, improve the links between developing countries and developed countries, and establish collaboration in research and education. The first ICTAC (ICTAC'04) was held in Guiyang, China and its proceedings were published as "ICTAC 2004: Theoretical Aspects of Computing", LNCS 3407. ICTAC'05 will have a technical program for five days including two days for tutorials and three days for a conference, and a training school for 5 days. The topics of the conference include, but are not limited to: - automata theory and formal languages - principles and semantics of programming languages - logics and their applications - software architectures and their description languages - software specification, refinement, and verification - model checking and theorem proving - formal techniques in software testing - models of object and component systems - coordination and feature interaction - integration of formal and engineering methods - service-oriented development - document-driven development - models of concurrency, security, and mobility - theory of parallel, distributed, and internet-based (grid) computing - real-time and embedded systems - type and category theory in computer science SPONSORS AND ORGANISATION ICTAC'05 will be organised jointly between the Institute of Information Technology of the Vietnamese Academy of Sciences and Technology (IoIT), the University of Technology of the Vietnam National University in Hanoi (UoT-VNU) and UNU-IIST. UNU-IIST, IoIT and UoT-VNU are also sponsors of ICTAC'05. There will be an one-week training school during 10--14 October 2005 before the conference. TUTORIAL SUBMISSION You are welcome to submit a proposal for a tutorial on any subject related to the topics listed above. All tutorial proposal submissions should have a detailed description of the tutorial contents, the time duration, and an extended abstract written in English. The extended abstract should not not exceed 5 pages in LNCS format (see http://www.springer.de/comp/lncs/authors.html for details). The extended abstract of the accepted tutorials will be published in the proceedings of the ICTAC05 conference which will be published by Springer in the Lecture Notes in Computer Science series. All queries and tutorial proposals should be sent to the program committee co-chairs Dang Van Hung, e-mail: dvh(a)iist.unu.edu, or Martin Wirsing, e-mail: wirsing(a)informatik.uni-muenchen.de. The deadline for tutorial proposal submission is 11 July 2005, and the notification of tutorial proposal acceptance is 25 July 2005. The date for tutorials is 17-18 October, 2005. ADVISORY COMMITTEE Dines Bjorner, Singapore Manfred Broy, Germany Jifeng He, UNU-IIST Mathai Joseph, India Shaoying Liu, Japan Zhiming Liu, UNU-IIST Jim Woodcock, UK Jose Luiz Fiadeiro, UK Tobias Nipkow, Germany PUBLICITY CHAIR Bernhard K. Aichernig, UNU-IIST ORGANISING COMMITTEE Le Hai Khoi, IoIT (co-chair) Ho Si Dam, UoT-VNU (co-chair) Nguyen Tue, UoT-VNU Bui The Duy, UoT-VNU Nguyen Viet Ha, UoT-VNU Vu Duc Thi, IoIT Le Quoc Hung, IoIT Do Nang Toan, IoIT Ngo Quoc Tao, IoIT PROGRAM COMMITTEE Marc Aiguier, France Keijiro Araki, Japan J.O.A. Ayeni, Nigeria Jay Bagga, USA Hubert Baumeister, Germany Michel Bidoit, France Jonathan Bowen, UK Victor A. Braberman, Argentina Cristian S. Calude, New Zealand Ana Cavalcanti, UK Yifeng Chen, UK Dang Van Hung, UNU-IIST (co-chair) Jim Davies, UK Janos Demetrovics, Hungary Jin Song Dong, Singapore Henning Dierks, Germany Do Long Van, Vietnam Marcelo F. Frias, Argentina Wan Fokkink, Netherlands Susanna Graf, France Valentin Goranko, South Africa Dimitar Guelev, Bulgaria Michael R. Hansen, Denmark Jozef Hooman, Netherlands Purush Iyer, USA Ryszard Janicki, Canada Takuya Katayama, Japan Maciej Koutny, UK Xuandong Li, China Antonia Lopes, Portugal Antoni Mazurkiewicz, Poland Hrushikesha Mohanty, India Ngo Quang Hung, USA Nguyen Cat Ho, Vietnam Paritosh Pandya, India Jean-Eric Pin, France Narjes Ben Rajeb, Tunisia R. Ramanujam, India. Anders P. Ravn, Denmark Gianna Reggio, Italy Wolfgang Reif, Germany Riadh Robbana, Tunisia Mark Ryan, UK Zaidi Sahnoun, Algeria Augusto Sampaio, Brazil Don Sannella, UK Bernhard Schaetz, Germany Andrea Maggiolo-Schettini, Italy Carolyn Talcott, USA P. S. Thiagarajan, Singapore Ji Wang, China Martin Wirsing, Germany (co-chair) Mingsheng Ying, China Jian Zhang, China Hongjun Zheng, USA -- Bernhard Aichernig, Research Fellow of UNU-IIST www.iist.unu.edu/~bka ---------------------------------------------------------------------- SEFM 2005: 3rd IEEE International Conference on Software Engineering and Formal Methods, Koblenz, Germany, 7.- 9. Sept. 2005 http://sefm2005.uni-koblenz.de ICTAC 2005: International Colloquium on Theoretical Aspects of Computing, Hanoi, Vietnam, 17-21 October, 2005 http://www.iist.unu.edu/ictac05/

1 0

Re: [Haskell] Compiling GHC on Panther using darwin ports
by Gregory Wright 27 Feb '05

27 Feb '05

Hi Chris, Excellent news. Thank you for helping to track down the bug in the port. Best Wishes, Greg On Feb 27, 2005, at 1:37 PM, Chris Brown wrote: > Greg, > > That appears to be working now! Thanks very much for your help! > > Kind regards, > > Chris. > > > On 27 Feb 2005, at 18:00, Gregory Wright wrote: > >> >> Hi Chris, >> >> Portfile revision 14 is in cvs and (I hope) does what you need. >> Let me know if you have problems. >> >> If you have trouble, just try installing dlcompat by hand (sudo port >> install dlcompat) >> and ghc should built. But let me know if you have to resort to this >> so I can fix the portfile. >> >> The ghc build is somewhat of a hairball. Thanks for helping find these >> bugs. >> >> Best Wishes, >> Greg >> >> >> On Feb 27, 2005, at 12:11 PM, Chris Brown wrote: >> >>> Hi Greg, >>> >>> Thanks very much for your help, however I am still getting exactly >>> the same error message. >>> >>> I have done a cvs update in the darwinports directly and tried to >>> install ghc again (after a make clean). I have checked the revision >>> number of the portfile for ghc and it says it is revision number 13. >>> >>> Hope you can help further... >>> >>> Thanks, >>> >>> Chris. >>> >>> >>> On 27 Feb 2005, at 16:15, Gregory Wright wrote: >>> >>>> >>>> Hi Chris, >>>> >>>> Forget about my last message. I had accidentally introduced a bug >>>> in my last revision. I have updated the portfile; update from cvs >>>> and >>>> you should be ready to go. >>>> >>>> (The bootstrap compiler still depends on the darwinports dlcompat >>>> library, which was not a dependency of the port. It is now. I >>>> hope to >>>> remove this constraint and use the system dlcompat when ghc 6.4 >>>> appears in a few weeks.) >>>> >>>> Best Wishes, >>>> Greg >>>> >>>> >>>> >>>> On Feb 27, 2005, at 6:12 AM, Chris Brown wrote: >>>> >>>>> Hi, >>>>> >>>>> I am trying to install GHC on Mac OS X (Panther) using Darwin >>>>> Ports. When i run >>>>> >>>>> sudo port install ghc >>>>> >>>>> I get the following error message shortly into the compilation: >>>>> >>>>> ------------------------------------------------------------------- >>>>> ----- >>>>> ==fptools== make boot - --no-print-directory -r; >>>>> in >>>>> /Users/chrisbrown/darwinports/dports/lang/ghc/work/ghc-6.2.2/ghc/ >>>>> utils/hasktags >>>>> ------------------------------------------------------------------- >>>>> ----- >>>>> /Users/chrisbrown/darwinports/dports/lang/ghc/work/ghc-bootstrap/ >>>>> bin/ghc -M -optdep-f -optdep.depend -osuf o -H16m -O >>>>> -I/opt/local/include -L/opt/local/lib HaskTags.hs >>>>> dyld: >>>>> /Users/chrisbrown/darwinports/dports/lang/ghc/work/ghc-bootstrap/ >>>>> lib/ghc-6.2.2/ghc-6.2.2 can't open library: >>>>> /opt/local/lib/libdl.1.dylib (No such file or directory, errno = >>>>> 2) >>>>> make[3]: *** [depend] Trace/BPT trap >>>>> make[2]: *** [boot] Error 1 >>>>> make[1]: *** [boot] Error 1 >>>>> make: *** [build] Error 1 >>>>> >>>>> >>>>> I remember on Tiger this was because the portfile which tells >>>>> darwin ports what to do has a condition in it to compile the >>>>> bootstrap differently for panther or jaguar (and obviously not >>>>> tiger). >>>>> >>>>> Could anyone please help me to fix this compilation error? >>>>> >>>>> Thanks, >>>>> >>>>> Chris Brown. >>>>> >>>>> _______________________________________________ >>>>> Haskell mailing list >>>>> Haskell(a)haskell.org >>>>> http://www.haskell.org/mailman/listinfo/haskell >>>>> >>>> >>> >> >

1 0

Encode module library
by Otakar Smrz 27 Feb '05

27 Feb '05

I might be wrong, but it seems there is no module library in Haskell that would provide a unified interface for converting strings from one encoding into another, be it Unicode Transformation Formats, the numerous 8-bit encodings, or some user-defined transliterations or transcriptions. Inspired by the Encode module in Perl, I have sketched an architecture of such an interface for Haskell. Let me give links to the proto-implementation and its documentation: http://ckl.mff.cuni.cz/smrz/Encode-0.01.zip http://ckl.mff.cuni.cz/smrz/Encode/doc/index.html There, I further discuss and illustrate how extending the library with new encodings would be done, and what the common data representation type might be. I would be happy for your comments and suggestions. Thank you, Otakar Smrz

3 2