News aggregator

Bryan O'Sullivan: Once more into the teach, dear friends

Planet Haskell - Tue, 05/13/2014 - 11:18pm

Since the beginning of April, David Mazières and I have been back in the saddle teaching CS240H at Stanford again.

If you’re tuning in recently, David and I both love systems programming, and we particularly get a kick out of doing it in Haskell. Let me state this more plainly: Haskell is an excellent systems programming language.

Our aim with this class is to teach both enough advanced Haskell that students really get a feel for how different it is from other programming languages, and to apply this leverage to the kinds of problems that people typically think of as “systemsy”: How do I write solid concurrent software? How do I design it cleanly? What do I do to make it fast? How do I talk to other stuff, like databases and web servers?

As before, we’re making our lecture notes freely available. In my case, the notes are complete rewrites compared to the 2011 notes.

I had a few reasons for rewriting everything. I have changed the way I teach: every class has at least some amount of interactivity, including in-class assignments to give students a chance to absorb what I’m throwing at them. Compared to the first time around, I’ve dialed back the sheer volume of information in each lecture, to make the pace less overwhelming. Everything is simply fresher in my mind if I write the material right before I deliver it.

And finally, sometimes I can throw away plans at the last minute. On the syllabus for today, I was supposed to rehash an old talk about folds and parallel programming, but I found myself unable to get motivated by either subject at 8pm last night, once I’d gotten the kids to bed and settled down to start on the lecture notes. So I hemmed and hawed for a few minutes, decided that talking about lenses was way more important, and went with that.

Some of my favourite parts of the teaching experience are the most humbling. I hold office hours every week; this always feels like a place where I have to bring my “A” game, because there’s no longer a script. Some student will wander in with a problem where I have no idea what the answer is, but I vaguely remember reading a paper four years ago that covered it, so when I’m lucky I get to play glorified librarian and point people at really fun research.

I do get asked why we don’t do this as a MOOC.

It is frankly a pleasure to actually engage with a room full of bright, motivated people, and to try to find ways to help them and encourage them. I don’t know quite how I’d replicate that visceral feedback with an anonymous audience, but it qualitatively matters to me.

And to be honest, I’ve been skeptical of the MOOC phenomenon, because while the hype around them was huge, it’s always been clear that almost nobody knew what they were doing, or what it would even mean for that model to be successful. If the MOOC world converges on a few models that make some sense and don’t take a vast effort to do well, I’m sure we’ll revisit the possibility.

Until then, enjoy the slides, and happy hacking!

Categories: Offsite Blogs

CS240h lecture notes

Haskell on Reddit - Tue, 05/13/2014 - 8:53pm
Categories: Incoming News

Why isn't halvm getting more attention in haskell land?

Haskell on Reddit - Tue, 05/13/2014 - 8:16pm

Over in the ocaml world (and even outside of it) mirage gets a fair bit of attention and use. Halvm is the same deal for haskell, but it doesn't seem like anyone uses it or talks about it. So, how come? Lack of awareness? Not easy enough to use? Are there some limitations or problems with it? Or is it just a general lack of interest?

submitted by haskellnoob
[link] [26 comments]
Categories: Incoming News

How to teach a kid what "a program" is? Any success stories?

Haskell on Reddit - Tue, 05/13/2014 - 7:37pm

I' been taught (when was 13) that a program is serie of steps. It was easy to start coding, knowing all your writeln and readln where executed in order you specified (unless ifs where used).

But what about functional programming and Haskell in particular? Seems like children don't like monads, functors and abstractions, they like writeln. It is easy to experiment in Pascal, knowing a little, is that true for Haskell?

submitted by danbst
[link] [46 comments]
Categories: Incoming News

AlternateLayoutRule

glasgow-user - Tue, 05/13/2014 - 3:04pm
Hi, I noticed that ghc now supports an 'AlternateLayoutRule' but am having trouble finding information about it. Is it based on my proposal and sample implementation? http://www.mail-archive.com/haskell-prime< at >haskell.org/msg01938.html https://ghc.haskell.org/trac/haskell-prime/wiki/AlternativeLayoutRule implies it has been in use since 6.13. If that is the case, I assume it has been found stable? I ask because I was going to rewrite the jhc lexer and would like to use the new mechanism in a way that is compatible with ghc. If it is already using my code, so much the better. John
Categories: Offsite Discussion

ANNOUNCE: graphviz-2999.17.0.0

