News aggregator

Dominic Orchard: The Four Rs of Programming Language Design (revisited)

Planet Haskell - Sat, 07/12/2014 - 4:13am

Following my blog post last year about the “four Rs of programming language design” I wrote a short essay expanding upon the idea which has now been included in the online post-proceedings of the ACM Onward ’11 essay track (part of the SPLASH conference).

The essay was a lot of fun to write (I somehow end up referencing books from the 19th century, a sci-fi novel, 1984, and The Matrix!) and is a kind of mission statement (at least for myself) for language design; it is available on my research page here. I hope that it provides some food-for-thought for others interested in, or working in, language design.


Categories: Offsite Blogs

ERDI Gergo: Arrow's place in the Applicative/Monad hierarchy

Planet Haskell - Sat, 07/12/2014 - 3:30am

I've been thinking lately about arrows in relation to applicative functors and monads. The difference between the latter two is easy to intuit (and I'll describe it via an example below), but I never managed to get the same level of understanding about arrows. There's a somewhat famous paper about this question, which has a very clear-cut diagram showing that applicatives embed into arrows and arrows embed into monads (and both containments are non-trivial), which I understood as meaning every arrow is an applicative functor, and every monad is an arrow.

At first glance, this makes sense, given the well-known result that monads are exactly equivalent to arrows that are also instances of ArrowApply, as witnessed by the Haskell types Kleisli and ArrowMonad. However, there's no immediately obvious reason why you couldn't also turn an applicative functor into an arrow, so how does that leave any room for arrows to be different from applicatives? (As an aside, the fact that applicative functors have kind ⋆ → ⋆ and arrows have kind ⋆ → ⋆ → ⋆ has been a huge complication for me in trying to compare them).

Now, finally, based on the helpful replies to that StackOverflow question and the associated Reddit thread, I am confident enough to answer my own question.

Tom Ellis suggested thinking about a concrete example involving file I/O, so let's compare three approaches to it using the three typeclasses. To make things simple, we will only care about two operations: reading a string from a file and writing a string to a file. Files are going to be identified by their file path:

type FilePath = String Monadic I/O

Our first I/O interface is defined as follows:

data IOM ∷ ⋆ → ⋆ instance Monad IOM readFile ∷ FilePath → IOM String writeFile ∷ FilePath → String → IOM ()

Using this interface, we can for example copy a file from one path to another:

copy ∷ FilePath → FilePath → IOM () copy from to = readFile from >>= writeFile to

However, we can do much more than that: the choice of files we manipulate can depend on effects upstream. For example, the below function takes an index file which contains a filename, and copies it to the given target directory:

copyIndirect ∷ FilePath → FilePath → IOM () copyIndirect index target = do from ← readFile index copy from (target ⟨/⟩ to)

On the flip side, this means there is no way to know upfront the set of filenames that are going to be manipulated by a given value action ∷ IOM α. By "upfront", what I mean is the ability to write a pure function fileNames :: IOM α → [FilePath].

Of course, for non-IO-based monads (such as ones for which we have some kind of extractor function μ α → α), this distinction becomes a bit more fuzzy, but it still makes sense to think about trying to extract information without evaluating the effects of the monad (so for example, we could ask "what can we know about a Reader Γ α without having a value of type Γ at hand?").

The reason we can't really do static analysis in this sense on monads is because the function on the right-hand side of a bind is in the space of Haskell functions, and as such, is completely opaque.

So let's try restricting our interface to just an applicative functor.

Applicative I/Odata IOF ∷ ⋆ → ⋆ instance Applicative IOF readFile ∷ FilePath → IOF String writeFile ∷ FilePath → String → IOF ()

Since IOF is not a monad, there's no way to compose readFile and writeFile, so all we can do with this interface is to either read from a file and then postprocess its contents purely, or write to a file; but there's no way to write the contents of a file into another one.

How about changing the type of writeFile?

writeFile′ ∷ FilePath → IOF (String → ())

The main problem with this interface is that while it would allow writing something like

