September 2003 - Haskell

SVV'03 call for papers
by Abhik Roychoudhury 08 Sep '03

08 Sep '03

(Apologies if you receive multiple copies of this message) SECOND CALL FOR PAPERS [ Submission deadline: September 15, 2003 ] *************************************************** International Workshop on Software Verification and Validation (SVV 2003) In Conjunction with International Conf. on Logic Programming (ICLP) 2003 Mumbai (India), December 2003 URL: http://www.comp.nus.edu.sg/~abhik/SVV03/index.html *********************************************** -------------------------------------- Topics Covered --------------------------------------- The workshop will focus on theoretical techniques, practical methods as well as case studies for verification of conventional and embedded software systems. In particular, we welcome papers which describe combinations of formal and informal reasoning, as well as formal verification and program analysis techniques. Tool papers and case studies, which report on advances in verifying large scale programs in standard languages are particularly sought. The list of topics include, but are not restricted to: Tools/environments/case studies for large scale software verification Static analysis/Abstract interpretation/Program transformations for verification Use of model checking and deductive techniques for software verification Role of declarative programming languages (such as Prolog) for infinite state verification. Techniques to validate system software (such as compilers) as well as assembly code/Java byte-code Proof techniques for verifying specific classes of software (such as object-oriented programs) Integrating testing and run-time monitoring with formal techniques Validation of UML diagrams, and/or requirement specifications Software certification and proof carrying code Integration of formal verification into software development projects ------------------------------- Workshop Format ----------------------------- The one day workshop will mostly involve talks of peer reviewed research papers in an informal setting. We plan to have several break-out sessions apart from the research paper sessions to promote informal discussions. In addition, there will be an invited talk (detailed information given below). ----------------------------- Submissions Information ------------------------------ Regular submissions should be no more than 15 pages. Short papers (up to 5 pages) describing initial ideas are also welcome. All submitted papers should be in PS or PDF. Please avoid using zip, gzip, compress, tar etc. Papers should be submitted via e-mail to svv03(a)comp.nus.edu.sg The deadlines are as follows. Submission deadline: September 15, 2003 Notification of Acceptance: October 15, 2003 Final Version submission: November 15, 2003 We plan to publish selected papers from the workshop as Electronic Notes in Theoretical Computer Science (ENTCS). Note that ENTCS papers should be at least 10 pages in ENTCS format. ----------------------- Program Committee -------------------------- Krzysztof R. Apt, CWI (Netherlands) and NUS (Singapore). Giorgio Delzanno, University of Genova (Italy). Maurizio Gabbrielli, University of Bologna (Italy). Shriram Krishnamurthi, Brown University (USA). Andreas Podelski, Max Planck Institute (Germany). C.R. Ramakrishnan, SUNY Stony Brook (USA). Wang Yi, Uppsala University (Sweden). --------------------- Invited Speaker ------------------------ Ramesh Bharadwaj, Naval Research Laboratory (USA). Talk Title: Rigorous Methods for Software Construction: Retrofitting "Engineering" into Software Engineering -------------------------- Organizers ---------------------------- Sandro Etalle, University of Twente, Netherlands. Supratik Mukhopadhyay, NASA IV&V and University of West Virginia, USA. Abhik Roychoudhury, National University of Singapore (Workshop Co-ordinator). ****************************************************

1 0

Re: Circular Instance declarations
by oleg＠pobox.com 08 Sep '03

08 Sep '03

Ashley Yakeley wrote: > Would it be reasonable for the compiler to check back through the > stack and allow the circularity? It will just create an ordinary > recursive function. The following works. Flags: -fglasgow-exts -fallow-undecidable-instances data D r = ZeroD | SuccD (r (D r)) instance (Eq (r (D r))) => Eq (D r) where ZeroD == ZeroD = True (SuccD a) == (SuccD b) = a == b _ == _ = False newtype C a = MkC a instance Eq (C (D C)) where (MkC ZeroD) == (MkC ZeroD) = True (MkC (SuccD a)) == (MkC (SuccD b)) = a == b _ == _ = False equalDC :: D C -> D C -> Bool equalDC = (==) c2 = SuccD (MkC (SuccD (MkC ZeroD))) c1 = SuccD (MkC (ZeroD)) *Main> equalDC c2 c2 True *Main> equalDC c2 c1 False *Main> equalDC ZeroD c1 False *Main> equalDC ZeroD ZeroD True *Main>