haskell-cafe - Tue, 05/13/2014 - 2:18pm
It's taken me over a year, but I'm pleased to announce the latest version of my graph visualisation (via the Graphviz suite of tools) library: http://hackage.haskell.org/package/graphviz You can read all the changes in the Changelog (now linked to from the Hackage page, thanks to the magic of Hackage 2.0! :o), but here are some explicit non-API changes that people should probably be made aware of: * Parsing is currently about 8x slower than previously... because I suggested something two years ago to Malcolm Wallace on what seemed to make polyparse faster; he then released that change as part of polyparse-1.9 a year ago, but now when I do proper benchmarks (rather than the extremely limited ones I did then) I find that my changes actually make it _slower_ in real world usage. Whoops! I'm still using polyparse-1.9 in the hopes that Malcolm is able to release a point-fix release to revert my suggestion. * I'm not sure when it happened, but upstream Graphviz seems to have changed the behaviour of `dot -Tca
Categories: Offsite Discussion

FLOPS 2014 call for participation (early registration deadline extended)

haskell-cafe - Tue, 05/13/2014 - 11:39am
Dear colleagues, The early registration for FLOPS 2014 (Twelfth International Symposium on Functional and Logic Programming, June 4-6, Kanazawa, Japan) is now open until May 16 Friday, 23:59 JST. - Please register *now* (that is, if you plan to attend) at: http://www.jaist.ac.jp/flops2014/registration.html - Program: http://www.jaist.ac.jp/flops2014/program.html - Invited talks by Ranjit Jhala, Shin-ya Katsumata, and Gabriele Keller: http://www.jaist.ac.jp/flops2014/invited.html - Proceedings to be published as LNCS 8475 - Hyakuman-goku Matsuri Festival http://www.kanazawa-tourism.com/eng/event/event2.php on the day after the symposium (June 7); accommodation can be extended on request basis via the registration site (use the comments field) - More information at: http://www.jaist.ac.jp/flops2014/ Thank you again, FLOPS 2014 Program Co-Chairs Michael Codish and Eijiro Sumii
Categories: Offsite Discussion

News

del.icio.us/haskell - Tue, 05/13/2014 - 11:23am
Categories: Offsite Blogs

Visiting Portland 6/12-6/14 (and Eugene after that)

haskell-cafe - Tue, 05/13/2014 - 10:14am
Hi, I’ll be visiting a summer school in Eugene¹ in June and my travel plans include two days in Portland, (Tuesday June 12th, afternoon until Saturday, June 14th, shortly past noon). If there anybody wants to meet for keysigning/sightseeing/discussing Haskell/other stuff, let me know. Also, I’d be happy to join any interesting event such as User group meetings, and I can offer to hold a talk (most likely something Haskell related, or general Debian topics). I haven’t book accommodation yet. Useful secret tips are welcome :-) After that I’ll be in Eugene for two weeks and although the schedule is full I’m sure there will be time to meet likewise people in the evening. Or even during the event – I would be surprised if I were there the only haskell-cafe reader that attends the summer school. Greetings, Joachim ¹ http://www.cs.uoregon.edu/research/summerschool/summer14/
Categories: Offsite Discussion

Brent Yorgey: Unique isomorphism and generalized “the”

Planet Haskell - Tue, 05/13/2014 - 9:52am

This is part two in a series of posts on avoiding the axiom of choice; you can read part one here.

In category theory, one is typically interested in specifying objects only up to unique isomorphism. In fact, definitions which make use of actual equality on objects are sometimes referred to (half-jokingly) as evil. More positively, the principle of equivalence states that properties of mathematical structures should be invariant under equivalence. This principle leads naturally to speaking of “the” object having some property, when in fact there may be many objects with the given property, but all such objects are uniquely isomorphic; this cannot cause confusion if the principle of equivalence is in effect.

This phenomenon should be familiar to anyone who has seen simple universal constructions such as terminal objects or categorical products. For example, an object is called if there is a unique morphism from each object . In general, there may be many objects satisfying this criterion. For example, in , the category of sets and functions, every singleton set is terminal: there is always a unique function from any set to a singleton set , namely, the function that sends each element of to . However, it is not hard to show that any two terminal objects must be uniquely isomorphic1. Thus it “does not matter” which terminal object we use—they all have the same properties, as long as we don’t do anything “evil”—and one therefore speaks of “the” terminal object of . As another example, a product of two objects is a diagram with the universal property that any other with morphisms to and uniquely factors through . Again, there may be multiple such products, but they are all uniquely isomorphic, and one speaks of “the” product .

Note that in some cases, there may be a canonical choice among isomorphic objects. For example, this is the case with products in , where we may always pick the Cartesian product as a canonical product of and (even though there are also other products, such as ). In such cases use of “the”, as in “the product of and ”, is even more strongly justified, since we may take it to mean “the canonical product of and ”. However, in many cases (for example, with terminal objects in ), there is no canonical choice, and “the terminal object” simply means something like “some terminal object, it doesn’t matter which”.

