Re: [Haskell-cafe] lambda calculus and equational logic
On 14/07/2010, at 6:26 , Patrick Browne wrote: Thanks for your clear and helpful responses. I am aware that this question can lead to into very deep water. I am comparing Haskell with languages based on equational logic (EL) (e.g. Maude/CafeOBJ, lets call them ELLs). I need to identify the fundamental distinction between the semantics of ELLs and Haskell. The focus of my original question was just the purely functional, side effect free, part of Haskell. If you ignore anything to do with the IO monad (or ST), then all of Haskell can be desugared to (untyped) call-by-name/need lambda calculus. If you stick with Haskell98 then you can desugar it to the rank-2 fragment of System-F + algebraic data types + case expressions + appropriate constants and primops. This is generally regarded as the Haskell Kernel Language, which is mentioned but explicitly not defined in the language standard. The relationship between the denotational and the proof theoretic semantic is important for soundness and completeness. Which was sort of behind my original question. Would it be fair to say 1) Lambda calculus provides the operational semantics for Haskell Notionally yes, but practically no. AFAIC there isn't a formal semantics for Haskell, but there is for fragments of it, and for intermediate representations like System-Fc (on which GHC is based). There are also multiple lambda calculi, depending on which evaluation mechanism you use. The point I was trying to make in the previous message is what while Haskell includes the IO monad, people insist on calling the whole language purely functional and side effect free, which is murky territory. Sabry's What is a Purely Functional Language shows that unrestricted beta-reduction is not sound in a simple monadic language using a pass-the-world implementation -- though Wouter's paper gives a cleaner one. Another paper that might help is Sondergaard and Sestoft's highly readable Referential Transparency, Definiteness and Unfoldability. 2) Maybe equational logic provides the denotational semantics. 3)I am not sure of proof theoretic semantic for Haskell. The Curry-Howard correspondence is a proof theoretic view but only at type level. Obviously, the last three points are represent my efforts to address this question. Hopefully the café can comment on the accuracy of these points. My (limited) understanding of Maude is that rewrites can happen at any point in the term being reduced. This is different from, say, the semantics of call-by-name lambda calculus which has a specific evaluation order. In Haskell it's no problem to pass a diverging expression to some function, which might store it in a data structure, but then discard it later. However, when rewrites can happen at any point in the term being reduced, if any part of it diverges then the whole thing does. This is just from skimming slides for Maude talks though... Ben. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: cryptohash and an incremental API
On Mon, Jul 12, 2010 at 02:52:10PM -0700, Thomas M. DuBuisson wrote: I've been working on a new crypto library specifically to provide a unified API for packages implementing cryptographic algorithms. You can see the discussions on librar...@haskell.org [1] [2]. Please feel free to take a look, comment, contribute, and hopefully move to the interface. I should be finishing up BlockCipher modes and adding hash tests soon. Hi Thomas, first, I think that's a great efforts to standardize the crypto API ! couple of comments around the hashes interface: * updateCtx works on blockLength, instead of working on arbitrary size: while this does represent what the underlaying algorithm do, letting the algorithm implementation process any size is, I think, better. chunking the bytestring might have a significant cost (a rope based implementation would not suffer this), and in my case, processing as much as possible at each update call, prevent from suffering from the marshalling/unmarshalling cost of the mutable state. * hash is a generic operation based on the class Hash. In my case, it improve performance by not running the pure init/update/finalize exposed, but use the hidden impure function. I realized yesterday it's not as much as i though since i had a bug in my benchmark, but it's still there (100ms for 500mb of data). * Why is the digest of a specific type ? I like representing different things with different types, but i'm not sure what do you gain with digests though. * is strength really useful in the Hash class ? it might be accurate when the thing get implemented, but i'm not sure what would happens over time, and flaws are discovered. would people actually updates it ? The blockCipher should exposes the chaining modes as overridable typeclass functions, with default generic implementations that use encryptBlocks. For example the haskell AES package has different C implementations for each chaining modes (e.g. cbc, ebc), and i suspect that using a generic chaining implementation would slow things down. what about something like: -- each plaintext bytestring need to be a multiple of blockSize class (Binary k, Serialize k) = BlockCipher k where blockSize:: Tagged k BitLength encryptBlocks:: k - ByteString - ByteString decryptBlocks:: k - ByteString - ByteString encryptBlocksCBC :: k - ByteString - (k, ByteString) encryptBlocksCBC = genericCBC encryptBlocks decryptBlocksCBC :: k - ByteString - (k, ByteString) .. same for ebc, ... buildKey:: ByteString - Maybe k keyLength :: k - BitLength -- ^ keyLength may inspect... and my last comment, is that i don't understand the streamcipher interface you're proposing. I've got a (inefficient) RC4 implementation that has this interface: stream :: Ctx - B.ByteString - (Ctx, B.ByteString) streamlazy :: Ctx - L.ByteString - (Ctx, L.ByteString) I'm not sure how it would fit this interface (some kind of state monad ?): encryptStream :: k - B.ByteString - B.ByteString I hope that's useful comments, -- Vincent Hanquez ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Collecting MonadError errors generically
Leon Grynszpan wrote:
What I want, instead, is to run a whole bunch of
computations that may throw errors. If there are any errors, I want to
collect them all into one big master error. If not, I want a list of
results. Here's an example of usage:
couldThrowError :: (Error e, MonadError e m) = t1 - m t2
getParams :: (Error e, MonadError e m) = [t1] -- m [t2]
getParams = groupErrors . map couldThrowError
I found it pretty easy to implement groupErrors for Either String:
...
The problem, though, is that running this function now causes type
inference to provide Either String as my MonadError implementation...
It would be nice if I could stay generic.
You might find the following two functions useful:
reify :: (Error e, MonadError e m) = m a - m (Either e a)
reify m = (m = return . Right) `catchError` (return . Left)
-- Not needed here, but very nice to have anyway
reflect :: (Error e, MonadError e m) = m (Either e a) - m a
reflect m = m = either throwError return
Then groupErrors can be written almost the same way you wrote for
the Either String monad -- but now generically
groupErrors :: (Monoid e, Error e, MonadError e m) = [m a] - m [a]
groupErrors lst = mapM reify lst = \lst -
case partitionEithers lst of
([],xs) - return xs
(errs,_) - throwError (mconcat errs)
If you don't like the Monoid constraint, this is fine. But you have to
provide then some other way to group errors. For example, you could
use the new extensible exceptions.
Here is the rest of the code:
couldThrowError :: (MonadError String m) = String - m Int
couldThrowError s = case reads s of
[(n,)] - return n
_- throwError $ parse error: ++ s ++ \n
getParams :: (Monoid e, Error e, MonadError e m) =
(t1 - m t2) - [t1] - m [t2]
getParams f = groupErrors . map f
test :: Either String [Int]
test = getParams couldThrowError [1,2,a,b]
If you wish to know more about reify and reflect, a good paper to
start is the following. Section 1.2 talks directly about exception monads.
@InProceedings{ filinski-representing,
author= Andrzej Filinski,
title = Representing Monads,
pages = 446--457,
crossref = popl1994,
url = http://www.diku.dk/~andrzej/papers/RM-abstract.html
http://www.diku.dk/~andrzej/papers/RM.dvi
http://www.diku.dk/~andrzej/papers/RM.ps.gz;,
abstract = We show that any monad whose unit and extension
operations are expressible as purely functional terms can be embedded
in a call-by-value language with ``composable continuations''. As part
of the development, we extend Meyer and Wand's characterization of the
relationship between continuation-passing and direct style to one for
continuation-passing vs.~general ``monadic'' style. We further show
that the composable-continuations construct can itself be represented
using ordinary, non-composable first-class continuations and a single
piece of state. Thus, in the presence of two specific computational
effects---storage and escapes---\emph{any} expressible monadic
structure (e.g., nondeterminism as represented by the list monad) can
be added as a purely definitional extension, without requiring a
reinterpretation of the whole language. The paper includes an
implementation of the construction (in Standard ML with some New
Jersey extensions) and several examples.
}
There is a follow-up:
@InProceedings{ filinski-layered,
author= Andrzej Filinski,
title = Representing Layered Monads,
pages = 175--188,
crossref = popl1999,
url = http://www.diku.dk/~andrzej/papers/RLM-abstract.html
http://www.diku.dk/~andrzej/papers/RLM.dvi
http://www.diku.dk/~andrzej/papers/RLM.ps.gz;,
}
The term reification has been introduced 26 years ago:
@InProceedings{ friedman-reification,
author= {Daniel P. Friedman and Mitchell Wand},
title = {Reification: Reflection without Metaphysics},
pages = {348--355},
crossref = lfp1984,
abstract = {We consider how the data structures of an
interpreter may be made available to the program it is running, and
how the program may alter its interpreter's structures. We refer to
these processes as reification and reflection. We show how these
processes may be considered as an extension of the fexpr concept in
which not only the form and the environment, but also the
continuation, are made available to the body of the procedure. We show
how such a construct can be used to effectively add an unlimited
variety of ``special forms'' to a very small base language. We
consider some trade-offs in how interpreter objects are reified. Our
version of this construct is similar to one in 3-Lisp [Smith 82, 84],
but is independent of the rest of 3-Lisp. In particular, it does not
rely on the notion of a tower of interpreters.}
}
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
Re: [Haskell-cafe] lists of arbitrary depth
On Tue, Jul 13, 2010 at 11:28 AM, Shlomi Vaknin shlomivak...@gmail.com wrote: Thank you Bob, your example clarified how actually using such data type would appear in haskell. I naively thought it would be as simple as defining a regular list, but i see it is slightly more strict than that. I appreciate your help! Vadali Well it _is_ as simple as defining a regular list, which would be (fictionally since (:) and [] are reserved identifiers) : data [] a = [] | a : [a] Which is the same as : data List a = Empty | Cons a (List a) You can then handle lists with pattern matching : map f [] = [] map f (x:xs) = f x : map f xs Or for our List type : map f Empty = Empty map f (Cons x xs) = Cons (f x) (map f xs) His definition of a tree : data Tree a = Leaf | Branch a [Tree a] follows the same idea and is as easy to handle with pattern matching : treeMap f Leaf = Leaf treeMap f (Branch x xs) = Branch (f x) (map (treeMap f) xs) As you see, an user defined type is manipulated with the same mechanism as a primitive type, this uniformity is part of the power of Haskell in that it encourages users to create their types and allows seamless integration of external library types with primitive types. -- Jedaï ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: [Haskell] ANNOUNCE: Haskell 2010 Report (final)
On 14/07/2010 03:36, John Meacham wrote: On Tue, Jul 13, 2010 at 10:24:00AM +0100, Simon Marlow wrote: Well, a main useful case is that I can do -phaskell98 and -phaskell2010 at the same time. So I can make the default jhc behavior be the union of the two languages easily. That works in GHC too: the modules of those two packages don't overlap. That is partly because we never moved Prelude from base to haskell98. But don't you still have to have things directly declare they depend on 'base' then in order to get 'Prelude'? The extra dependency on the implementation specific 'base' because you want both haskell98 and haskell2010 is what I am trying to avoid. In GHC 6.14.1 you'll be able to depend on haskell2010 instead of base if you wish, and we'll recommend doing so where it makes sense (indeed, if you use haskell2010 then you *cannot* also depend on base). Also, haskell98 and haskell2010 can be used together if you really want to. Cheers, Simon ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: [Haskell] ANNOUNCE: Haskell 2010 Report (final)
On 12/07/2010 22:12, John Meacham wrote: Yeah, I didn't realize how important the allocator was until I started benchmarking, spending time cutting the cost of marking garbage in half didn't help nearly as much as shaving a few cycles off the allocator. The fast pass of the allocator is actually very fast, each object type has its own allocator and free list so allocation is pretty much just pulling an object off of the free list, it is already of the appropriate size and its constant fields are pre-initialized as they arn't cleared during garbage collection. (there is a heuristic that claims full pages back to the general pool sometimes). The slow path has to grab a full page and initialize it, but that isn't really much slower as I can prefetch the cache lines needed so the cost is on the order of another cache line fill. (thinking about computational complexity in terms of O(cache line fills) rather than O(operations) is much more appropriate on todays architectures.). Right, you can see how important locality is by looking at these graphs that Don produced recently: http://haskell.org/haskellwiki/Ghc-gc-tune generational GC these days is important more for locality than for the benefits of avoiding repeated tracing. Speaking of prefetching, we get a lot of benefit in GHC from the automatic prefetching done by modern CPUs; I'm not sure how this would be affected by having multiple allocation regions. Manual prefetching is almost impossible to get right in my experience, see also Nethercote/Mycroft where they did some prefetching experiments with GHC: http://portal.acm.org/citation.cfm?id=773044 Cheers, Simon ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Comments on Haskell 2010 Report
Alex, many thanks for all these comments, I've fixed all the problems you pointed out, except for: On 09/07/2010 03:25, Alex Stangl wrote: 6. In section 3.17.2, the example that is supposed to return [undefined,undefined,undefined] seems like it really ought to return undefined, although I can see in the description above for ~apat matching where the other interpretation would hold. I actually tried this in GHC 10.4.2, binding the result to a variable and then applying the function length to it, and it comes back with undefined, whereas performing length [undefined,undefined,undefined] returns 3. So it appears that in this case, at least GHC 10.4.2 is returning undefined rather than [undefined,undefined,undefined]. did you mean this one? (\ ~(x:xs) - x:x:xs) ⊥ ⇒ ⊥:⊥:⊥ it is returning undefined:undefined:undefined, which is different from [undefined,undefined,undefined]. 10. Section 7.1 uses function in places where it ought to use action. It seems more correct to describe print as returning an action that outputs a value. Most of the Input Functions (e.g., getChar, getLine, getContents, readLn) should be described as actions, not functions. It switches to using the term operation, which seems better, but then reverts back to function. This is a larger change, I'll defer it to Haskell 2011 along with some other nomenclature-related cleanup I'd like to get done. 20. In heading for 20.9.2, quotes around Set are not balanced. Both are closing quotes. Ditto for 20.10.1, 20.10.2. and 22. In section 38.2, first occurrence of 'dual' has mismatched quotes. and 23. In section 41.1, quotes around perform are mismatched. Word function is mildly misused again here. the quotes are wrong, but it would be a fiddle to fix it in Haddock, so I'm punting on that. 25. In section 41.4.4, bullet before isPermissionError isn't rendered correctly. I can't see that - perhaps it has been fixed already. Cheers, Simon ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Applying a value to a function generically
Hello, I would like to construct a collection of function-like objects on which I could apply some value, in a typesafe and clean way. Let's say I have something like this: data Fun = forall a b . F (a - b) type Callables = Map String Fun I would like to be able to write: invoke :: Callables - a - String - b invoke m d k = case lookup k m of Just (F f) - f d Nothing - error $ unable to find function for key ++ k which of course does not compile nor even make sense. I suspect I need to have more information in Fun to be able to apply functions correctly, but don't know where to look at. I read recently an article about implicit configurations that used some type wizardry to ensure correct and typesafe use of external data and sounded pretty cool, (http://www.cs.rutgers.edu/~ccshan/prepose/prepose.pdf) but I suspect this is 1) too complex for me an 2) overkill for my problem. Could someone point me in the right direction ? Thanks in advance Arnaud ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Applying a value to a function generically
On Wed, Jul 14, 2010 at 8:25 AM, Arnaud Bailly arnaud.oq...@gmail.com wrote: Hello, I would like to construct a collection of function-like objects on which I could apply some value, in a typesafe and clean way. You could use Data.Typeable.cast [1] [1] http://haskell.org/ghc/docs/6.12.1/html/libraries/base-4.2.0.0/Data-Typeable.html#v%3Acast Let's say I have something like this: data Fun = forall a b . F (a - b) type Callables = Map String Fun Sorry, but using GADT syntax: data Fun where F :: (Typeable a, Typeable b) = (a - b) - Fun I would like to be able to write: invoke :: Callables - a - String - b invoke m d k = case lookup k m of Just (F f) - f d Nothing - error $ unable to find function for key ++ k Untested: invoke :: (Typeable a, Typeable b) = Callables - a - String - Maybe b invoke m d k = do F f - lookup k m arg - cast d cast (f arg) HTH! -- Felipe. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Applying a value to a function generically
2010/7/14 Felipe Lessa felipe.le...@gmail.com: On Wed, Jul 14, 2010 at 8:25 AM, Arnaud Bailly arnaud.oq...@gmail.com wrote: Hello, I would like to construct a collection of function-like objects on which I could apply some value, in a typesafe and clean way. You could use Data.Typeable.cast [1] [1] http://haskell.org/ghc/docs/6.12.1/html/libraries/base-4.2.0.0/Data-Typeable.html#v%3Acast [snip] Or maybe Data.Dynamic with type Callables = Map String Dynamic You can extract the function with fromDynamic in a type-safe way (it returns a Maybe). Probalby you might want 'invoke' to return a Maybe too (just like Felipe did). Cheers, Thu ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Please report any bug of gtk2hs-0.11.0!
bri...@aracnet.com writes: Short version of this post: Looks like the intsall depends on alex and that dependencies doesn't appear to be handled, i.e. I had to install alex before proceeding. why do is it called gtk2hs if you are actually installing package gtk ;-) Because before gtk2hs cabalized package release (gtk2hs-0.11.0), we put many gtk+ base package in *one* repository. Currently, glib, gio, cairo, pango, gtk still in repository : http://code.haskell.org/gtk2hs Where's the demo directory ?! Sorry, we forgot add demo in .cabal file when we released gtk2hs-0.11.0, We will include all demos in gtk2hs-0.11.1 Moral of the story: don't forget to install -dev version of the necessary libraries. For me that was libpango1.0-dev, libgtk2.0-dev and libglib2.0-dev. The long version: I have a debian system and I expect the problems I found to be relatively common. Hope this is useful. First I found that I needed package alex. then i was able to cabal install gtk2hs-buildtools however cabal install gtk didn't work: Configuring glib-0.11.0... setup: The pkg-config package glib-2.0 is required but it could not be found. cabal: Error: some packages failed to install: gio-0.11.0 depends on glib-0.11.0 which failed to install. glib-0.11.0 failed during the configure step. The exception was: ExitFailure 1 gtk-0.11.0 depends on glib-0.11.0 which failed to install. pango-0.11.0 depends on glib-0.11.0 which failed to install. cabal install glib Configuring glib-0.11.0... setup: The pkg-config package glib-2.0 is required but it could not be found. cabal: Error: some packages failed to install: glib-0.11.0 failed during the configure step. The exception was: ExitFailure 1 now it's not obvious to me at this point if it's referencing a cabal package glib-2.0 or the unix libs. But I'm going to guess it's actually the unix libs. I do have the unix libs installed : ii libglib2.0-0 2.24.1-1 The GLib library of C routines However I remembered that annoying little thing that there is always those darn -dev versions of the lib that you need when you actually want to compile against libraries. So I installed it and got farther along, crashing on pango. Turns out it's the same problem. So install libpango1.0-dev and continue... Stopped again on gtk+, aka gtk libgtk2.0-dev. Installed it, and trudged on. I noticed that the install process stays at this point for a long time: Preprocessing library gtk-0.11.0... But it does eventually continue, and it even completes successfully ! Strangely, at this point, I find that I don't know that I actually have gtk2hs installed. I know that this sound kinda dumb, but I just did cabal install gtk, right ? I immediately tried cabal install gtk2hs, which said no such library, and realized that gtk was it :-) So I'd like to run a demo to make sure things are installed properly. Running the demos. -- To get started, you can compile and run one of the programs that reside in the demo/ directory in the respective packages. For example: ~/gtk2hs/gtk/demo/hello:$ make But after the installation the demo directory is nowhere to be found. Do you need to pull it in with darcs ?? Brian On Tue, 13 Jul 2010 11:42:26 +0200 Christian Maeder christian.mae...@dfki.de wrote: Andy Stewart schrieb: Hi all, We plan to release bug fix version : gtk2hs-0.11.1 Please report any bug of gtk2hs-0.11.0, we will fix it before release gtk2hs-0.11.1 I'm looking forward for this bug-fix release (since gtk2hs-0.11.0 did not work for me). Because I've almost missed this message I reply to gtk2hs-us...@lists.sourceforge.net, too. Christian We plan to add many new APIs in gtk2hs-0.12.0, so gtk2hs-0.11.1 will be the last stable version with current APIs. Thanks for your help! -- Andy ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Comments on Haskell 2010 Report
On Wed, Jul 14, 2010 at 12:10:48PM +0100, Simon Marlow wrote: it is returning undefined:undefined:undefined, which is different from [undefined,undefined,undefined]. My mistake. I should have read more carefully. 25. In section 41.4.4, bullet before isPermissionError isn't rendered correctly. I can't see that - perhaps it has been fixed already. Check the failure codes for hSeek. It was still there in the HTML version, at least, when I checked this morning. Thanks, Alex ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Please report any bug of gtk2hs-0.11.0!
On Wed, 14 Jul 2010 21:05:35 +0800 Andy Stewart lazycat.mana...@gmail.com wrote: Where's the demo directory ?! Sorry, we forgot add demo in .cabal file when we released gtk2hs-0.11.0, We will include all demos in gtk2hs-0.11.1 I think that would be very helpful. It's a big package with lots of dependencies, so the first thing I would do is run a couple of demos to make sure it installed correctly. As an aside for those interested, the demos are in the gtk2hs tarballs available for download from the sourceforge page. Kudos to the team ! Overall it went quite smoothly and will make it considerably easier to install. I know that I couldn't get things to work last time I tried... Brian ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Call for Copy: Monad.Reader Issue 17
Whether you're an established academic or have only just started learning Haskell, if you have something to say, please consider writing an article for The Monad.Reader! The submission deadline for Issue 17 will be: **Friday, October 1, 2010** The Monad.Reader The Monad.Reader is a electronic magazine about all things Haskell. It is less formal than journal, but somehow more enduring than a wiki page. There have been a wide variety of articles: exciting code fragments, intriguing puzzles, book reviews, tutorials, and even half-baked research ideas. Submission Details ~~ Get in touch with me if you intend to submit something -- the sooner you let me know what you're up to, the better. Please submit articles for the next issue to me by e-mail (byorgey at cis.upenn.edu). Articles should be written according to the guidelines available from http://themonadreader.wordpress.com/contributing/ Please submit your article in PDF, together with any source files you used. The sources will be released together with the magazine under a BSD license. If you would like to submit an article, but have trouble with LaTeX please let me know and we'll work something out. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] IFL 2010: 3rd CFP and 1st Call for Participation
3RD CALL FOR PAPERS and 1ST CALL FOR PARTICIPATION 22nd Symposium on Implementation and Application of Functional Languages (IFL 2010) September 1-3, 2010 Utrecht University Alphen aan den Rijn, The Netherlands http://www.cs.uu.nl/ifl2010 *** **Submission and Registration are now both OPEN ** ** If you intend to participate in IFL 2010, help us by registering as soon as possible. ** ** ** **Submission closes July 25, Registration closes August 1 ** *** After a first successful visit to the USA, the Symposium on Implementation and Application of Functional Languages returns to Europe for its 22nd edition. The hosting institution is Utrecht University in the Netherlands, although the conference itself will take place in the ornithological theme park Avifauna in Alphen aan den Rijn, situated conveniently close to Schiphol (Amsterdam Airport). The symposium dates are September 1-3, 2010. The goal of the IFL symposia is to bring together researchers actively engaged in the implementation and application of functional and function-based programming languages. IFL 2010 will be a venue for researchers to present and discuss new ideas and concepts, work in progress, and publication-ripe results related to the implementation and application of functional languages and function-based programming. Following the IFL tradition, IFL 2010 will use a post-symposium review process to produce formal proceedings which will be published by Springer Verlag in the Lecture Notes in Computer Science series. All participants in IFL 2010 are invited to submit either a draft paper or an extended abstract describing work to be presented at the symposium. At no time may work submitted to IFL be simultaneously submitted to other venues. Here we follow the ACM Sigplan republication policy as defined on http://www.sigplan.org/republicationpolicy.htm. The submissions will be screened by the program committee chair to make sure they are within the scope of IFL, and will appear in the draft proceedings distributed at the symposium. Submissions appearing in the draft proceedings are not peer-reviewed publications. After the symposium, authors will be given the opportunity to incorporate the feedback from discussions at the symposium and will be invited to submit a revised full article for the formal review process. These revised submissions will be reviewed by the program committee using prevailing academic standards to select the best articles, which will appear in the formal proceedings. INVITED SPEAKER Johan Nordlander of Lulea University, the designer and developer of the Timber language, is the invited speaker at IFL 2010. Timber is a functional programming language that draws some of its concepts from object-oriented programming, and has built-in facilities for concurrent execution. The language is specifically targeted at implementing real-time embedded systems. TOPICS IFL welcomes submissions describing practical and theoretical work as well as submissions describing applications and tools. If you are not sure that your work is appropriate for IFL 2010, please contact the PC chair at j...@cs.uu.nl. Topics of interest include, but are not limited to: language concepts type checking contracts compilation techniques staged compilation runtime function specialization runtime code generation partial evaluation (abstract) interpretation generic programming techniques automatic program generation array processing concurrent/parallel programming concurrent/parallel program execution functional programming and embedded systems functional programming and web applications functional programming and security novel memory management techniques runtime profiling and performance measurements debugging and tracing virtual/abstract machine architectures validation and verification of functional programs tools and programming techniques industrial applications of functional programming PAPER SUBMISSIONS Prospective authors are encouraged to submit papers or extended abstracts to be published in the draft proceedings and to present them at the symposium. All contributions must be written in English, conform to the Springer-Verlag LNCS series format and not exceed 16 pages. The draft proceedings will appear as a technical report of the Department of Computer Science of Utrecht University. SPONSORS IFL 2010 is sponsored by Microsoft Research. As a result we can offer decreased participation fees for Master students and PhD students who plan to attend or present at IFL 2010. PETER
[Haskell-cafe] Docs on the current and future constraint solver?
I believe I have run headlong into issue #3064 in ghc (http://hackage.haskell.org/trac/ghc/ticket/3064). All I think I know is this: * this is a performance issue with the system used to solve type constraints. * the solver is undergoing an overhaul to resolve performance issues in addition to other issues. * An efficient constraint solver is difficult. NP-Complete in the general case? Beyond that I'm at a loss. What can I read to understand the constraint satisfaction problem as it stands in GHC? Is there a paper on the implementation of the current solver? Anything on how the new solver will differ from the current? I think I located one page on the new solver: http://hackage.haskell.org/trac/ghc/wiki/TypeFunctionsSolving Cheers, Corey O'Connor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: cryptohash and an incremental API
Vincent said:
couple of comments around the hashes interface:
* updateCtx works on blockLength, instead of working on arbitrary size...
So for performance reasons you seem to prefer Semantics 1.2?
1.2 Multiple of blockSize bytes
Implementations are encouraged to consume data (continue updating,
encrypting, or decrypting) until there is less than blockSize bits
available.
Also, I'll amend 1.2 and say the hashUpdate/encrypt/decrypt functions
should only consume n * blockSize bytes, tracking the remainder will
be done at the higher level. Also, the higher level default
implementations should only pass n * blocksize inputs to these
functions.
I can see how that's reasonable and am strongly considering using
these semantics instead of 1.1.
* hash is a generic operation based on the class Hash. In my case, it improve
performance by not running the pure init/update/finalize exposed, but use the
hidden
impure function. I realized yesterday it's not as much as i though since i had
a bug in my benchmark, but it's still there (100ms for 500mb of data).
Humm, 0.2 sections / GB is significant so again I can be swayed - it
isn't like I can't have a default definition of hash (and others) when
its part of the class instance.
* Why is the digest of a specific type ? I like representing different
things with different types, but i'm not sure what do you gain with digests
though.
This I am less flexible on. My thought on how people will use this
library is centered around the instantiation of classes on the keys
used or resulting digests. Anyone wanting ByteString results can
simply use Data.[Serialize,Binary].encode.
Here is a user getting a sha256 hash:
let h = hash contents :: SHA256
or the type could be implicit due to context (not shown):
let h = hash contents
* is strength really useful in the Hash class ? it might be accurate when the
thing get implemented, but i'm not sure what would happens over time, and
flaws
are discovered. would people actually updates it ?
Will people actually update it? I hope so but if they don't are we
really worse off than not having any strength numbers? People who
care about strength will likely keep track of the algorithms on which
they depend. I added strength largely because the Hash class came
from DRBG (NIST SP 800-90) and that needed strength values.
If we don't have strength then applications like DRBG need a way to
know which algorithm each data type represents then to look up that
algorithm their its own table of algorithm strength - very messy. I'd
imaging crypto-api would have to look something like:
\begin{code}
data HashAlgorithm = MD5 | SHA1 | SHA256 | SHA512 | ...
class Hash d c | d - c, c - d where
...
algorithm :: Tagged d HashAlgorithm
...
\end{code}
I don't consider this a win - crypto-api now enumerating all hash
algorithms wanting Hash instances.
The blockCipher should exposes the chaining modes as overridable typeclass
functions, with default generic implementations that use encryptBlocks. For
example the haskell AES package has different C implementations for each
chaining modes (e.g. cbc, ebc), and i suspect that using a generic chaining
implementation would slow things down.
As with hash being part of the hash typeclass, I don't have a strong
objection here. It allows particular implementations to be slightly
higher performance and does not preclude default definitions. This is
rather messier than I wanted, but the reasoning seems sound.
WRT your specific examples:
encryptBlocksCBC :: k - ByteString - (k, ByteString)
decryptBlocksCBC :: k - ByteString - (k, ByteString)
These I do object to. The key does not change as the CBC algorithm
progresses, but contextual information does. My initial mode
implementations have types like:
cbc :: (BlockCipher k) = k - IV k - ByteString - (ByteString, IV k)
In other words, initialization vectors are explicit and separate from
the key. The type parameter on IV allows us to build an IV of proper
size, something like:
buildIV :: (BlockCipher k, MonadRandom m) = m (IV k)
and it is always true that
iv :: IV k
iv - buildIV
B.length (encode iv) == blockSize `for` (undefined :: k)
and my last comment, is that i don't understand the streamcipher interface
you're proposing. I've got a (inefficient) RC4 implementation that has this
interface:
stream :: Ctx - B.ByteString - (Ctx, B.ByteString)
streamlazy :: Ctx - L.ByteString - (Ctx, L.ByteString)
My interface was just a quick hack with me understanding it would
likely change - I didn't know there was a Haskell RC4 binding or
implementation and will happily follow your lead here. Is this
implementation on hackage?
Cheers,
Thomas
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] trees and pointers
Hi cafe! I have a question of C-to-Haskell type:)
Imagine web application wich allows users to browse some shared
filesystem located at the server.
Application stores every users's position within that filesystem
(current directory or file).
In C this can be implemented with the help of following data types:
struct tree_node {
union item {
// some file data
struct file *file;
// struct dir has link to another list of tree_node
struct dir *dir;
};
int type;
// List of tree_nodes
struct tree_node *next;
struct tree_node *prev;
};
struct user {
struct tree_node *position;
// List of users
struct user *next;
struct user *prev;
};
This implementation will give us
1) O(1) time to insert to shared tree
2) O(1) time to access user's current position
Is it possible to reach this requirements in haskell?
For example, managing distinct tree type like
data TreeNode = File | Dir [TreeNode]
will lead to failure of req. 2 (have to traverse this
tree to find each user's position).
Also one could manage several zipper types (one for every user):
data TreeNodeCtx = Top | TreeNodeCtx {
left :: [TreeNode],
right :: [TreeNode],
up :: TreeNodeCtx
}
data TreeNodeZ = TreeNodeZ {
ctx :: [TreeNodeCtx]
pos :: TreeNode
}
It works for one user but not for many because of req. 1 (have to
insert new item into
several zippers).
Any ideas?
--
Thanks,
Sergey
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] trees and pointers
2010/7/14 Sergey Mironov ier...@gmail.com: Hi cafe! I have a question of C-to-Haskell type:) Imagine web application wich allows users to browse some shared filesystem located at the server. Application stores every users's position within that filesystem (current directory or file). In C this can be implemented with the help of following data types: Any ideas? Use IORef. ;) PS MVar is better, actually. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Expression dye
I'm trying to write a function that builds a series of results in a very complicated way. Eventually I ended up writing things like newtype Dye = Dye String deriving (Eq, Show) instance Num Dye where (Dye x) + (Dye y) = Dye (x ++ + ++ y) (Dye x) - (Dye y) = Dye (x ++ - ++ y) (Dye x) * (Dye y) = Dye (x ++ * ++ y) abs (Dye x) = Dye (abs ++ x) and so on. In this way, you can do something like sum [Dye x, Dye y, Dyez] and get 0 + x + y + z as the result. (In reality you probably want to keep track of bracketing and so forth.) In this way, you can take functions that accept any Num instance and feed the dye through them to see what they're actually computing on a given run. Has anybody ever put anything like this on Hackage? I'd prefer to not invent this stuff if somebody has already done it... (The small problem with the approach above, of course, is that as soon as the function wants to do comparisons or take flow control decisions, you've got trouble. It's not impossible to solve, but it *is* a lot of work...) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] trees and pointers
Serguey Zefirov wrote: Use IORef. ;) PS MVar is better, actually TVar is better still. ;-) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] trees and pointers
Or you can get the best of all worlds by combining all three!
data User = User
{userNext :: IORef (MVar (TVar User)))
,userPrev :: IORef (MVar (TVar User)))
}
On 07/14/10 14:39, Andrew Coppin wrote:
Serguey Zefirov wrote:
Use IORef. ;)
PS
MVar is better, actually
TVar is better still. ;-)
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] trees and pointers
You can implement pure pointers on top of Data.Map with O(log n) time:
{-# LANGUAGE ExistentialQuantification #-}
import Data.Map ( Map )
import qualified Data.Map as Map
import Data.Typeable
import Control.Monad.State
import Data.Maybe
type PointerSpace = Map Int PackedValue
newtype Pointer a = Pointer Int
data PackedValue = forall a. Typeable a = PackedValue a
readPointer :: Pointer a - State PointerSpace a
readPointer ( Pointer key ) = do
space - get
return $ fromJust $ cast $ Map.find key space
writePointer :: a - Pointer a - State PointerSpace ()
writePointer a ( Pointer key ) = do
space - get
put $ Map.insert key ( PackedValue a ) space
newPointer :: a - State PointerSpace ( Pointer a )
newPointer a = do
space - get
let key = findEmptyKey space -- implement it yourself
p = Pointer key
writePointer a p
return p
Code can contain some typos.
Sergey Mironov пишет:
Hi cafe! I have a question of C-to-Haskell type:)
Imagine web application wich allows users to browse some shared
filesystem located at the server.
Application stores every users's position within that filesystem
(current directory or file).
In C this can be implemented with the help of following data types:
struct tree_node {
union item {
// some file data
struct file *file;
// struct dir has link to another list of tree_node
struct dir *dir;
};
int type;
// List of tree_nodes
struct tree_node *next;
struct tree_node *prev;
};
struct user {
struct tree_node *position;
// List of users
struct user *next;
struct user *prev;
};
This implementation will give us
1) O(1) time to insert to shared tree
2) O(1) time to access user's current position
Is it possible to reach this requirements in haskell?
For example, managing distinct tree type like
data TreeNode = File | Dir [TreeNode]
will lead to failure of req. 2 (have to traverse this
tree to find each user's position).
Also one could manage several zipper types (one for every user):
data TreeNodeCtx = Top | TreeNodeCtx {
left :: [TreeNode],
right :: [TreeNode],
up :: TreeNodeCtx
}
data TreeNodeZ = TreeNodeZ {
ctx :: [TreeNodeCtx]
pos :: TreeNode
}
It works for one user but not for many because of req. 1 (have to
insert new item into
several zippers).
Any ideas?
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Expression dye
2010/7/14 Andrew Coppin andrewcop...@btinternet.com: I'm trying to write a function that builds a series of results in a very complicated way. Eventually I ended up writing things like newtype Dye = Dye String deriving (Eq, Show) instance Num Dye where (Dye x) + (Dye y) = Dye (x ++ + ++ y) (Dye x) - (Dye y) = Dye (x ++ - ++ y) (Dye x) * (Dye y) = Dye (x ++ * ++ y) abs (Dye x) = Dye (abs ++ x) and so on. In this way, you can do something like sum [Dye x, Dye y, Dyez] and get 0 + x + y + z as the result. (In reality you probably want to keep track of bracketing and so forth.) In this way, you can take functions that accept any Num instance and feed the dye through them to see what they're actually computing on a given run. Has anybody ever put anything like this on Hackage? I'd prefer to not invent this stuff if somebody has already done it... (The small problem with the approach above, of course, is that as soon as the function wants to do comparisons or take flow control decisions, you've got trouble. It's not impossible to solve, but it *is* a lot of work...) Hi, Why not make some kinf of AST and pretty-print it ? Also you can use -XOverloadedStrings to write x + y instead of Dye x + Dye y. If the goal is to see some common expressions as text, I believe there is such a package on Hackage but can't remember its name. Cheers, Thu ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Expression dye
2010/7/14 Vo Minh Thu not...@gmail.com: 2010/7/14 Andrew Coppin andrewcop...@btinternet.com: I'm trying to write a function that builds a series of results in a very complicated way. Eventually I ended up writing things like newtype Dye = Dye String deriving (Eq, Show) instance Num Dye where (Dye x) + (Dye y) = Dye (x ++ + ++ y) (Dye x) - (Dye y) = Dye (x ++ - ++ y) (Dye x) * (Dye y) = Dye (x ++ * ++ y) abs (Dye x) = Dye (abs ++ x) and so on. In this way, you can do something like sum [Dye x, Dye y, Dyez] and get 0 + x + y + z as the result. (In reality you probably want to keep track of bracketing and so forth.) In this way, you can take functions that accept any Num instance and feed the dye through them to see what they're actually computing on a given run. Has anybody ever put anything like this on Hackage? I'd prefer to not invent this stuff if somebody has already done it... (The small problem with the approach above, of course, is that as soon as the function wants to do comparisons or take flow control decisions, you've got trouble. It's not impossible to solve, but it *is* a lot of work...) Hi, Why not make some kinf of AST and pretty-print it ? Also you can use -XOverloadedStrings to write x + y instead of Dye x + Dye y. If the goal is to see some common expressions as text, I believe there is such a package on Hackage but can't remember its name. Oh, maybe not on Hackage, I think what I had in mind was in fact a blog post: http://tom.lokhorst.eu/2009/09/deeply-embedded-dsls Cheers, Thu ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Expression dye
http://hackage.haskell.org/package/simple-reflect This is what is used in lambdabot. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Plotting Vectors with GnuPlot Wrapper
Hi When I use Vectors as a PlotStyle in Graphics.Gnuplot.Simple, the output curve.gp and curve0.csv is not generated correctly. For example when I write in ghci: plotPathStyle [] (PlotStyle Vectors (DefaultStyle 1)) [(1,1),(2,7)] the output files are: curve.gp: plot curve0.csv using 1:2 with vectors linestyle 1 curve0.csv: 1, 1 2, 7 But they must be: curve.gp: plot curve0.csv using 1:2:3:4 with vectors linestyle 1 curve0.csv: 1, 1, 2, 7 Is there any option that should I use to correct this behavior? Regards Mary ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: [Haskell] ANNOUNCE: Haskell 2010 Report (final)
On Wed, Jul 14, 2010 at 10:35:50AM +0100, Simon Marlow wrote: Yeah, I didn't realize how important the allocator was until I started benchmarking, spending time cutting the cost of marking garbage in half didn't help nearly as much as shaving a few cycles off the allocator. The fast pass of the allocator is actually very fast, each object type has its own allocator and free list so allocation is pretty much just pulling an object off of the free list, it is already of the appropriate size and its constant fields are pre-initialized as they arn't cleared during garbage collection. (there is a heuristic that claims full pages back to the general pool sometimes). The slow path has to grab a full page and initialize it, but that isn't really much slower as I can prefetch the cache lines needed so the cost is on the order of another cache line fill. (thinking about computational complexity in terms of O(cache line fills) rather than O(operations) is much more appropriate on todays architectures.). Right, you can see how important locality is by looking at these graphs that Don produced recently: http://haskell.org/haskellwiki/Ghc-gc-tune generational GC these days is important more for locality than for the benefits of avoiding repeated tracing. Yeah, jhc's GC is currently not generational, it is certainly something I want to do, something I have considered as a quick hack was splitting up allocations based on whether they were updatable or not. allocating things that can statically be determined to be in HNF into an older generation and allocating updatable thunks in a younger one. The theory being updatable thunks are more likely to be overwritten by a indirection and become garbage soon, I was thinking this could give me some of the benefits of a generational collector without having to rewrite my GC around being able to promote objects to an older generation. I am not sure if it will work, but it is an idea I have been toying with. Implementing better heap profiling support for jhc generated code is a prerequisite in any case. Speaking of prefetching, we get a lot of benefit in GHC from the automatic prefetching done by modern CPUs; I'm not sure how this would be affected by having multiple allocation regions. Manual prefetching is almost impossible to get right in my experience, see also Nethercote/Mycroft where they did some prefetching experiments with GHC: http://portal.acm.org/citation.cfm?id=773044 Ah, this paper looks very interesting, I was wondering if you had experimented with prefetching just ahead of the allocation pointer. Looks like it helped :) John -- John Meacham - ⑆repetae.net⑆john⑈ - http://notanumber.net/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Docs on the current and future constraint solver?
The latest work is OutsideIn(X): http://www.haskell.org/haskellwiki/Simonpj/Talk:OutsideIn This is quite long paper. It describes a framework for constraint-based type inference and then instantiates it with a constraint solver that supports type families, GADTs and type classes. Constraint-based type inference divides type checking into two phases: constraint-generation and solving. In practice the two may be interleaved for efficiency reasons, of course. As an example (does not type check): type family C a type instance C Int = Int c :: a - C a f :: Int - Bool f = \n - c n In order to type check f we generate the *wanted* constraints (~ denotes equality) (c - C c) ~ (d - e) -- from c - n (d - e) ~ (Int - Bool) -- from type signature From the type family declarations we additionally get the top-level axiom: C Int ~ Int The wanted constraints are now simplified, e.g., c ~ d, C c ~ e -- from the first constraint d ~ Int, e ~ Bool -- from the second constraint c ~ Int, C c ~ Bool, d ~ Int, e ~ Bool-- from the above constraints C Int ~ Bool -- also Now we get an error when combining this with the top-level axiom. If the user specifies type class constraints in the type signature or performs a GADT pattern match we additionally get *given* constraints. The general solver state thus takes the form: G = W where G are the given constraints and W the wanted constraints and = is implication. The solver then reacts two constraints from G, two constraints from W, or one from each, until no more simplifications are possible. To make this efficient, the solver also regularly canonicalises constraints. E.g., function symbols go to the left and constructors to the right. Further performance improvements must come from clever indexing the current state to make the search for applicable rules efficient. This solver is currently being implemented in GHC (there's a branch on darcs.h.o), but correctness comes first. It'll probably take a while until this new solver becomes efficient. The paper does not talk about efficiency, but it lists all the rules and many other details. / Thomas On 14 July 2010 18:39, Corey O'Connor coreyocon...@gmail.com wrote: I believe I have run headlong into issue #3064 in ghc (http://hackage.haskell.org/trac/ghc/ticket/3064). All I think I know is this: * this is a performance issue with the system used to solve type constraints. * the solver is undergoing an overhaul to resolve performance issues in addition to other issues. * An efficient constraint solver is difficult. NP-Complete in the general case? Beyond that I'm at a loss. What can I read to understand the constraint satisfaction problem as it stands in GHC? Is there a paper on the implementation of the current solver? Anything on how the new solver will differ from the current? I think I located one page on the new solver: http://hackage.haskell.org/trac/ghc/wiki/TypeFunctionsSolving Cheers, Corey O'Connor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- If it looks like a duck, and quacks like a duck, we have at least to consider the possibility that we have a small aquatic bird of the family Anatidae on our hands. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] trees and pointers
On 07/14/2010 05:01 PM, Victor Gorokhov wrote: You can implement pure pointers on top of Data.Map with O(log n) time Or on top of Data.IntMap with O(1) time. ;) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