1 0

Re: [mercury-users] pragma compiled_memo for compile-time tabled evaluation
by Stefan Karrmann 05 Sep '03

05 Sep '03

André Platzer (Fri, Sep 05, 2003 at 04:03:42PM +0200): > Hello Mercury users! > > Is there any way to extend tabled evaluation to compile-time? As far as > I understand, normal tabled evaluation memorises values computed at > run-time. On an invocation with the same arguments, then mercury reuses > those values instead of a second computation. This is very cool. > > However, I wonder if there is a way to extend this idea to compile-time. > So in case of a constant function like > > %% computes the number pi with a precision of 500 digits. > :- func pi_to_500_digits = string. > :- mode pi_to_500_digits = out is det. > :- pragma memo(pi_to_500_digits/0). > > after compilation, the program will compute pi to 500 digits only at the > first time this constant is used, but repeat this computation for every > program run. An improvement in this situation of constant functions (or > at least functions depending upon arguments of a small finite domain) > would be to perform the respective computation only once, at > compile-time instead of repeatedly at each new program run. The compiler > would evaluate the function at compile-time and store its tabled value > instead of the machine code for performing the computation. How could one balance compile-time computation against space consumption? E.g. (in Haskell - sorry) pi_s_500_digit = pi_to_500_digits !! 500 The space consumption of the result is small, but the computation is expensive. This is a good case for compile-time computation. While enumerate_123456 = [1..123456] consumes much space and minimal time. To decide automatically about compile-time computation we may need a pragma that sets a threshold: :- pragma reductions_per_byte_at_compile_time(10). Store the value in the library if the compiler needs 10 or more reductions per byte of the value. Sincerly, -- Stefan

1 0

Re: Haskell for non-Haskell's sake
by Graham Hutton 05 Sep '03

05 Sep '03

I use Haskell for processing the examination marks of our 900 students. Our University has a system that can do all of this, but to ensure that I understood all the rules and regulations I coded up a simple version in Haskell, which comprises around 400 lines. It takes a CSV (comma separated values) file downloaded from our central marks database, from which five different marks reports can be produced, which are then written out as CSV files for viewing and further processing using Excel. Interesting, this simple Haskell program showed that the University system implemented one of the progression rules incorrectly :-) Graham +---------------------------------------------------------------------+ | Dr Graham Hutton Email : gmh(a)cs.nott.ac.uk | | School of Computer Science and IT Web : www.cs.nott.ac.uk/~gmh | | University of Nottingham | | Jubilee Campus, Wollaton Road | | Nottingham NG8 1BB Phone : +44 (0)115 951 4220 | | United Kingdom Fax : +44 (0)115 951 4254 | +---------------------------------------------------------------------+

5 6

unary minus
by Christian Maeder 05 Sep '03

05 Sep '03

Hi, I wonder why Haskell only allows the unary minus on the left side of an expression ("lexp" in the grammar). There should be no problem to uniquely recognize an unary minus right beside an operation symbol ("qop"). Does the grammar allow two consecutive qops in other cases? This would allow "1 * - 1" to be correct (which I think is sort of "standard"), while "1 - 1" clearly is the infix minus. What was the rational for the current restriction of the unary minus? Do I oversee something? Christian

1 1

Re: proving the monad laws
by oleg＠pobox.com 05 Sep '03

05 Sep '03