Beneath this seemingly innocuous use of “the” (often referred to as generalized “the”), however, lurks the axiom of choice! For example, if a category has all products, we can define a functor 2 which picks out “the” product of any two objects and —indeed, may be taken as the definition of the product of and . But how is to be defined? Consider , where denotes the set of all possible products of and , i.e. all suitable diagrams in . Since has all products, this is a collection of nonempty sets; therefore we may invoke AC to obtain a choice function, which is precisely , the action of on objects. The action of on morphisms may then be defined straightforwardly.

The axiom of choice really is necessary to construct : as has already been noted, there is, in general, no way to make some canonical choice of object from each equivalence class. On the other hand, this seems like a fairly “benign” use of AC. If we have a collection of equivalence classes, where the elements in each class are all uniquely isomorphic, then using AC to pick one representative from each really “does not matter”, in the sense that we cannot tell the difference between different choices (as long as we refrain from evil). Unfortunately, even such “benign” use of AC still poses a problem for computation.

  1. If you have never seen this proof before, I highly recommend working it out for yourself. Given two terminal objects and , what morphisms must exist between them? What can you say about their composition? You will need to use both the existence and uniqueness of morphisms to terminal objects.

  2. Note that we have made use here of “the” product category —fortunately , like , has a suitably canonical notion of products.


Categories: Offsite Blogs

Brent Yorgey: Avoiding the axiom of choice, part I

Planet Haskell - Tue, 05/13/2014 - 9:32am

I’m hard at work on my dissertation, and plan to get back to doing a bit of blogging based on stuff I’m writing and thinking about, as a way of forcing myself to explain things clearly and to potentially get some useful feedback. Yes, this means you can expect more on species! But first, I’ll write a few posts about the axiom of choice and anafunctors, which have turned out to be fundamental to some of the work I’ve been doing. If you look at the nLab page for anafunctors, linked above, you could be forgiven for thinking this is a pretty esoteric corner of category theory, but in fact it’s not too bad once you grasp the essentials, and is quite relevant for anyone interested in category theory and constructive/computational foundations (such as homotopy type theory (HoTT)).

The Axiom of Choice

The (in)famous Axiom of Choice (hereafter, AC) can be formulated in a number of equivalent ways. Perhaps the most well-known is:

The Cartesian product of any collection of non-empty sets is non-empty.

Given a family of sets , an element of their Cartesian product is some -indexed tuple where for each . Such a tuple can be thought of as a function (called a choice function) which picks out some particular from each .

The Axiom of Choice in type theory, take 1

We can express this in type theory as follows. First, we assume we have some type which indexes the collection of sets; that is, there will be one set for each value of type . Given some type , we can define a subset of the values of type using a predicate, that is, a function (where denotes the universe of types). For some particular , applying to yields a type, which can be thought of as the type of evidence that is in the subset ; is in the subset if and only if is inhabited. An -indexed collection of subsets of can then be expressed as a function . In particular, is the type of evidence that is in the subset indexed by . (Note that we could also make into a family of types indexed by , that is, , but it wouldn’t add anything to this discussion.)

A set is nonempty if it has at least one element, so the fact that all the sets in are nonempty can be modeled by a dependent function which yields an element of for each index, along with a proof that it is contained in the corresponding subset.

(Note I’m using the notation for dependent function types instead of , and for dependent pairs instead of .) An element of the Cartesian product of can be expressed as a function that picks out an element for each (the choice function), together with a proof that the chosen elements are in the appropriate sets:

Putting these together, apparently the axiom of choice can be modelled by the type

Converting back to and notation and squinting actually gives some good insight into what is going on here:

Essentially, this says that we can “turn a (dependent) product of sums into a (dependent) sum of products”. This sounds a lot like distributivity, and indeed, the strange thing is that this is simply true: implementing a function of this type is a simple exercise! If you aren’t familiar with dependent type theory, you can get the intuitive idea by implementing a non-dependent Haskell analogue, namely something of type

(i -> (a,c)) -> (i -> a, i -> c).

Not too hard, is it? (The implementation of the dependent version is essentially the same; it’s only the types that get more complicated, not the implementation.) So what’s going on here? Why is AC so controversial if it is simply true in type theory?

The Axiom of Choice in type theory, take 2

This is not the axiom of choice you’re looking for. — Obi-Wan Funobi

The problem, it turns out, is that we’ve modelled the axiom of choice improperly, and it all boils down to how non-empty is defined. When a mathematician says “ is non-empty”, they typically don’t actually mean “…and here is an element of to prove it”; instead, they literally mean “it is not the case that is empty”, that is, assuming is empty leads to a contradiction. (Actually, it is a bit more subtle yet, but this is a good first approximation.) In classical logic, these viewpoints are equivalent; in constructive logic, however, they are very different! In constructive logic, knowing that it is a contradiction for to be empty does not actually help you find an element of . We modelled the statement “this collection of non-empty sets” essentially by saying “here is an element in each set”, but in constructive logic that is a much stronger statement than simply saying that each set is not empty.

