- Haskell - Haskell.org

RE: Typesafe MRef with a regular monad
by George Russell 06 Jun '03

06 Jun '03

In fact I think these Typesafe MRef's are exactly equivalent to dynamic types. In other words, if you've got one, you've got the other. Ralf Hinze has just shown that if you have dynamic types you can implement Typesafe MRef. The reverse implementation would be something like > data Dynamic = FM () > > toDyn :: a -> Dynamic > toDyn a = insert empty () a > > fromDynamic :: Dynamic -> Maybe a > fromDynamic fm = > let > bogus :: Key () a > (_,bogus) = insert empty () undefined > in > lookup fm bogus

1 0

Call for Papers on Compositional Verification of UML Models
by frb 06 Jun '03

06 Jun '03

Call for Papers Compositional Verification of UML Models Workshop of the UML 2003 Conference The definition of UML has been motivated by the need for a standard notation for modelling system architectures and behaviours at functional and implementation level. The main fqocus has been essentially on terminology, notation and syntax without addressing semantic, validation and methodology issues which are important for formal design and verification techniques. This workshop addresses the application of formal methods and techniques that exploit the architectural structure of UML models in a compositional manner. TOPICS The workshop topics include (but are not limited to): * semantic foundations of architectural and component-based design within UML * compositional techniques for the analysis embedded and real-time systems in UML * compositional model checking of UML behavioural models * compositional deductive methods based on OCL * methodologies based on compositional formal techniques FORMAT OF THE WORKSHOP The workshop will consist of presentations of the accepted papers, which will be the basis for an intensive discussion on the workshop topics. Extended abstracts of the presentations will be published after the workshop by Elsevier Science as a volume of the Electronic Notes in Theoretical Computer Science. For an up-to-date program and invited talks see the workshop web-site http://fmco.liacs.nl/compuml.html SUBMISSIONS Authors are invited to submit by August 25th an extended abstract not exceeding 20 pages electronically to F.S.de.Boer(a)cwi.nl. Submissions must be either in Postscript or PDF format and prepared for USLetter or A4 page sizes. Submissions will be evaluated by the program committee for inclusion in the proceedings, which will be published by Electronic Notes in Theoretical Computer Science series. Papers must contain original contributions, be clearly written, and include appropriate reference to and comparison with related work. Simultaneous submissions to other conferences are not allowed. IMPORTANT DATES 25 August Submission deadline 10 September Notification to authors 1 October Deadline for preliminary version 21 October Workshop date 21 November Deadline for final version PROGRAM COMMITTEE Frank de Boer (CWI, NL) Marcello Bonsangue (LIACS, NL) Werner Damm (OFFIS, DE) Susanne Graf (Verimag, France) David Harel (Weizmann Institute, Israel) Jozef Hooman (University of Nijmegen, NL) Bernhard Josko (OFFIS, DE) Amir Pnueli (Weizmann Institute, ISR) Willem-Paul de Roever (Kiel University, DE) Joseph Sifakis (Verimag, FR) ORGANIZERS Frank de Boer (CWI, NL) Marcello Bonsangue (LIACS, NL) Bernhard Josko (OFFIS, DE) SPONSORS This workshop is sponsored by the European R&D project OMEGA - Correct Development of Real-time Embedded Systems (http://www-omega.imag.fr) and the German-Dutch project Mobi-J (main sponsor of FMCO, http://fmco.liacs.nl) Call for Papers Compositional Verification of UML Models Workshop of the UML 2003 Conference The definition of UML has been motivated by the need for a standard notation for modelling system architectures and behaviours at functional and implementation level. The main fqocus has been essentially on terminology, notation and syntax without addressing semantic, validation and methodology issues which are important for formal design and verification techniques. This workshop addresses the application of formal methods and techniques that exploit the architectural structure of UML models in a compositional manner. TOPICS The workshop topics include (but are not limited to): * semantic foundations of architectural and component-based design within UML * compositional techniques for the analysis embedded and real-time systems in UML * compositional model checking of UML behavioural models * compositional deductive methods based on OCL * methodologies based on compositional formal techniques FORMAT OF THE WORKSHOP The workshop will consist of presentations of the accepted papers, which will be the basis for an intensive discussion on the workshop topics. Extended abstracts of the presentations will be published after the workshop by Elsevier Science as a volume of the Electronic Notes in Theoretical Computer Science. For an up-to-date program and invited talks see the workshop web-site http://fmco.liacs.nl/compuml.html SUBMISSIONS Authors are invited to submit by August 25th an extended abstract not exceeding 20 pages electronically to F.S.de.Boer(a)cwi.nl. Submissions must be either in Postscript or PDF format and prepared for USLetter or A4 page sizes. Submissions will be evaluated by the program committee for inclusion in the proceedings, which will be published by Electronic Notes in Theoretical Computer Science series. Papers must contain original contributions, be clearly written, and include appropriate reference to and comparison with related work. Simultaneous submissions to other conferences are not allowed. IMPORTANT DATES 25 August Submission deadline 10 September Notification to authors 1 October Deadline for preliminary version 21 October Workshop date 21 November Deadline for final version PROGRAM COMMITTEE Frank de Boer (CWI, NL) Marcello Bonsangue (LIACS, NL) Werner Damm (OFFIS, DE) Susanne Graf (Verimag, France) David Harel (Weizmann Institute, Israel) Jozef Hooman (University of Nijmegen, NL) Bernhard Josko (OFFIS, DE) Amir Pnueli (Weizmann Institute, ISR) Willem-Paul de Roever (Kiel University, DE) Joseph Sifakis (Verimag, FR) ORGANIZERS Frank de Boer (CWI, NL) Marcello Bonsangue (LIACS, NL) Bernhard Josko (OFFIS, DE) SPONSORS This workshop is sponsored by the European R&D project OMEGA - Correct Development of Real-time Embedded Systems (http://www-omega.imag.fr) and the German-Dutch project Mobi-J (main sponsor of FMCO, http://fmco.liacs.nl)