Hello! > Would it be possible to write a piece of Haskell code which checks > the monadic laws automatically by simulating evaluation in this way? To some extent, yes. The proof in the previous message was based on normalization, with respect to associative laws and some betas. So we can take (st f) . (st g) and do: - inlining of the 'st' operation - de-sugaring into core Haskell - more inlining and beta [perhaps to a certain depth] - rearranging expression based on associative laws, e.g., converting f . (g . h) into (f . g) . h converting case (case x of P -> A) of P' -> A' into case x of P -> case A of P' -> A' Then do the same for (st ((st f) . g)) and compare the results. If the results are identical, great. Otherwise, the user has to look at the results and decide if they are the same based on his intuition. GHC already does inlining, de-sugaring, and some betas. I think there is a flag that makes GHC dump the result of these operations for normalization with respect associative laws. BTW, GHC accepts user-defined rules: so we can express associativity rules for known operations and direct GHC to normalize terms with respect to these laws. I don't know how to express side conditions though (e.g., the normalization of 'case' above is valid only if the variables bound by pattern P do not occur in P', A'). It would be great if there was a RULES-pragma operation to alpha-rename bound variables in a term. In that case, we can safely normalize more expressions.

1 0

Fundep & Datatype Request
by Ashley Yakeley 05 Sep '03

05 Sep '03

OK, this is an issue I have raised before I think, but I don't remember what the opinion on it was. The following doesn't compile with ghc -fglasgow-exts (or Hugs -98): -- ghc -fglasgow-exts -c TypeLambda.hs module TypeLambda where { class Fc a b | a -> b; instance Fc Bool Int; data F1 a = forall b. (Fc a b) => MkF1 b; makeF1 :: Int -> F1 Bool; makeF1 = MkF1; getF1 :: F1 Bool -> Int; getF1 (MkF1 i) = i; data F2 a = MkF2 (forall b. (Fc a b) => b); makeF2 :: Int -> F2 Bool; makeF2 i = MkF2 i; getF2 :: F2 Bool -> Int; getF2 (MkF2 i) = i; } Clearly makeF1 and getF2 are OK. But I claim getF1 and makeF2 should compile, since the type inside either an "F1 Bool" or an "F2 Bool" must always be an Int. Instead I get this: TypeLambda.hs:14: Inferred type is less polymorphic than expected Quantified type variable `b' is unified with `Int' When checking an existential match that binds i :: b and whose type is F1 Bool -> Int In the definition of `getF1': getF1 (MkF1 i) = i TypeLambda.hs:19: Cannot unify the type-signature variable `b' with the type `Int' Expected type: b Inferred type: Int In the first argument of `MkF2', namely `i' In the definition of `makeF2': makeF2 i = MkF2 i So why is this useful? Because you can do some form of type-lambda with it. For instance, you might have some system of collection types: Word8 -->> UArray Int Word8 Word16 -->> UArray Int Word16 (a -> b) -->> Array Int (a -> b) It would be nice to hide the implementation and just expose some type-constructor: MyCollection Word8 MyCollection Word16 MyCollection (a -> b) I believe this can't be done currently. -- Ashley Yakeley, Seattle WA

1 0

need some info/help
by Pratik Bhadra 04 Sep '03

04 Sep '03

Hi I know there is a general consensus about finding out new things to use with Haskell but I am quite a newcomer in this field and am attempting to write a compiler and a runtime system in Haskell. At this important juncture I would like to ask for some help with some resources, books or links which I can look up which would help me understand the process better. Your help is highly appreciated. Thanks :)

3 2

Re: proving the monad laws
by oleg＠pobox.com 04 Sep '03

04 Sep '03

