- Haskell-Cafe - Haskell.org

Space not reclaimed by GC
by Neil Mitchell 18 Nov '10

18 Nov '10

Hi, I have a program which runs, then calls performGC multiple times. I'd expect all (or nearly all) of the memory to be freed by that point. But it isn't. Given this program: import Language.Haskell.Exts.Annotated -- from haskell-src-exts import System.Mem main :: IO () main = do let src = fromParseResult $ parseFileContents $ "data C = C {a :: F {- " ++ replicate 400000 'd' ++ " -} }" putStrLn $ "Total length is: " ++ show (length $ show $ src) performGC performGC performGC I run with: ghc --make Temp.hs -rtsopts && Temp.exe +RTS -G1 -S (the use of 1 generation is to make sure all GC's clear up everything, the leak still happens without it). I am using GHC 7.0.1 I get the output: Alloc Copied Live GC GC TOT TOT Page Flts bytes bytes bytes user elap user elap ... lots of values ... 16187336 9598808 9600428 0.05 0.06 0.47 0.66 0 0 (Gen: 0) 19513288 11571104 11572724 0.06 0.07 0.55 0.77 0 0 (Gen: 0) 23519176 13948292 13949912 0.09 0.08 0.67 0.89 0 0 (Gen: 0) Total length is: 4226 24645752 548 2091128 0.00 0.00 0.75 0.98 0 0 (Gen: 0) 20 540 2091120 0.00 0.00 0.75 0.99 0 0 (Gen: 0) 0 540 2091120 0.00 0.00 0.75 1.00 0 0 (Gen: 0) 1288 844 3028 0.00 0.00 0.75 1.01 0 0 (Gen: 0) 0 0.00 0.00 162,592,312 bytes allocated in the heap 81,004,756 bytes copied during GC 13,949,912 bytes maximum residency (30 sample(s)) 226,344 bytes maximum slop 63 MB total memory in use (6 MB lost due to fragmentation) Generation 0: 30 collections, 0 parallel, 0.48s, 0.51s elapsed INIT time 0.02s ( 0.02s elapsed) MUT time 0.25s ( 0.47s elapsed) GC time 0.48s ( 0.51s elapsed) EXIT time 0.00s ( 0.00s elapsed) Total time 0.75s ( 1.01s elapsed) %GC time 64.6% (50.6% elapsed) Alloc rate 613,093,182 bytes per MUT second Productivity 33.3% of total user, 24.7% of total elapsed QUESTION 1: My reading of this report is that performGC leaves 2091120 of live data. However, the program seems to run a GC on termination, when only 3028 bytes of data are left. Why is all the data not released on performGC? QUESTION 2: It seems that the haskell-src-exts parser has some kind of space leak in "data C = C {a :: F {- ddddd -} }", but not in "data C = C {a :: F} {- ddddd -}". That's fair enough, but is it because it's a space leak that performGC doesn't get the data? If I change to the second form then the in use memory after performGC is about 3Kb. I found that if I did the parseFileContents/print bit once I get 2Mb of leak, if I do it twice I get 2Mb, and if I do it three times I get 1Mb of leak, which really confused me. Thanks, Neil

1 0

[ANNOUNCE] A Haskell interface to Lego Mindstorms NXT
by Mitar 18 Nov '10

18 Nov '10

Hi! I have just published my library which provides Haskell interface to Lego Mindstorms NXT over Bluetooth. http://hackage.haskell.org/package/NXT So take your NXTs out of your closets or out of your children hands and try it out! ;-) Feel free to contribute additional features, interfaces for more sensors and propose or write other (example) programs. I also more than welcome any comments as it is my first library in Haskell. So if you have any suggestion about code improvements or some other best practices, I would really like to hear them. Currently haddock documentation does not compile because of this bug: http://hackage.haskell.org/trac/hackage/ticket/656 Can anybody help with fixing this bug? It would be much nicer to see all documentation on HackageDB I made. Mitar

1 0

Papers discussing interpreters for call by need?
by oleg＠okmij.org 18 Nov '10

18 Nov '10

David Sankel wrote: > I'm writing an interpreter for a call by need language... Is anyone > aware of any papers out there that go into detail on the construction > of an actual interpreter? You might find the following call-by-need interpreter useful: http://okmij.org/ftp/tagless-final/tagless-typed.html#call-by-any http://okmij.org/ftp/tagless-final/course/CBAny.hs (the files also implement interpreters for the other two popular strategies). The key to call-by-need is the `share' function, whose more complex instance is described in the paper mentioned here yesterday: http://okmij.org/ftp/Computation/monads.html#lazy-sharing-nondet

1 0

Haskell Weekly News: Issue 159 - November 17, 2010
by Daniel Santa Cruz 18 Nov '10

18 Nov '10

Welcome to issue 159 of the HWN, a newsletter covering developments in the [1]Haskell community in the week of November 07 - 13. We have a new GHC to celebrate! On November 16 the GHC team announced the [2]release of GHC 7.0.1. Plenty of goodness here, with many bug fixes and numerous performance improvements over the previous 6.12 branch. The good folks at GHC remind us that most users should countinue to use the Haskell Platform. This "release is aimed primarily at package maintainers and early adopters." Many kudos to the team! Curious about the most active members of the #haskell IRC channel? Out of around 28K "utterances" in the channel this week, 24% of them where spoken by the top 5 most active members. Not suprisingly, the dear lambdabot is at the top of the list. lambdabot 2094 kmc 1263 jmcarthur 1221 Eduard_Munteanu 1142 EvanR-work 1007 This week we had 299 messages posted to Haskell-Cafe (down 79 from last week), 26 stories posted to Reddit (4 less than last week), 36 questions posted to StackOverflow (4 less than last week), and 135 updates to Hackage (39 more than last week). Fun to see the different package maintainers upgrading their packages to the new GHC. Announcements Simon Meier uploaded [3]blaze-builder, a library which provides an abstraction of buffered output of byte streams and several convenience functions to exploit it. He notes that blaze-builder was inspired by the Data.Binary.Builder module. David Peixotto introduced the [4]Fibon benchmark tools and suite for running and analyzing programs. It includes an optional set of benchmark programs, including many taken from Hackage. Tom Lokhorst uploaded [5]language-cil, a library for manipulating Common Intermediate Language, the lowest level language used by Microsoft .NET and Mono. Janis Voigtländer announced that the [6]Haskell Communities and Activities Report is now available in both PDF and HTML format. Check it out and see what others in the community are doing. The list of contributors should be enough to convince you to read it! Top Reddit Stories * Manatee - a Haskell integrated environment written in Haskell Domain: hackage.haskell.org, Score: 34, Comments: 11 On Reddit: http://www.reddit.com/r/haskell/comments/e43y6/manatee_a_haskell_integrated… Original: http://hackage.haskell.org/package/manatee * A Neighborhood of Infinity: Statistical Fingertrees Domain: blog.sigfpe.com, Score: 31, Comments: 4 On Reddit: http://www.reddit.com/r/haskell/comments/e3iph/a_neighborhood_of_infinity_s… Original: http://blog.sigfpe.com/2010/11/statistical-fingertrees.html * November 2010 edition of the Haskell Communities and Activities Report Domain: haskell.org, Score: 28, Comments: 3 On Reddit: http://www.reddit.com/r/haskell/comments/e3dps/november_2010_edition_of_the… Original: http://haskell.org/communities/11-2010/html/report.html * Please Break Yesod Domain: docs.yesodweb.com, Score: 28, Comments: 0 On Reddit: http://www.reddit.com/r/haskell/comments/e4qfk/please_break_yesod/ Original: http://docs.yesodweb.com/blog/please-break-yesod/ * "Atomo - The programmer's programmable programming language" -- written in Haskell Domain: atomo-lang.org, Score: 28, Comments: 10 On Reddit: http://www.reddit.com/r/haskell/comments/e5m3i/atomo_the_programmers_progra… Original: http://atomo-lang.org/ * Language.Cil Domain: hackage.haskell.org, Score: 27, Comments: 11 On Reddit: http://www.reddit.com/r/haskell/comments/e2fwm/languagecil/ Original: http://hackage.haskell.org/package/language-cil * Defragmenting lazy bytestrings for better performance Domain: lambda-view.blogspot.com, Score: 25, Comments: 0 On Reddit: http://www.reddit.com/r/haskell/comments/e4cbg/defragmenting_lazy_bytestrin… Original: http://lambda-view.blogspot.com/2010/11/defragmenting-lazy-bytestrings.html * "We are looking for someone who has experience in porting **from** Haskell to java" Domain: haskell.org, Score: 22, Comments: 33 On Reddit: http://www.reddit.com/r/haskell/comments/e4km8/we_are_looking_for_someone_w… Original: http://www.haskell.org/pipermail/haskell-cafe/2010-November/086228.html * Zeno: Automatically Prove Haskell Program Properties Domain: doc.ic.ac.uk, Score: 21, Comments: 5 On Reddit: http://www.reddit.com/r/haskell/comments/e5ph3/zeno_automatically_prove_has… Original: http://www.doc.ic.ac.uk/~ws506/tryzeno/ * Tips on a Computer Algebra System in Haskell? Domain: self.haskell, Score: 20, Comments: 17 On Reddit: http://www.reddit.com/r/haskell/comments/e348f/tips_on_a_computer_algebra_s… Original: http://www.reddit.com/r/haskell/comments/e348f/tips_on_a_computer_algebra_s… Top StackOverflow Questions * Is performance of partial or curried functions well defined in Haskell? votes: 13, answers: 4 http://stackoverflow.com/questions/4166924/is-performance-of-partial-or-cur… * What Self Balancing Tree is simplest in Functional Programming? votes: 11, answers: 3 http://stackoverflow.com/questions/4166027/what-self-balancing-tree-is-simp… * Attoparsec allocates a ton of memory on large 'take' call. votes: 7, answers: 0 http://stackoverflow.com/questions/4151265/attoparsec-allocates-a-ton-of-me… * Emacs Haskell indentation votes: 7, answers: 1 http://stackoverflow.com/questions/4169962/emacs-haskell-indentation * What is the difference between Pattern Matching and Guards? votes: 5, answers: 4 http://stackoverflow.com/questions/4156727/what-is-the-difference-between-p… * Impact on style of GHC -Wall votes: 5, answers: 4 http://stackoverflow.com/questions/4174629/impact-on-style-of-ghc-wall * Cartesian product votes: 4, answers: 9 http://stackoverflow.com/questions/4119730/cartesian-product * What's wrong with my type signatures here? votes: 4, answers: 1 http://stackoverflow.com/questions/4125692/whats-wrong-with-my-type-signatu… * combining StateT and State votes: 4, answers: 2 http://stackoverflow.com/questions/4138671/combining-statet-and-state * Useful projects in Haskell votes: 4, answers: 2 http://stackoverflow.com/questions/4167864/useful-projects-in-haskell Quotes of the week * hpc: (<$>) = fmap; (<*>) = magic * medfly: it's awesome not to be an expert here. you ask questions that you think are difficult and they are so easy to others that they are all excited to explain it to you. * EvanR: think of [grant applications] as the interface to the real world, like the IO monad * ray: every paul graham essay contains an ad-hoc, informally specified implementation of a good idea About the Haskell Weekly News New editions are posted to [7]the Haskell mailing list as well as to [8]the Haskell Sequence and [9]Planet Haskell. [10]RSS is also available, and headlines appear on [11]haskell.org. To help create new editions of this newsletter, please send stories to dstcruz * at * gmail * dot * com. The code used to produce this version of the newsletter is not yet publicly available, as it is a complete hack designed to get things started again. Until next time, Daniel Santa Cruz References 1. http://haskell.org/ 2. http://new-www.haskell.org/ghc/docs/7.0.1/html/users_guide/release-7-0-1.ht… 3. http://article.gmane.org/gmane.comp.lang.haskell.general/18283 4. http://article.gmane.org/gmane.comp.lang.haskell.general/18288 5. http://groups.google.com/group/haskell-cafe/browse_thread/thread/9f73730058… 6. http://groups.google.com/group/haskell-cafe/browse_thread/thread/860f3a2e9c… 7. http://www.haskell.org/mailman/listinfo/haskell 8. http://sequence.complete.org/ 9. http://planet.haskell.org/ 10. http://sequence.complete.org/node/feed 11. http://haskell.org/

2 1

Papers discussing interpreters for call by need?
by David Sankel 17 Nov '10

17 Nov '10

I'm writing an interpreter for a call by need language and have been doing a direct implementation of the Launchbury semantics. My problem is that in the variable rule, an alpha conversion is done that, as far as I understand, is going to hinder any tail call optimization. I realize that the intent of Launchbury's paper is to come up with a theoretical framework for call by need, not to guide an implementation per say. Is anyone aware of any papers out there that go into detail on the construction of an actual interpreter? TIA, David -- David Sankel Sankel Software www.sankelsoftware.com 585 617 4748 (Office)

2 2

[ANNOUNCE] Parallel Haskell project underway
by Dmitry Astapov 17 Nov '10

17 Nov '10

Parallel Haskell project underway GHC HQ and Well-Typed are pleased to report that work has started on the MSR-funded project to push the real-world use of parallel Haskell. We will be working with four industrial partners over the next two years, with the aim of demonstrating that parallel Haskell can be employed successfully in industrial projects. The participating organizations are: * Dragonfly (New Zealand) * IIJ Innovation Institute Inc. (Japan) * Los Alamos National Laboratory (USA) * Willow Garage Inc. (USA) Each group is working on their own project, applying parallel Haskell and their domain-specific expertise. In addition to providing advice on Haskell tools and techniques, we will work with these partners to identify and resolve any issues that are hindering progress. We are prepared to handle issues covering anything from the compiler and runtime system, through to platform, tool and library problems. All the participants are working on complex, real-world problems. Three projects involve scientific problems, and the fourth involves network servers. Three of the projects are targeting single-node SMP systems, while the fourth is targeting clusters. In two cases, Haskell will be directly pitted against existing code written in C or C++. Project progress reports will be posted to the Well-Typed blog [1] and to the new Parallel Haskell mailing list [2]. [1]: http://www.well-typed.com/blog/ [2]: http://groups.google.com/group/parallel-haskell == Dragonfly == http://www.dragonfly.co.nz/ Participants: Finlay Thompson, Edward Abraham Cloudy Bayes: Hierarchical Bayesian modeling in Haskell The Cloudy Bayes project aims to develop a fast Bayesian model fitter that takes advantage of modern multiprocessor machines. It will support model descriptions in the BUGS model description language (WinBUGS, OpenBUGS, and JAGS). It will be implemented as an embedded domain specific language (EDSL) within Haskell. A wide range of model hierarchical Bayesian model structures will be possible, including many of the models used in medical, ecological, and biological sciences. Cloudy Bayes will provide an easy to use interface for describing models, running Monte Carlo Markov chain (MCMC) fitters, diagnosing performance and convergence criteria as it runs, and collecting output for post-processing. Haskell's strong type system will be used to ensure that model descriptions make sense, providing a fast, safe development cycle. == IIJ Innovation Institute Inc. == http://www.iij-ii.co.jp/en/ Participants: Kazu Yamamoto Haskell is suitable for many kinds of domain, and GHC's support for lightweight threads makes it attractive for concurrency applications. An exception has been network server programming because GHC 6.12 and earlier have an IO manager that is limited to 1024 network sockets. The upcoming GHC 7 has a new IO manager implementation that gets rid of this limitation. This project will implement several network servers to demonstrate that Haskell is suitable for network servers that handle a massive number of concurrent connections. == Los Alamos National Laboratory == http://www.lanl.gov/ Participants: Michael Buksas, Timothy M. Kelley This project will use parallel Haskell to implement high-performance Monte Carlo algorithms, a class of algorithms which use randomness to sample large or otherwise intractable solution spaces. The initial goal is a particle-based MC algorithm suitable for modeling the flow of radiation, with application to problems in astrophysics. From this, the project is expected to move to identification of suitable abstractions for expressing a wider variety of Monte Carlo algorithms, and using models for different physical phenomena. == Willow Garage == http://www.willowgarage.com/ Participants: Ryan Grant Distributed Rigid Body Dynamics in ROS Willow Garage seeks a high-level representation for a distributed rigid body dynamics simulation, capable of excellent parallel speedup on current and foreseeable hardware, yet linking to existing optimized libraries for low-level message passing and matrix math. This project will drive API, performance, and profiling tool requirements for Haskell's interface to the Message Passing Interface (MPI) specification, an industry-standard in High Performance Computing (HPC), as used on clusters of many nodes. Competing internal initiatives use C++/MPI and CUDA directly. Willow Garage aims to lay the groundwork for personal robotics applications in everyday life. ROS (Robot Operating System - ROS.org) is an open source, meta-operating system for your robot. -- Dmitry Astapov Well-Typed LLP, http://www.well-typed.com/

2 2

Re: Making monadic code more concise
by oleg＠okmij.org 17 Nov '10

17 Nov '10

Ling Yang wrote > I think a good question as a starting point is whether it's possible > to do this 'monadic instance transformation' for any typeclass, and > whether or not we were lucky to have been able to instance Num so > easily (as Num, Fractional can just be seen as algebras over some base > type plus a coercion function, making them unusually easy to lift if > most typeclasses actually don't fit this description). > > In general, what this seems to be is a transformation on functions > that also depends explicitly on type signatures. For example in Num: Things start to break down when we get to the higher order. In the first order, it is indeed easy to see that the monadification of the term Int -> Int -> Int should/could be m Int -> m Int -> m Int Indeed, liftM2 realizes this transformation. But what about (Int -> Int) -> Int ? Should it be (m Int -> m Int) -> m Int ? A moment of thought shows that there is no total function of the type Monad m => ((Int -> Int) -> Int) -> ((m Int -> m Int) -> m Int) because there is no way, in general, to get from (m Int -> m Int) to the pure function Int->Int. That is, we can't write Monad m => (m Int -> m Int) -> m (Int->Int) One may try tabulation (for finite domains) tf f = do vt <- f (return True) vf <- f (return False) return $ \x -> if x then vt else vf but that doesn't quite work: what if the resulting function is never invoked on the True argument. We have needlessly computed that value, vt. Worse, we have incurred the effect of computing vt; that effect could be failure. We have needlessly failed. One can say: we need runnable > class (Monad m) => Runnable m where > exit : m a -> a are there many monads that are members of that typeclass? For example, Maybe cannot be Runnable; otherwise, what is (exit Nothing)? Any Error or MonadPlus monad can't be Runnable.