1 0

RE: Typesafe MRef with a regular monad
by Simon Peyton-Jones 06 Jun '03

06 Jun '03

Yes, one *could* use dynamic types. But the check would always succeed! That suggests a lack in the static type system. It's not surprising: the soundness depends on the un-forgeability of keys. So it's reasonable that there should be some language extension. I'm just looking for the minimal such extension. Finite maps see a bit of a big hammer. Simon | -----Original Message----- | From: Ralf Hinze [mailto:ralf@informatik.uni-bonn.de] | Sent: 06 June 2003 14:29 | To: Simon Peyton-Jones; Tim Sweeney; haskell(a)haskell.org; Ashley Yakeley | Subject: Re: Typesafe MRef with a regular monad | | Am Freitag, 6. Juni 2003 15:23 schrieb Simon Peyton-Jones: | > Oh bother, I forgot to add that you can of course insert a new value | > with an old key (suitably typed) and have it overwrite. Else, as you | > say, there would not be much point. | > | > Maybe it'd be better to have a separate key-construction function | > newKey :: k -> Key k a | > instead of having insert return a key. | > | > S | | Seriously, isn't this just an application of dynamics? The key | type allows us to insert a cast when looking up a data structure | of dynamic values? | | Cheers, Ralf |

2 1

RE: forall quantifier
by Simon Peyton-Jones 06 Jun '03

06 Jun '03

| classify :: Eq b => [a->b] -> [a] -> [[[a]]] | classify cs xs = ... | | where for each classifying function in cs, I would get the xs | partitioned accordingly. E.g. | | classify [fst,snd] [(1,0), (1,2), (2,0)] | | would yield | | [ [(1,0), (1,2)], [(2,0)] -- classified by `fst` | , [(1,0), (2,0)], [(1,2)]] -- classified by `snd` | | Now, obviously, the problem is that fst and snd, being passed in a | list, needs to be of the same type; this complicates classifying a | list of type [(Int,Bool)], for instance¹. Use existentials data Classifier a = forall b. Ord b => CL (a->b) classify :: [Classifier a] -> [a] -> [[[a]]] classify cls as = map (classify1 as) cls classify1 :: Classifier a -> [a] -> [[a]] classify1 (CL f) as = ... classify as using f.... Think of a classifier (CL f) as a pair of a) a function f:a->b b) an Ord dictionary for comparing b's I forget whether I've aired this on the list, but I'm seriously thinking that we should change 'forall' to 'exists' in existential data constructors like this one. One has to explain 'forall' every time. But we'd lose a keyword. Simon

4 3

RE: Typesafe MRef with a regular monad
by Simon Peyton-Jones 06 Jun '03

06 Jun '03

Oh bother, I forgot to add that you can of course insert a new value with an old key (suitably typed) and have it overwrite. Else, as you say, there would not be much point. Maybe it'd be better to have a separate key-construction function newKey :: k -> Key k a instead of having insert return a key. S | -----Original Message----- | From: Ralf Hinze [mailto:ralf@informatik.uni-bonn.de] | Sent: 06 June 2003 14:12 | To: Simon Peyton-Jones; Tim Sweeney; haskell(a)haskell.org; Ashley Yakeley | Subject: Re: Typesafe MRef with a regular monad | | > A more concrete way to formulate a problem that I believe to be | > equivalent is this. Implement the following interface | > | > module TypedFM where | > data FM k -- Abstract; finite map indexed by keys | > of type k | > data Key k a -- Abstract; a key of type k, indexing a | > value of type a | > | > empty :: FM k | > insert :: Ord k => FM k -> k -> a -> (FM k, Key k a) | > lookup :: Ord k => FM k -> Key k a -> Maybe a | > | > The point is that the keys are typed, like Refs are. But the finite map | > FM is only parameterised on k, not a, so it can contain (key,value) | > pairs of many different types. | > | > I don't think this can be implemented in Haskell, even with | > existentials. But the interface above is completely well typed, and can | > be used to implement lots of things. What I *don't* like about it is | > that it embodies the finite-map implementation, and there are too many | > different kinds of finite maps. | | Here is a Haskell 98 implementation: | | > module TypedFM | > where | | > data FM k = FM | > data Key k a = Key k a | | > empty = FM | > insert FM k a = (FM, Key k a) | > lookup FM (Key k a) = Just a | | Cheers, Ralf |