Steffen Mazanek posed a problem: given the monad: > data Error a = Error String | Ok a > data TI a = TI (Subst -> Int -> Error (Subst, Int, a)) > instance Monad TI where > return x = TI (\s n -> Ok (s,n,x)) > TI f >>= g = TI (\s n -> case f s n of > Ok (s',m,x) -> let TI gx = g x in > gx s' m > Error s->Error s) > fail s = TI (\_ _->Error s) prove the associativity of bind: > m@(TI mf) >>= (\a->f a >>= h) = > = TI (\s n -> case mf s n of > Ok (s',m,x) -> let TI gx = (\a->f a >>= h) x in > gx s' m > Error s->Error s) = ... > = ((TI mf) >>= f) >>= h > I was wondering, if it is possible to simplify: "let TI gx = f x >>=h in > ...". > But the "a" may occur in "h"? No, it may not. First of all, the third monadic law specifically disclaims such an occurrence. Indeed, if 'a' had occurred free in 'h', then ((TI mf) >>= f) >>= h would make no sense. Although (>>=) notation is better for practical programming, I believe Filinski's notation is superior for manipulation. Filinski defines a postfix operator "raised star", which is denoted 'st' below: st:: (Monad m) => (a -> m b) -> m a -> m b st f m = m >>= f Indeed, st = flip (>>=) In Filinski's notation, the third monadic law has an especially appealing form: st ((st f) . g) = (st f) . (st g) Let us also define arun (TI f) s n = f s n We can then write for our monad: st f = \m -> TI $ \s n -> case arun m s n of Ok (s',m',x') -> arun (f x') s' m' Error s' -> Error s' Let _m, _s and _n denote "fresh" values of the right type (so we can later appeal to the universal generalization rule (closely related to eta-reduction) Phase 1: arun ((st ((st f) . g)) _m) _s _n => case arun _m _s _n of Ok (s',m',x') -> arun ((st f) $ g x') s' m' -- x' is not free in f, g Error s' -> Error s' => case arun _m _s _n of Ok (s',m',x') -> case arun (g x') s' m' of Ok (s'',m'',x'') -> arun (f x'') s'' m'' Error s'' -> Error s'' Error s' -> Error s' Phase 2: arun (((st f) . (st g)) _m) _s _n => arun (((st f) $ (st g) _m) _s _n => case arun ((st g) _m) _s _n of Ok (s'',m'',x'') -> arun (f x'') s'' m'' -- x'' is not free in f, g Error s'' -> Error s'' => case (case arun _m _s _n of Ok (s',m',x') -> arun (g x') s' m' -- x' is not free in f, g Error s' -> Error s') of Ok (s'',m'',x'') -> arun (f x'') s'' m'' -- x'' is not free in f, g Error s'' -> Error s'' => {see note below} case arun _m _s _n of Ok (s',m',x') -> case arun (g x') s' m' of Ok (s'',m'',x'') -> arun (f x'') s'' m'' Error s'' -> Error s'' Error s' -> Error s' Now, the results of Phase 1 and Phase 2 are identical. Given that _m, _s and _n were unique, fresh variables, by appealing to the universal generalization rule and the Church-Rosser property of our reductions, we conclude that st ((st f) . g) = (st f) . (st g) The critical step is the associativity of case: case (case x of C1 -> O1; C2 -> O2) of C1' -> O1'; C2' -> O2' ==> case x of C1 -> case O1 of C1' -> O1'; C2' -> O2' C2 -> case O2 of C1' -> O1'; C2' -> O2' provided that variables bound in C1 and C2 do not occur in C1', O1', C2', O2'

2 1

Haskell for non-Haskell sake
by Gordon James Miller 03 Sep '03

03 Sep '03

I'm currently examining using Haskell for doing numerical modelling of middle atmospheric photochemistry for my PhD work. I've long been troubled by the disconnect between the mathematical formulation of physical laws as found in textbooks and the imperative formulation of them in C/Fortran/Java. I absolutely love the expressiveness of Haskell with respect to writing mathematical software and so I'm pursuing this with some vigor and hope to have a series of web reports to present my successes and failures with this. Gordon James Miller Promisemark, Inc. Senior Computer Scientist gmiller(a)promisemark.com (571)330-9012 Everyone has a place, some just need to be put there.

2 1