3 4

Re: ANNOUNCE zeno 0.1.0
by Petr Pudlak 17 Nov '10

17 Nov '10

Hi Will, I was wondering, Zeno capable of proving just equational statements, or is it able to prove more general statements about programs? In particular, it would be interesting if Zeno would be able to prove that a function is total by verifying that it uses only structural (inductive) recursion (on a well defined inductive type), i.e. each recursive function call must be on a syntactic subcomponent of its parameter. And dually, one might want to prove that a function is corecursive, meaning that each recursive call is guarded by a constructor. Best regards, Petr > Hi all, > > My masters project Zeno was recently mentioned on this mailing list so > I thought I'd announce that I've just finished a major update to it, > bringing it slightly closer to being something useful. Zeno is a fully > automated inductive theorem proving tool for Haskell programs. You can > express a property such as "takeWhile p xs ++ dropWhile p xs === xs" > and it will prove it to be true for all values of p :: a -> Bool and > xs :: [a], over all types a, using only the function definitions. > > Now that it's updated it can use polymorphic types/functions, and you > express properties in Haskell itself (thanks to SPJ for the > suggestion). It still can't use all of Haskell's syntax: you can't > have internal functions (let/where can only assign values), and you > can't use type-classed polymorphic variables in function definitions - > you'll have to create a monomorphic instance of the function -but I > hope to have these added reasonably soon. It's also still missing > primitive-types/IO/imports so it still can't be used with any > real-world Haskell code, it's more a bit of theorem proving "fun". > > You can try it out at http://www.doc.ic.ac.uk/~ws506/tryzeno, the code > file given there has some provable properties about a few prelude > functions among other things. > > Another feature is that it lists all the sub-properties it has proven > within each proof. When it verifies insertion-sort "sorted (insertsort > xs) === True" it also proves the antisymmetry of "<=" and that the > "insert" function preserves the "sorted" property. > > Any suggestions or feedback would be greatly appreciated. > > Cheers, > > Will