copy ∷ FilePath → FilePath → IOF () copy from to = writeFile′ to ⟨*⟩ readFile from

it leads to all kind of nasty problems because String → () is such a horrible model of writing a string to a file, since it breaks referential transparency. For example, what do you expect the contents of out.txt to be after running this program?

(λ write → [write "foo", write "bar", write "foo"]) ⟨$⟩ writeFile′ "out.txt" Two approaches to arrowized I/O

First of all, let's get two arrow-based I/O interfaces out of the way that don't (in fact, can't) bring anything new to the table: Kleisli IOM and Applicarrow IOF.

The Kleisli-arrow of IOM, modulo currying, is:

readFile ∷ Kleisli IOM FilePath String writeFile ∷ Kleisli IOM (FilePath, String) ()

Since writeFile's input still contains both the filename and the contents, we can still write copyIndirect (using arrow notation for simplicity). Note how the ArrowApply instance of Kleisli IOM is not even used.

copyIndirect ∷ Kleisli IOM (FilePath, FilePath) () copyIndirect = proc (index, target) → do from ← readFile ↢ index s ← readFile ↢ from writeFile ↢ (to, s)

The Applicarrow of IOF would be:

readFile ∷ FilePath → Applicarrow IOF () String writeFile ∷ FilePath → String → Applicarrow IOF () ()

which of course still exhibits the same problem of being unable to compose readFile and writeFile.

A proper arrowized I/O interface

Instead of transforming IOM or IOF into an arrow, what if we start from scratch, and try to create something in between, in terms of where we use Haskell functions and where we make an arrow? Take the following interface:

data IOA ∷ ⋆ → ⋆ → ⋆ instance Arrow IOA readFile ∷ FilePath → IOA () String writeFile ∷ FilePath → IOA String ()

Because writeFile takes the content from the input side of the arrow, we can still implement copy:

copy ∷ FilePath → FilePath → IOA () () copy from to = readFile from >>> writeFile to

However, the other argument of writeFile is a purely functional one, and so it can't depend on the output of e.g. readFile; so copyIndirect can't be implemented with this interface.

If we turn this argument around, this also means that while we can't know in advance what will end up being written to a file (before running the full IOA pipeline itself), but we can statically determine the set of filenames that will be modified.

Conclusion

Monads are opaque to static analysis, and applicative functors are poor at expressing dynamic-time data dependencies. It turns out arrows can provide a sweet spot between the two: by choosing the purely functional and the arrowized inputs carefully, it is possible to create an interface that allows for just the right interplay of dynamic behaviour and amenability to static analysis.

Categories: Offsite Blogs

ERDI Gergo: Arrow's place in the Applicative/Monad hierarchy

Planet Haskell - Sat, 07/12/2014 - 3:30am

I've been thinking lately about arrows in relation to applicative functors and monads. The difference between the latter two is easy to intuit (and I'll describe it via an example below), but I never managed to get the same level of understanding about arrows. There's a somewhat famous paper about this question, which has a very clear-cut diagram showing that applicatives embed into arrows and arrows embed into monads (and both containments are non-trivial), which I understood as meaning every arrow is an applicative functor, and every monad is an arrow.

At first glance, this makes sense, given the well-known result that monads are exactly equivalent to arrows that are also instances of ArrowApply, as witnessed by the Haskell types Kleisli and ArrowMonad. However, there's no immediately obvious reason why you couldn't also turn an applicative functor into an arrow, so how does that leave any room for arrows to be different from applicatives? (As an aside, the fact that applicative functors have kind ⋆ → ⋆ and arrows have kind ⋆ → ⋆ → ⋆ has been a huge complication for me in trying to compare them).

Now, finally, based on the helpful replies to that StackOverflow question and the associated Reddit thread, I am confident enough to answer my own question.

Tom Ellis suggested thinking about a concrete example involving file I/O, so let's compare three approaches to it using the three typeclasses. To make things simple, we will only care about two operations: reading a string from a file and writing a string to a file. Files are going to be identified by their file path:

