- Haskell - Haskell.org

FM 2003 Call for Tool Exhibition
by mailinglist-admin＠fmeurope.org 05 Jun '03

05 Jun '03

Sorry if some of you receive multiple copies of this message. Stefania Gnesi (FM2003 General Chair) ============================================================================== Call for Tool Exhibition ------------------------------------------------------------------------------ The 12th International FME Symposium Pisa, Italy - September 8-14, 2003 http://fme03.isti.cnr.it - fme03(a)isti.cnr.it ------------------------------------------------------------------------------ FM 2003, will host 7 Workshops, 8 Tutorials and 1 Day dedicated to the Industry besides the 3 days of the FME Symposium. Tool demonstrations will also take place during the symposium, with the opportunity of holding presentations for each tool. We will be glad to host tool demonstrations presenting tools based on formal technologies (e.g., theorem-proving, model-checking, static analysis, or other formal methods) and introducing also formal methods in the practice of industrial processes (technical, organizational, social, psychological aspects). Both industrial tools and tools developed in academia are welcome at the FME Tool Exhibition. Proposals comprising: * the completed form below and * a description of the tool (max. 5 pages) should be submitted electronically as contributions to the category "Tool Exhibition" at http://sttt.cs.uni-dortmund.de/fme2003/servlet/Conference Submission Deadline: June 9th Notification of Acceptance: July 1st In case of questions please contact the Tool Exhibition Chair: Tiziana Margaria Universität Dortmund and Metaframe Baroperstr. 301 D-44227 Dortmund, Germany Phone: +49 231 755 5804 Fax: +49 231 755 5802 E-mail:tiziana@ls5.cs.uni-dortmund.de http://ls5-www.cs.uni-dortmund.de/staff/margaria_cv.en.html We have also defined a sponsorship program, which may be of interest industrial exhibitors, see http://fme03.isti.cnr.it/fme-sponsprog.htm.

1 0

Safe and sound STRef [Was Implementing RefMonads in Haskell without ST,IO]
by oleg＠pobox.com 05 Jun '03

05 Jun '03

