June 2003 - Haskell - Haskell.org

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

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