(I should mention at this point that when working in HoTT, the best way to model what classical mathematicians mean when they say “ is non-empty” is probably not with a negation, but instead with the propositional truncation of the statement that contains an element. Explaining this would take us too far afield; if you’re interested, you can find details in Chapter 3 of the HoTT book, where all of this and much more is explained in great detail.)

From this point of view, we can see why the “AC” in the previous section was easy to implement: it had to produce a function choosing a bunch of elements, but it was given a bunch of elements to start! All it had to do was shuffle them around a bit. The “real” AC, on the other hand, has a much harder job: it is told some sets are non-empty, but without any actual elements being mentioned, and it then has to manufacture a bunch of elements out of thin air. This is why it has to be taken as an axiom; we can also see that it doesn’t fit very well in a constructive/computational context. Although it is logically consistent to assume it as an axiom, it has no computational interpretation, so anything we define using it will just get stuck operationally.

So, we’ll just avoid using AC. No problem, right?

Don’t look now, but AC is behind you

The problem is that AC is really sneaky. It tends to show up all over the place, but disguised so that you don’t even realize it’s there. You really have to train yourself to think in a fundamentally constructive way before you start to notice the places where it is used. Next time I’ll explain one place it shows up a lot, namely, when defining functors in category theory (though thankfully, not when defining Functor instances in Haskell).


Categories: Offsite Blogs

How to build a large binary tree

Haskell on Reddit - Tue, 05/13/2014 - 7:46am

Hello,

I am a Haskell newbie - just learning about Functors, Applicative and Monads. I thought I would play with a simple binary tree and see how far can I get. Well ... not too far - I have the tree defined as follows

data Tree a = Empty | Node a (Tree a) (Tree a) deriving (Eq, Show)

Then I have a function that creates a leaf

leaf :: a -> Tree a leaf x = Node x Empty Empty

Now there is a function that builds a tree using random numbers

buildIntTree :: Int -> IO (Tree Int) buildIntTree acc | acc == 0 = leaf <$> ((`mod` 100) <$> (randomIO :: IO Int) ) | otherwise = do r <- randomIO :: IO Int left <- buildIntTree (acc - 1) right <- buildIntTree (acc - 1) return (Node (r `mod` 100) (left) (right))

It all works, but you will most likely have noticed that my buildIntTree function is recursive and will get stuck for larger number of nodes.

buildIntTree 5

works great obviously, but if I give anything larger that 30 it will get into trouble.

The question I have is how to optimize buildIntTree so that I can build this tree with any number of nodes and not get into stack problems?

submitted by djogon
[link] [17 comments]
Categories: Incoming News

How to get good at haskell

Haskell on Reddit - Tue, 05/13/2014 - 3:06am

Hi guys,

So I'm somewhat new to haskell, and have written a few projects (mostly project euler problems) in haskell, and have been reading a lot of articles on monads, functors, monad combinators, etc. I find haskell really interesting and want to take some time to get really good at haskell. Any resources/project ideas you guys recommend for either conceptually understanding stuff or learning by doing? Project ideas would also be much appreciated. Currently, I'm trying to implement a markdown parser using parsec and applicatives.

To give you guys a quick estimate as to where I think I am at as far as understanding various concepts, I definitely grok monads, and have a pretty good understanding of monoids, applicatives and functors. I'm still working on reading up about lenses and monad combinators. I've read through learn you a haskell and have skimmed through real world haskell.

Thanks

submitted by sakekasi
[link] [34 comments]
Categories: Incoming News

NICTA course :: help with State exercise

Haskell on Reddit - Tue, 05/13/2014 - 2:45am

I'm going through the NICTA course and slowly but surely understand new thing after another when doing exercises. Currently for some reason I am stuck at one point and would like to request a bit of help from you guys to explain me one thing.

Here is what we are given:

instance Applicative (State s) where pure a = State (\s -> (a, s)) get :: State s s get = State (\s -> (s, s)) put :: s -> State s () put s = State (\x -> ((), s))

We are given a task to implement the findM function which has a signature of

findM :: Monad f => (a -> f Bool) -> List a -> f (Optional a)

But before implementing that there is an example:

-- >>> let p x = (\s -> (const $ pure (x == 'c')) =<< put (1+s)) =<< get in runState (findM p $ listh ['a'..'h']) 0 -- (Full 'c',3)

Would you mind helping me out to understand the first part of that example before runState? The definition of "p x". What should my thought process be like when I encounter such a construct? I tried to write it out on the paper but got lost near the end.

submitted by faorien
[link] [6 comments]
Categories: Incoming News