Back in September 2001, Koen Claessen wrote: ] Here is a little experiment I did a while ago. I was trying to isolate ] the capability of the ST monad to deal with different types at the ] same time.... I conjecture this functionality cannot be implemented ] in Haskell 98, nor in any of the known safe extensions of Haskell. Recently, Tim Sweeney wrote ] Is it possible to actually implement a working instance of RefMonad in ] Haskell, without making use of a built-in monad like IO or ST? The following code shows a safe and sound implementation of a polymorphic heap with references and updates. The heap is capable of storing of polymorphic, functional and IO values. All operations are *statically* checked. An attempt to alter a heap reference with a value of a mismatched type leads to a _compile-time_ error. Everything is implemented in Haskell98 + multiparameter classes with functional dependencies + overlapping instances. I suspect that the latter isn't strictly needed, but it's almost midnight. Most importantly, no IO or ST monad, no unsafePerformIO or unsafeCoerce, no existential types and no Dynamics are needed. It seems that the polymorphic updateable heap can be implemented safely. Although the code looks like a monadic code, the Monad class doesn't seem to be polymorphic enough to wrap our heap. Perhaps arrows will help. I'd like to remark first that the ST monad with polymorphic STRef can be implemented in Haskell98 + safe extensions _provided_ all the values question are in the class Show/Read. When we store values, we store their external representation. When we retrieve a value, we read it. Similarly for values in the Binary class. All such values are _safely_ coercible. The following code however does not make this assumption. In our heap below, we can even store polymorphic functions and IO values! First, the tags for values in our heap > data Zero > data Succ a > > class HeapTag a where > tag_value:: a -> Int > > instance HeapTag Zero where > tag_value _ = 0 > -- I just can't avoid the undefined arithmetics > instance (HeapTag t) => HeapTag (Succ t) where > tag_value _ = 1 + tag_value (undefined::t) The heap reference is the combination of the tag and the desired type. As we will see, the value of the second argument of the HeapRef doesn't actually matter -- only its type does. > data HeapRef t a = HeapRef t a Our heap is implemented as a polymorphic associative list > data Nil t v r = Nil > data Cons t v r = Cons t v r > > class PList ntype ttype vtype cdrtype where > cdr:: ntype ttype vtype cdrtype -> cdrtype > empty:: ntype ttype vtype cdrtype -> Bool > value:: ntype ttype vtype cdrtype -> vtype > tag:: ntype ttype vtype cdrtype -> ttype > > instance PList Nil ttype vtype cdrtype where > empty = const True > > instance (PList n t v r,HeapTag tag) => PList Cons tag vtype (n t v r) where > empty = const False > value (Cons t v r) = v > tag (Cons t v r) = t > cdr (Cons t v r) = r The following is the statically typed polymorphic heap itself: > class Heap t v h | t h -> v where > fetch:: (HeapRef t v) -> h -> v > alter:: (HeapRef t v) -> v -> h -> h > > instance (HeapTag t,PList Cons t v r) => Heap t v (Cons t v r) where > fetch _ p = value p > alter _ vnew (Cons t v r) = (Cons t vnew r) > > instance (HeapTag t,Heap t v r,PList Cons t' v' r) => > Heap t v (Cons t' v' r) where > fetch ref p = fetch ref $ cdr p > alter ref vnew (Cons t v r) = Cons t v $ alter ref vnew r Let's make our heap instances of a class Show, so we have something to show. > instance (PList Nil ttype vtype cdrtype) => Show (Nil ttype vtype cdrtype) > where > show _ = "[]" > instance (Show vtype, HeapTag ttype, PList Cons ttype vtype cdrtype, > Show cdrtype) => > Show (Cons ttype vtype cdrtype) > where > show x = (show $ (tag_value $ tag x, value x)) ++ " : " ++ (show $ cdr x) Let's take a few simple examples > tinc (x::t) = undefined::(Succ t) > tag_one = (undefined::(Succ Zero)) > acons = Cons > lst1 = acons tag_one 'a' $ Nil > lst2 = acons (tinc tag_one) 'a' $ acons tag_one True $ Nil > test1 = fetch (HeapRef tag_one 'z') lst1 The result is 'a'. We see that the value of the second argument of HeapRef doesn't actually matter. But its type sure does: if we uncomment the following line > -- test1' = fetch (HeapRef tag_one (1::Int)) lst1 we get an error: /tmp/o1.lhs:127: Couldn't match `Char' against `Int' Expected type: Char Inferred type: Int When using functional dependencies to combine Heap t v (Cons t v r), arising from the instance declaration at /tmp/o1.lhs:91 Heap (Succ Zero) Int (Cons (Succ Zero) Char (Nil t v r)), arising from use of `fetch' at /tmp/o1.lhs:127 When generalising the type(s) for `test1'' Indeed, the stored value is of type Char and we try to read it as an Int. More tests: > test21 = fetch (HeapRef tag_one False) lst2 > -- the latter test again makes sure that fetching is type safe > --test22' = fetch (HeapRef (tinc tag_one) False) lst2 > test22 = fetch (HeapRef (tinc tag_one) (undefined::Char)) lst2 Testing alternation: > testa1 = alter (HeapRef tag_one (undefined::Bool)) False lst2 > --gives: (2,'a') : (1,False) : [] > testa2 = alter (HeapRef (tinc tag_one) (undefined::Char)) 'y' lst2 > --gives: (2,'y') : (1,True) : [] Now we can bundle our heap with an allocation pointer > -- p is the heap, t is the next tag to allocate in p > data GHeap t p = GHeap t p > > instance (HeapTag t,Show p) => Show (GHeap t p) where > show (GHeap t p) = "Global heap: alloc ptr " ++ (show$tag_value t) ++ > "\n" ++ (show p) > init_gh = GHeap (undefined::Zero) Nil > fetch_gh ref (GHeap _ p) = fetch ref p > alloc_gh x (GHeap t p) = (HeapRef t x,GHeap (tinc t) (Cons t x p)) > alter_gh ref newval (GHeap t p) = GHeap t $ alter ref newval p And finally the big test. The test shows storing and altering regular values, polymorphic function values and even IO values. > test3 = do > let heap = init_gh > let (xref,heap1) = alloc_gh 'a' heap > let (yref,heap2) = alloc_gh [(1::Int),2,3] heap1 > let (zref,heap3) = alloc_gh (Just False) heap2 > putStrLn "\nAfter allocations" > print heap3 > > putStr "x is "; print $ fetch_gh xref heap3 > putStr "y is "; print $ fetch_gh yref heap3 > putStr "z is "; print $ fetch_gh zref heap3 > > let heap31 = alter_gh xref 'z' heap3 > let heap32 = alter_gh yref [] heap31 > let heap33 = alter_gh zref (Just True) heap32 > putStrLn "\nAfter updates" > print heap33 > putStr "x is "; print $ fetch_gh xref heap33 > putStr "y is "; print $ fetch_gh yref heap33 > putStr "z is "; print $ fetch_gh zref heap33 > > putStrLn "\nPolymorphic and IO values" > let (gref,heap4) = alloc_gh (\x->x+1) heap33 > let (href,heap5) = alloc_gh id heap4 > let (mref,heap7) = alloc_gh (putStrLn "Monad!") heap5 > putStr "g 1 is "; print $ (fetch_gh gref heap4) (1::Int) > putStr "h True is "; print $ (fetch_gh href heap5) True > putStr "h 'a' is "; print $ (fetch_gh href heap5) 'a' > putStr "m is "; (fetch_gh mref heap7) > > let heap71 = alter_gh mref (putStrLn "New Monad") heap7 > let heap72 = alter_gh gref (\x->x+5) heap71 > putStrLn "\nAfter updates to polymorphic and IO values" > putStr "g 1 is "; print $ (fetch_gh gref heap72) (1::Int) > putStr "m is "; (fetch_gh mref heap72) > return () I had many occasions to see that an attempt to retrieve the value of a wrong type or change the value with that of a wrong type result in a compiler error! Although we are "altering" polymorphic values, the type safeness seems to be preserved > test4 = do let heap = init_gh > let (xref,heap1) = alloc_gh [] heap > let (yref,heap2) = alloc_gh [(1::Int)] heap > let (zref,heap3) = alloc_gh [True] heap > let heap11 = alter_gh xref [(1::Int)] heap1 > --let z = fetch_gh zref heap11 > let z = fetch_gh zref heap1 > print z If we uncomment the commented line, we will get a type error! The lines like *> let (yref,heap2) = alloc_gh [(1::Int),2,3] heap1 *> let (zref,heap3) = alloc_gh (Just False) heap2 almost suggest a monad. Alas, the Monad class doesn't seem to be polymorphic enough. The type of the >>= is forall m b a. (Monad m) => m a -> (a -> m b) -> m b although 'b' at the end doesn't have to be the same as 'a' at the beginning, 'm' must be the same in the argument of >>= and in its result. However, in our example, heap2 has a type different from that of heap1. ghci -fglasgow-exts -fallow-undecidable-instances -fallow-overlapping-instances /tmp/o1.lhs