type FilePath = String Monadic I/O

Our first I/O interface is defined as follows:

data IOM ∷ ⋆ → ⋆ instance Monad IOM readFile ∷ FilePath → IOM String writeFile ∷ FilePath → String → IOM ()

Using this interface, we can for example copy a file from one path to another:

copy ∷ FilePath → FilePath → IOM () copy from to = readFile from >>= writeFile to

However, we can do much more than that: the choice of files we manipulate can depend on effects upstream. For example, the below function takes an index file which contains a filename, and copies it to the given target directory:

copyIndirect ∷ FilePath → FilePath → IOM () copyIndirect index target = do from ← readFile index copy from (target ⟨/⟩ to)

On the flip side, this means there is no way to know upfront the set of filenames that are going to be manipulated by a given value action ∷ IOM α. By "upfront", what I mean is the ability to write a pure function fileNames :: IOM α → [FilePath].

Of course, for non-IO-based monads (such as ones for which we have some kind of extractor function μ α → α), this distinction becomes a bit more fuzzy, but it still makes sense to think about trying to extract information without evaluating the effects of the monad (so for example, we could ask "what can we know about a Reader Γ α without having a value of type Γ at hand?").

The reason we can't really do static analysis in this sense on monads is because the function on the right-hand side of a bind is in the space of Haskell functions, and as such, is completely opaque.

So let's try restricting our interface to just an applicative functor.

Applicative I/Odata IOF ∷ ⋆ → ⋆ instance Applicative IOF readFile ∷ FilePath → IOF String writeFile ∷ FilePath → String → IOF ()

Since IOF is not a monad, there's no way to compose readFile and writeFile, so all we can do with this interface is to either read from a file and then postprocess its contents purely, or write to a file; but there's no way to write the contents of a file into another one.

How about changing the type of writeFile?

writeFile′ ∷ FilePath → IOF (String → ())

The main problem with this interface is that while it would allow writing something like

copy ∷ FilePath → FilePath → IOF () copy from to = writeFile′ to ⟨*⟩ readFile from

it leads to all kind of nasty problems because String → () is such a horrible model of writing a string to a file, since it breaks referential transparency. For example, what do you expect the contents of out.txt to be after running this program?

(λ write → [write "foo", write "bar", write "foo"]) ⟨$⟩ writeFile′ "out.txt" Two approaches to arrowized I/O