2 1

RE: Typesafe MRef with a regular monad
by Simon Peyton-Jones 06 Jun '03

06 Jun '03

| Conjecture: It's impossible to implement RefMonad directly in Haskell | without making use of built-in ST or IO functionality and without unsafe or | potentially diverging code (such as unsafeCoerce). A more concrete way to formulate a problem that I believe to be equivalent is this. Implement the following interface module TypedFM where data FM k -- Abstract; finite map indexed by keys of type k data Key k a -- Abstract; a key of type k, indexing a value of type a empty :: FM k insert :: Ord k => FM k -> k -> a -> (FM k, Key k a) lookup :: Ord k => FM k -> Key k a -> Maybe a The point is that the keys are typed, like Refs are. But the finite map FM is only parameterised on k, not a, so it can contain (key,value) pairs of many different types. I don't think this can be implemented in Haskell, even with existentials. But the interface above is completely well typed, and can be used to implement lots of things. What I *don't* like about it is that it embodies the finite-map implementation, and there are too many different kinds of finite maps. There is, I guess, some nice language extension that would enable one to program TypedFM, rather than provide it as primitive; but I don't know what it is. Simon

2 1

RE: ANN: H98 FFI Addendum 1.0, Release Candidate 10
by Simon Peyton-Jones 06 Jun '03

06 Jun '03

| Or maybe it would be better to provide some useful guidance? How about, | | To preserve the soundness of the type system, the result of | unsafePerformIO should always have a monomorphic type. For | example, | | listRef = unsafePerformIO (newIORef []) | | is unsafe, while | | listRef = unsafePerformIO (newIORef ([] :: [Int])) | | is type safe. In the first case listRef is assigned type IORef | [a], which makes it possible to store a list of one type and fetch | it with a different type. Yes! Yes! Advice is good! Simon

3 2

Gtk2hs - developer snapshot 0.9.3 now available
by Axel Simon 05 Jun '03

05 Jun '03

This release should compile on FreeBSD, Linux, MacOS X, Solaris and Windows. It features loads of small additions, in particular many functions of the Pixbuf library. It compiles against Gtk 2.0 and Gtk 2.2. Despite the fact that the configure script suggests it, GtkGLExt and OpenGL is not yet supported (but this is certainly one of the next goals). Concerning the future development of gtk2hs: The Gtk library will exhibit the same interface as it does now. Once the Common GUI API effort produces some first suggestions, the Mogul layer will change accordingly. The only useful thing in Mogul are the table functions which could be moved into Gtk, so I hope this will not result in major problems. Please report all bugs and requests to: gtk2hs-users(a)sourceforge.net Thanks for taking interest in gtk2hs, Axel.

2 1

categories: technical question about omega-categories
by Philippe Gaucher 05 Jun '03

05 Jun '03

Dear all, Let C be an omega-category (strict, globular). Let U be the forgetful functor from strict globular omega-categories to globular sets. And let F be its left adjoint. Let us suppose that we are considering an equivalence relation R on UC (the underlying globular set of C) such that the source and target maps pass to the quotient : i.e. one can deal with the quotient globular set UC/R. The canonical morphism of globular sets UC --> UC/R induces a morphism of omega-categories F(UC) --> F(UC/R) by functoriality of F. Consider the following push-out in the category of omega-categories : F(UC) -----> F(UC/R) | | | | | | v v C ---------> D The morphism F(UC)-->C (the counit of the adjonction) is surjective on the underlying sets. The morphism F(UC)-->F(UC/R) is generally not surjective on the underlying sets : because by taking the quotient by R, one may add composites in F(UC/R) which do not exist in F(UC). However the intuition tells (me) that the morphism F(UC/R)-->D is surjective on the underlying sets : this morphism only adds in F(UC/R) the calculation rules of C : this is precisely what I want by introducing D. But I cannot see why with a rigorous mathematical argument. Thanks in advance. pg.

1 0

Collecting values from Functors?
by Graham Klyne 05 Jun '03

05 Jun '03

I'm trying to figure if there's any way I can use (say) monads to collect values from a Functor. For example, suppose I have a tree of some values that supports fmap, is there any way I can use the fmap function to collect a list of all the node values? #g ------------------- Graham Klyne <GK(a)NineByNine.org> PGP: 0FAA 69FF C083 000B A2E9 A131 01B9 1C7A DBCA CB5E

8 11