5 8

[tim@epicgames.com: Fw: Typesafe MRef with a regular monad]
by Andrew J Bromage 05 Jun '03

05 Jun '03

G'day all. On Wed, Jun 04, 2003 at 07:31:03PM -0500, Tim Sweeney wrote: > 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). > Any takers? WARNING: This is not rigorous. Take a prototypical simple state monad: type MyRefMon a = SomeState -> (a. SomeState) type MyRef a = Int -- Could be anything other than Int, but -- the important point is that "a" is not -- mentioned on the RHS anywhere. where SomeState is abstract but concrete. Note that it has no type parameters. Let's also assume the existence of this function: myDeref :: MyRef a -> MyRefMon a Again, we know nothing about its implementation (yet). Without loss of generality, and because a has no type constraints, myDeref is equivalent to a function of this type: myDeref' :: Int -> SomeState -> (a, SomeState) (This step I believe to be far too handwavy. I have no justification for the ability to drop the "a" parameter here except that Haskell semantics state that if a is not constrained, you can't do anything with it.) Intuitively, there is nothing in the above type signature which gives you any way to construct something of type a, therefore it must be bottom. The parametricity theorem (i.e. "free theorem") can probaly be used to show this formally. The only ways I can think of to get over this within Haskell is to: - change the definition of MyRef so that it contains enough information to extract something of type a from SomeState, or - constrain the type (e.g. using Typeable). Cheers, Andrew Bromage

1 0

RE: Haddock module description
by Graham Klyne 04 Jun '03

04 Jun '03

At 14:58 04/06/03 +0100, Simon Marlow wrote: >Haddock understands the style of module header that we're using for the >hierarchical libraries. The module header is described in this document >(see the section Reference Libraries->Coding Style->Module Header): > >http://www.haskell.org/hierarchical-modules/libraries/libraries.html Great... just what I wanted. Thanks. #g ------------------- Graham Klyne <GK(a)NineByNine.org> PGP: 0FAA 69FF C083 000B A2E9 A131 01B9 1C7A DBCA CB5E

1 0

forall quantifier
by ketil＠ii.uib.no 04 Jun '03

04 Jun '03