First of all, let's get two arrow-based I/O interfaces out of the way that don't (in fact, can't) bring anything new to the table: Kleisli IOM and Applicarrow IOF.

The Kleisli-arrow of IOM, modulo currying, is:

readFile ∷ Kleisli IOM FilePath String writeFile ∷ Kleisli IOM (FilePath, String) ()

Since writeFile's input still contains both the filename and the contents, we can still write copyIndirect (using arrow notation for simplicity). Note how the ArrowApply instance of Kleisli IOM is not even used.

copyIndirect ∷ Kleisli IOM (FilePath, FilePath) () copyIndirect = proc (index, target) → do from ← readFile ↢ index s ← readFile ↢ from writeFile ↢ (to, s)

The Applicarrow of IOF would be:

readFile ∷ FilePath → Applicarrow IOF () String writeFile ∷ FilePath → String → Applicarrow IOF () ()

which of course still exhibits the same problem of being unable to compose readFile and writeFile.

A proper arrowized I/O interface

Instead of transforming IOM or IOF into an arrow, what if we start from scratch, and try to create something in between, in terms of where we use Haskell functions and where we make an arrow? Take the following interface:

data IOA ∷ ⋆ → ⋆ → ⋆ instance Arrow IOA readFile ∷ FilePath → IOA () String writeFile ∷ FilePath → IOA String ()

Because writeFile takes the content from the input side of the arrow, we can still implement copy:

copy ∷ FilePath → FilePath → IOA () () copy from to = readFile from >>= writeFile to

However, the other argument of writeFile is a purely functional one, and so it can't depend on the output of e.g. readFile; so copyIndirect can't be implemented with this interface.

If we turn this argument around, this also means that while we can't know in advance what will end up being written to a file (before running the full IOA pipeline itself), but we can statically determine the set of filenames that will be modified.

Conclusion

Monads are opaque to static analysis, and applicative functors are poor at expressing dynamic-time data dependencies. It turns out arrows can provide a sweet spot between the two: by choosing the purely functional and the arrowized inputs carefully, it is possible to create an interface that allows for just the right interplay of dynamic behaviour and amenability to static analysis.

Categories: Offsite Blogs

regular-xmlpickler

haskell-cafe - Fri, 07/11/2014 - 11:47pm
Hi, I am using a very cool package called regular-xmlpickler. Does anyone know of a way to skip one level of nesting for nested complex fields? So I would like to elide that outer/inner Header. Here is the full code: http://lpaste.net/107362 data User = User { name :: String , admin :: Bool , dt :: UTCTime , header :: Header } data Header = Header { header1 :: String , header2 :: String } so instead of generating <header> twice <header> <header> <header1>abb</header1> <header2>abb</header2> </header> </header> I would like to have it generate this. <header> <header1>abb</header1> <header2>abb</header2> </header> Thanks, Grant _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe< at >haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Categories: Offsite Discussion

[ANNOUNCE] New Core Libraries Committee Members

libraries list - Fri, 07/11/2014 - 11:26pm
I'm pleased to announce that Eric Mertens and Luite Stegeman have joined the core libraries committee. http://www.haskell.org/haskellwiki/Core_Libraries_Committee Brent Yorgey and Doug Beardsley stepped down to make room. I'd like to thank them for helping us get the committee started. In the short term Eric will probably help out with moving the Applicative Monad Proposal forward and with the knock-on effects of that change, and Luite will join Joachim Breitner in trying to figure out the right path forward for the split base proposal. -Edward Kmett _______________________________________________ Libraries mailing list Libraries< at >haskell.org http://www.haskell.org/mailman/listinfo/libraries
Categories: Offsite Discussion

PPDP 2014 Call for Participation

General haskell list - Fri, 07/11/2014 - 11:00pm
====================================================================== CALL FOR PARTICIPATION: PPDP 2014 16th International Symposium on Principles and Practice of Declarative Programming Canterbury, Kent, September 8-10, 2014 http://users-cs.au.dk/danvy/ppdp14/ co-located with LOPSTR 2014 24th International Symposium on Logic-Based Program Synthesis and Transformation Canterbury, Kent, September 9-11, 2014 http://www.iasi.cnr.it/events/lopstr14/ ====================================================================== Registration is now open: http://www.cs.kent.ac.uk/events/2014/ppdp-lopstr-14/ A significant discount is available when registering to both events, especially as a student (until August 8). PPDP 2014 features * an invited talk by Roberto Giacobazzi, shared with LOPSTR: "Obscuring Code -- Unveiling and Veiling Information in Programs" * no fewer than 4 distilled tutorials by - Henrik Nilsson a
Categories: Incoming News

wren gayle romano: #done

Planet Haskell - Fri, 07/11/2014 - 7:54pm

Holy hell, things are bad for everyone.

I've started having PTSD issues again. One of my wife's coworkers got thrown in jail for 24hrs due to a domestic violence accusation (as required by Indiana state law for every accusation with any shred of evidence). Once he got out he filed for divorce because of it, to which his wife shot their son and herself and lit the house on fire— timed at 17 minutes before he was scheduled to (and did) arrive to pick up their son. An online friend of mine was dealing with a family crisis, got dumped by her fiancée, and has been on suicide watch. And now another friend is dealing with a suicide close to her

WTF world? W. T. F?



comments
Categories: Offsite Blogs

What is the state of the art in testing codegeneration?

haskell-cafe - Fri, 07/11/2014 - 6:58pm
I am implementing an EDSL that compiles to SQL and I am wondering what is the state of the art in testing code generation. All the Haskell libraries I could find that deal with SQL generation are tested by implementing multiple one-off adhoc queries and checking that when either compiled to SQL or run against a database they give the expected, prespecified result. * https://github.com/prowdsponsor/esqueleto/blob/master/test/Test.hs * https://github.com/m4dc4p/haskelldb/blob/master/test/TestCases.hs * https://github.com/yesodweb/persistent/blob/master/persistent-test/SumTypeTest.hs I couldn't find any tests for groundhog. * https://github.com/lykahb/groundhog I also had a look at Javascript generators. They take a similar adhoc, one-off approach. * https://github.com/valderman/haste-compiler/tree/master/Tests * https://github.com/faylang/fay/tree/master/tests Is this the best we can do in Haskell? Certainly it seems hard to use a QuickCheck/SmallCheck approach for this purpose. Is there any wa
Categories: Offsite Discussion

Why is "sum" lazy?

Haskell on Reddit - Fri, 07/11/2014 - 5:28pm

I understand why one might want to use foldl in a lazy manner, but if the function passed to foldl is (+), why would anyone object to using foldl'? I work in big data, and I always forget that sum is lazy and I end up getting stack size overflows, tracing all the way back to sum. If it's a teaching function (like some argue foldl is), then can we seriously consider an official, built-in prelude which is more sane? I see that idea mentioned here a lot, but can we make that dream a reality?

submitted by Pugolicious2244
[link] [19 comments]
Categories: Incoming News

Is there any library that deals with the creation of trees with shared branches?

Haskell on Reddit - Fri, 07/11/2014 - 4:07pm

Code explains better than words, so, take a look:

type TreeId = Int leaf :: Int -> TreeId isLeaf :: TreeId -> Boolean leafValue :: TreeId -> Int node :: TreeId -> TreeId -> TreeId isNode :: TreeId -> Boolean nodeLeft :: TreeId -> TreeId nodeRight :: TreeId -> TreeId toTree :: TreeId -> Tree a = node (leaf 1) (leaf 2) b = node (leaf 0) (node (leaf 1) (leaf 2)) main = do print (a == (nodeLeft b)) print (a == b)

Output:

True False

What is going on is the following: node and leaf are constructors for a Tree type. There is a detail, though: before creating the tree, those functions should check, in constant time, if an identical tree already exists. If it doesn't, it creates the Tree, tags it with a unique id and returns that id. If it does, instead of actually allocating more memory, it just returns the id of the existing tree. Notice that a and (left b) are the same value, because they are the same tree. This will guarantee that the heap stays compact, with not a single duplicated branch ever stored.

My questions are:

  1. Is there a name for this?

  2. Are there good-performing libraries available?

submitted by SrPeixinho
[link] [14 comments]
Categories: Incoming News

help with some code

haskell-cafe - Fri, 07/11/2014 - 4:01pm
Hi Cafe, I've got some code where a user can provide a filter to subscribe to a particular type of event. The events come in as xml and are parsed using the toEvent method. The code works fine but is repetitive since each event record potentially has the information needed to parse the xml using the field names and types. So is there a way to get rid of the repetition and streamline the code? Should I be using TH or lenses or something else entirely? Here is the paste. http://lpaste.net/107338 Thanks for any pointers! Grant _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe< at >haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Categories: Offsite Discussion

ANNOUNCE: GHC version 7.8.3

General haskell list - Fri, 07/11/2014 - 2:40pm
============================================================== The (Interactive) Glasgow Haskell Compiler -- version 7.8.3 ============================================================== The GHC Team is pleased to announce a new patchlevel release of GHC, 7.8.3. This is an important bugfix release relative to 7.8.2 (with over 50 defects fixed), so we highly recommend upgrading from the previous 7.8 releases. The full release notes are here: https://www.haskell.org/ghc/docs/7.8.3/html/users_guide/release-7-8-3.html How to get it ~~~~~~~~~~~~~ The easy way is to go to the web page, which should be self-explanatory: https://www.haskell.org/ghc/ We supply binary builds in the native package format for many platforms, and the source distribution is available from the same place. Packages will appear as they are built - if the package for your system isn't available yet, please try again later. Background ~~~~~~~~~~ Haskell is a standard lazy functional programming language. GHC is
Categories: Incoming News

Recovering preconditions from Data.Constraint.(:-)

Haskell on Reddit - Fri, 07/11/2014 - 1:12pm

In the constraints package's Data.Constraint module, the 'a :- b' type expresses a dependency: the Constraint 'b' is entailed by the Constraint 'a'.

e.g.

(Show a, Show b) :- Show (a,b)

Now, for my use case: I am trying to write a Show1 instance for a GADT:

data Fmt r a where Int :: Fmt r Int (:&) :: Fmt r a -> Fmt r b -> Fmt r (a,b) Lift :: r a -> Fmt r a ...

In brief, (Show1 (Fmt r)) would allow me to show any Fmt r a whenever (Show a). However, when I try to write showsPrec1 for the case:

p :& q -> ...

I know from the type of showsPrec1 that there is an instance (Show (b,c)), since I have the original constraint (Show a) for Fmt r a, and in the (:&) case, the type a is refined to (b,c). But, I have been unable to convince the type checker that-- no, really-- there are instances (Show b, Show c), and so I should be able to call showsPrec1 on p and q.

I've turned to the constraints package to help me manage this explicitly, but I haven't figured out how, yet.

How can I recover the constraints (Show b, Show c) in this situation?

I suppose it comes down to being able to write a function:

super :: Dict a -> (b :- a) -> Dict b super Dict = _

Okay, so in the general case, super is impossible. It falls prey to the fallacy of 'P -> Q; Q; therefore P'. I'm not satisfied with that answer, though. In the Show example, we have an instance

instance (Show a, Show b) :=> Show (a,b) where ins = Sub Dict

which models the actual instance

instance (Show a, Show b) => Show (a,b) where showsPrec d (a,b) = ...

Why shouldn't we be able to derive knowledge of the preconditions, given proof of the consequent? Isn't the instance for Show (a,b) actually stating that Show holds for (a,b) iff Show holds for a and for b-- ie. a biconditional, rather than an implication?

submitted by resrvsgate
[link] [7 comments]
Categories: Incoming News

Embedding version info in executables

haskell-cafe - Fri, 07/11/2014 - 10:26am
What are existing solutions for embedding version info (git revision, build date/time, versions of dependencies) in Haskell programs? Roman _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe< at >haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Categories: Offsite Discussion

Edward Z. Yang: Type classes: confluence, coherence and global uniqueness

Planet Haskell - Fri, 07/11/2014 - 10:07am

Today, I'd like to talk about some of the core design principles behind type classes, a wildly successful feature in Haskell. The discussion here is closely motivated by the work we are doing at MSRC to support type classes in Backpack. While I was doing background reading, I was flummoxed to discover widespread misuse of the terms "confluence" and "coherence" with respect to type classes. So in this blog post, I want to settle the distinction, and propose a new term, "global uniqueness of instances" for the property which people have been colloquially referred to as confluence and coherence.

Let's start with the definitions of the two terms. Confluence is a property that comes from term-rewriting: a set of instances is confluent if, no matter what order constraint solving is performed, GHC will terminate with a canonical set of constraints that must be satisfied for any given use of a type class. In other words, confluence says that we won't conclude that a program doesn't type check just because we swapped in a different constraint solving algorithm.

Confluence's closely related twin is coherence (defined in the paper "Type classes: exploring the design space"). This property states that every different valid typing derivation of a program leads to a resulting program that has the same dynamic semantics. Why could differing typing derivations result in different dynamic semantics? The answer is that context reduction, which picks out type class instances, elaborates into concrete choices of dictionaries in the generated code. Confluence is a prerequisite for coherence, since one can hardly talk about the dynamic semantics of a program that doesn't type check.

So, what is it that people often refer to when they compare Scala type classes to Haskell type classes? I am going to refer to this as global uniqueness of instances, defining to say: in a fully compiled program, for any type, there is at most one instance resolution for a given type class. Languages with local type class instances such as Scala generally do not have this property, and this assumption is a very convenient one when building abstractions like sets.

So, what properties does GHC enforce, in practice? In the absence of any type system extensions, GHC's employs a set of rules to ensure that type class resolution is confluent and coherent. Intuitively, it achieves this by having a very simple constraint solving algorithm (generate wanted constraints and solve wanted constraints) and then requiring the set of instances to be nonoverlapping, ensuring there is only ever one way to solve a wanted constraint. Overlap is a more stringent restriction than either confluence or coherence, and via the OverlappingInstances and IncoherentInstances, GHC allows a user to relax this restriction "if they know what they're doing."

Surprisingly, however, GHC does not enforce global uniqueness of instances. Imported instances are not checked for overlap until we attempt to use them for instance resolution. Consider the following program:

-- T.hs data T = T -- A.hs import T instance Eq T where -- B.hs import T instance Eq T where -- C.hs import A import B

When compiled with one-shot compilation, C will not report overlapping instances unless we actually attempt to use the Eq instance in C. This is by design: ensuring that there are no overlapping instances eagerly requires eagerly reading all the interface files a module may depend on.

We might summarize these three properties in the following manner. Culturally, the Haskell community expects global uniqueness of instances to hold: the implicit global database of instances should be confluent and coherent. GHC, however, does not enforce uniqueness of instances: instead, it merely guarantees that the subset of the instance database it uses when it compiles any given module is confluent and coherent. GHC does do some tests when an instance is declared to see if it would result in overlap with visible instances, but the check is by no means perfect; truly, type-class constraint resolution has the final word. One mitigating factor is that in the absence of orphan instances, GHC is guaranteed to eagerly notice when the instance database has overlap (assuming that the instance declaration checks actually worked...)

Clearly, the fact that GHC's lazy behavior is surprising to most Haskellers means that the lazy check is mostly good enough: a user is likely to discover overlapping instances one way or another. However, it is relatively simple to construct example programs which violate global uniqueness of instances in an observable way:

-- A.hs module A where data U = X | Y deriving (Eq, Show) -- B.hs module B where import Data.Set import A instance Ord U where compare X X = EQ compare X Y = LT compare Y X = GT compare Y Y = EQ ins :: U -> Set U -> Set U ins = insert -- C.hs module C where import Data.Set import A instance Ord U where compare X X = EQ compare X Y = GT compare Y X = LT compare Y Y = EQ ins' :: U -> Set U -> Set U ins' = insert -- D.hs module Main where import Data.Set import A import B import C test :: Set U test = ins' X $ ins X $ ins Y $ empty main :: IO () main = print test -- OUTPUT $ ghc -Wall -XSafe -fforce-recomp --make D.hs [1 of 4] Compiling A ( A.hs, A.o ) [2 of 4] Compiling B ( B.hs, B.o ) B.hs:5:10: Warning: Orphan instance: instance [safe] Ord U [3 of 4] Compiling C ( C.hs, C.o ) C.hs:5:10: Warning: Orphan instance: instance [safe] Ord U [4 of 4] Compiling Main ( D.hs, D.o ) Linking D ... $ ./D fromList [X,Y,X]

Locally, all type class resolution was coherent: in the subset of instances each module had visible, type class resolution could be done unambiguously. Furthermore, the types of ins and ins' discharge type class resolution, so that in D when the database is now overlapping, no resolution occurs, so the error is never found.

It is easy to dismiss this example as an implementation wart in GHC, and continue pretending that global uniqueness of instances holds. However, the problem with global uniqueness of instances is that they are inherently nonmodular: you might find yourself unable to compose two components because they accidentally defined the same type class instance, even though these instances are plumbed deep in the implementation details of the components. This is a big problem for Backpack, or really any module system, whose mantra of separate modular development seeks to guarantee that linking will succeed if the library writer and the application writer develop to a common signature.

Categories: Offsite Blogs