5 7

typeclass namespace rational?
by Jonathan Geddes 16 Nov '10

16 Nov '10

cafe, Data Constructors and Type Constructors don't share the same namespace. You see code like the following all the time: > data MyRecord = MyRecord {...} This is possible because Data Constructors are used in different parts of the code than Type Constructors so there's never any ambiguity. Type Classes, on the other hand, share the same namespace as Type Constructors. You can't define this: >class String s where > ... > >instance String String where > ... >instance String ByteString where > ... >instance String Text where > ... Not that I'm running out of valid haskell identifiers or anything :P, I'm just wondering: what's the rationale behind keeping Type Classes and Type Constructors in the same namespace? I can't think of any ambiguity there would be if they each had their own namespace. And In some cases it would be convenient to be able to define both a concrete representation and an abstract one with the same name as in the String class example above. --Jonathan

3 3

Re: [Haskell] intent-typing
by Tillmann Rendel 16 Nov '10

16 Nov '10

Hi, Marcus Sundman wrote: > Hi, how would one go about implementing (or using if it's supported > out-of-the-box) intent-typing* for haskell? A basic technique is to use newtype declarations to declare separate types for separate intents. module StringSafety ( SafeString () , UnsafeString () , quote , considerUnsafe ) where newtype SafeString = SafeString String newtype UnsafeString = UnsafeString String considerUnsafe :: String -> UnsafeString considerUnsafe s = UnsafeString s quote :: UnsafeString -> SafeString quote (UnsafeString s) = SafeString s' where s' = ... s ... This module does not export the SafeString and UnsafeString constructors, so we can be sure that no other code in the program can invent SafeStrings which are not really safe. Every string can be safely treated as unsafe, however, so we export a function considerUnsafe which does so. Now, if we type our interface to the outside world as getInput :: ... -> UnsafeString sendOutput :: SafeString -> ... we can be sure that a return value from getInput needs to pass through quote on its way to sendOutput, because quote is the only way to produce a SafeString. This guarantuees safety. It has, however, a practical problem: We can't use the usual String functions on UnsafeString or SafeString values. For instance, we can't concatenate two UnsafeStrings using (++). A naive solution would be to provide separate (++) functions for unsafe and safe strings: append_safe :: SafeString -> SafeString -> SafeString append_safe (SafeString x) (SafeString y) = SafeString (x ++ y) append_unsafe :: SafeString -> SafeString -> SafeString append_unsafe (UnsafeString x) (UnsafeString y) = UnsafeString (x ++ y) Note that at least append_safe needs to be implemented in and exported from the StringSafety module. That is a good thing, because this function needs to be carefully checked for safety. The programmer needs to prove (or unit-test, or at least think about) the following theorem: If a and b are safe strings, so is a ++ b. After this fact has been established, other modules are free to use append_safe however they like without possibly compromising safety. Now, the above approach should work, but is still rather impractical: We need to copy the definitions of all String functions for unsafe and safe strings. However, since the bodies of all these copies are actually identical, so we can use parametric polymorphism to abstract over the difference between UnsafeString and SafeString. One way to achieve this is to use phantom types. With phantom types, we declare only a single newtype for both safe and unsafe strings, but we annotate that type with an additional flag to distinguish safe from unsafe uses. module StringSafety ( AnnotatedString () , Safe () , Unsafe () , quote , considerUnsafe , append ) where data Safe = Safe data Unsafe = Unsafe newtype AnnotatedString safety = AnnotatedString String considerUnsafe :: String -> AnnotatedString Unsafe considerUnsafe s = AnnotatedString s quote :: AnnotatedString Unsafe -> AnnotatedString Safe quote (AnnotatedString s) = AnnotatedString s' where s' = ... s ... append :: AnnotatedString a -> AnnotatedString a -> AnnotatedString a append (AnnotatedString x) (AnnotatedString y) = AnnotatedString (x ++ y) Note that AnnotatedString does not really use its type parameter safety: That's why it is called a phantom type. The data constructor AnnotatedString can be freely used to convert between safe and unsafe strings, so we better not export it from the module. Inside the module, uses of the data constructor gives rise to proof obligations as above. So the programmer needs to reason that the following is true to justify the implementation and export of append: If x and y have the same safety level, then (x ++ y) has again that same safety level. So now, we still have to write a wrapper around each string operation, but at least we need to write only one such wrapper for all intents, not a separate wrapper for each intent. There is an inconvenience left: We can't concatenate safe and unsafe strings, because both arguments to append need to have exactly the same type. To fix this, we first have to figure out what the result of sucha concatenation would be: It would be an unsafe string, because at least one of the inputs is unsafe. We need to teach this kind of reasoning to the compiler, for instance, using type families: type family Join a b type instance Join Safe Safe = Safe type instance Join Safe Unsafe = Unsafe type instance Join Unsafe Safe = Unsafe type instance Join Unsafe Unsafe = Unsafe The idea is that (Join a b) is the safety level of the result of an operation which consumes data of safety level a and b. I called the type family Join because the safety levels form a lattice, with unsafe levels higher then safe levels, and the type family computes the join operation for that lattice. So we are encoding a simple static analysis into the type system here! Using this lattice structure of safety level, we can give a more polymorphic type to append: append :: AnnotatedString a -> AnnotatedString b -> AnnotatedString (Join a b) The implementation can remain unchanged. Now, the programmer needs to reason that the following statement is true to justify this type of append: (x ++ y) is at least as safe as the least safe of x and y. So to conclude, statically checked intent-typing can be expressed in Haskell using newtype wrappers with phantom types, and possibly some type-level computation on these phantom types to teach the compiler domain knowledge about the intents. Tillmann PS. Crossposted to the haskell cafe, please consider dropping haskell(a)haskell.org when answering.

3 2