Hi, This is one of those topics everybody else seems to be familiar with, but which I don't quite understand, and can't seem to find any good information about. I have a function declared as: anova2 :: (Fractional c, Ord b) => [a->b] -> (a->c) -> [a] -> [Anova1 c] where the first parameter is a list of classifiers. I could simplify it, I guess, to something like 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¹. I have a vague notion this is solvable using quantifiers (since I ever only use Eq operations on the type), but I'm not sure exactly how, I can't seem to find a good tutorial, and my Monte-Carlo programming approach doesn't seem to be leading anywhere :-) Can somebody suggest a solution, or a place to look? -kzm ¹ I guess I can convert Bool to Int (True->1, False->0), but it's not very appealing, IMHO. -- If I haven't seen further, it is by standing in the footprints of giants

4 3

RE: forall quantifier
by Markus.Schnell＠infineon.com 04 Jun '03

04 Jun '03

Yes, this would work, thanks. But let me extent my question: what if all the types would be in a class FakeClass which has function specialID :: a -> ID and I would like to do > foo $ map specialID [a,b,c,d] ?

2 1

RE: Haddock module description
by Simon Marlow 04 Jun '03

04 Jun '03

> The Haddock document [1] section 3.3 gives a very simple > specification for > the module description, but the accompanying examples [2][3] > suggest that > certain common layout in the module description is picked up > and formatted > specially. Is there a description of this? Haddock understands the style of module header that we're using for the hierarchical libraries. The module header is described in this document (see the section Reference Libraries->Coding Style->Module Header): http://www.haskell.org/hierarchical-modules/libraries/libraries.html Cheers, Simon

1 0

Re: labelled fields
by George Russell 04 Jun '03

04 Jun '03

Steffen wrote > I need something like > > data Type = TCon String {lmtc::Maybe String} ... > > but this does not seem to be possible. Instead > I have to waste identifiers: > > data Type = TCon {senseless::String,lmtc::Maybe String} ... > > Why? Are there any formal reasons against the > above declaration? Clearly it's arguable, since SML allows general record types. My SML syntax is rusty but I think you could write: > datatype ty = ty string {lmtc : string option} or indeed use {lmtc : string option} just like a type. I don't think haskell(a)haskell.org is suitable for lengthy discussions of the merits of SML versus Haskell or vice-versa, so I will state my view and leave it at that: (1) the Haskell approach costs you slightly more typing. (2) on the other hand the error messages are slightly better, since if you type TCon {sensless = "foo"} the compiler should spot immediately that "sensless" has no place in a TCon, while in ML the compiler will have to say something like "Expecting a {senseless :: String}, found a {sensless :: String}", which leaves you to work out what it is about the context that requires a "{senseless :: String}" (3) the Haskell approach allows several constructors to have the same field name, for example > data Ty1 = > TCon1 {lmtc :: Maybe String} > | TCon2 {lmtc :: Maybe String, extraField :: String} and you then have a function lmtc :: Ty1 -> Maybe String which works for all constructors having the lmtc field. (4) Haskell will fill in undefined fields, with values that give error messages if you try to look at them. Which you prefer is entirely up to you. None of the above points are terribly important. I personally prefer the Haskell approach, but not by much.

1 0

RE: forall quantifier
by Markus.Schnell＠infineon.com 04 Jun '03

04 Jun '03

> 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¹. I have a similar problem. Say I have a record: > data Rec = Rec { a :: Int, b :: Type1, c :: Type2, d :: Type3, ... } > rec = Rec { a = 1, b = ... } Now I want to print part of the record. What I would like to do is the following > putStrLn $ concatMap show [a,c,d] !!! bang !!! So what I actually do is > putStrLn $ concat [show a, show c, show d] Works, but a little bit clumsy, especially with long lists. Is there a nice solution? Markus

3 2

Haddock module description
by Graham Klyne 04 Jun '03

04 Jun '03

The Haddock document [1] section 3.3 gives a very simple specification for the module description, but the accompanying examples [2][3] suggest that certain common layout in the module description is picked up and formatted specially. Is there a description of this? (I'm starting to put simple Haddock markup into my code, but I'm not running Haddock yet so I'm not yet ready to "suck it and see".) #g -- [1] http://www.haskell.org/haddock/docs/x355.html [2] http://www.haskell.org/haddock/Test.hs [3] http://www.haskell.org/haddock/Test/Test.html ------------------- Graham Klyne <GK(a)NineByNine.org> PGP: 0FAA 69FF C083 000B A2E9 A131 01B9 1C7A DBCA CB5E

1 0