- Haskell-Cafe - Haskell.org

Is this a correct explanation of FRP?
by Peter Minten 04 Apr '12

04 Apr '12

Hi, I've been trying to get my head around Functional Reactive Programming by writing a basic explanation of it, following the logic that explaining something is the best way to understand it. Am I on the right track with this explanation? Greetings, Peter Minten P.S. Sorry about the long mail, the explanation ended up a little longer than I originally expected. :) Document (with markdown formatting) follows: --8<--8<--8<--8<--8<--8<--8<--8<--8<--8<--8<--8<--8<--8<--8<--8<-- This is an attempt to explain Functional Reactive Programming (FRP) enough to give a reader with no previous exposure to FRP an intuition what FRP is about. After reading this you should hopefully understand enough of FRP to understand the [reactive-banana](http://www.haskell.org/haskellwiki/Reactive-banana) examples. FRP has certain terms such as behavior, event and time-varying that can be confusing for people unfamiliar with it. I'll avoid these terms at first and will focus on spreadsheets and a generalization of spreadsheet cells (which I will call boxes). Later, once the most important concepts are explained, reactive-banana syntax will be introduced along with an example that demonstrates how to work with behaviors and events in reactive-banana. Finally some theory about time-varying functions and how events and behaviors can be implemented using pure functions by making time explicit should provide the necessary background to understand reactive-banana's haddock comments. The version of reactive-banana used here is [0.5.0.0](http://hackage.haskell.org/package/reactive-banana-0.5.0.0). Reactive Programming for the Masses: The Spreadsheet ==================================================== Spreadsheets are something we all (for certain values of we) know about. Let's talk about a typical, simplified, spreadsheet. We have a list of products that we sell and want to compute their price with the Value Added Tax (VAT) added. We might have cells A1 to A10 contain the raw prices of our products and cell B1 contain the current VAT rate (say 19 for a 19% VAT). In cells C1 to C10 we'd like to see the prices including VAT. In cell C1 we'd have a formula: `=A1*(1+B1/100)`, in cell C2 `=A2*(1+B1/100)`, etc. So if A1 contains $100 C1 would contain $119. But what if the government, in it's eternal quest to reduce the budget deficit, raises the VAT rate? We'd adjust cell B1, just change it to 20. And like magic all the C cells are updated. Though this may seem mundane what we've just seen is actually a very good example of reactive programming. We didn't tell the C cells to update; they updated on their own because a value they depend on changed. >From Cells to Boxes: Generalizing the Spreadsheet ================================================= Spreadsheets are nice, but if we want to truly get a feel for FRP we'll have to think beyond them. If we look at a spreadsheet at an abstract level it pretty much consists of cells of two types: value cells (`19`) and formula cells (`=A1*(1+B1/100)`). Let's lose the reference to spreadsheets and talk about boxes. Say, for now, that there are two kinds of boxes: formula boxes and value boxes. Both support a "get" operation that returns a value. Value boxes additionally support a "set" operation that sets the value. Formula boxes can contain any kind of pure function. They can also refer to the values of other boxes (both formula and value boxes). Value boxes don't have a function inside them, they have a value. The translation of our VAT spreadsheet would be something like a formula box *fIncl1* containing the expression `get(vExcl1) * (1 + get(vVat) / 100)`. This expression uses two value boxes: *vExcl1* and *vVat*. We could also write *fIncl1* using a helper formula box *fVat*. Let *fVat* have the formula `1 + get(vVat) / 100` and *fIncl1* have the formula `get(vExcl1) * get(vVat)`. I'll use `:=` for this kind of definition, the `:=` is there to remind you that this isn't Haskell. It's important to note that any kind of value may be put into value boxes, including IO actions and functions. Try doing this with a spreadsheet: `fIncls := [get(ve) * get(vVat) | ve <- vExcls]`. Or this: `fIncl1 := apply(get(vVatFunc), get(vExcl1))`. If you're wondering why I'm not using Haskell syntax, it's to focus on the meaning of boxes rather than what the functions and combinators mean. That said, this pseudo-imperative syntax is on its way out as it's getting too clunky (that `apply` function is really just ugly). For a quick peek ahead the last few examples would be something like this in reactive-banana: fIncls = map (\ve -> (*) <$> ve <*> fVat) vExcls fIncl1 = fVatFunc <*> vExcl1 Events ====== Let's say we want to build the worlds worst synthesizer. We have 7 buttons: "a", "b", "c", "d", "e", "f" and "g". Our output is generated by sampling a box twice per second and playing the frequency in the box until the next sample is taken. This can't be expressed with the crude formula and value boxes system we've had so far. There is no way to express key presses in that system, a key press isn't like changing a value, it's something that occurs on a specific point in time but after it occurs it's forgotten (your keyboard doesn't remember key strokes, at least mine doesn't). In this new system we'll forget about formula boxes and value boxes and introduce event boxes. Event boxes are like formula boxes in that they can refer to the value of other boxes. Event boxes can also react to events. Events can be thought of like signals in something like D-Bus. Multiple things (event boxes) can listen to them and do something once a specific event is fired (triggered). Every event has a value associated with it. Sometimes the value isn't important because the fact that the event has occurred is what's interesting but often we do want to know the value. Events come in streams. When we say event box *b1* changes to the value of event *e1* when it receives that event we're actually saying that whenever an event from the stream of events we colloquially call *e1* comes *b1* changes to the value of that event. Yes, that's confusing so I'll try to be precise. Just remember that when I refer to something like *e1* when defining an event box it's always to a stream of events, never a specific event. If you're puzzled by the stream just think of it as an acknowledgement that a certain kind of event can occur multiple times. It actually goes a lot deeper than that, involving those confusing `[(t, e)]` types, but for now just remembering that a kind of event can occur multiple times with possibly different values is good enough. Events have values and we can use that to chose to do something only for events with some value. So not only can we determine which streams of events we'll do something with when defining an event box, we can also determine for what values of events we'll do something. For example if we have an event that directly sets our synthesizer frequency we can apply a filter that only allows events with frequencies that are pleasant to the human ear. Some Reactive-Banana syntax =========================== Expressing event handling with the pseudo-code I've used before is tricky and gets near impossible soon. So it's a good thing that once you've understood or at least got a basic idea of the concepts of event streams and event boxes the syntax of reactive-banana starts to make sense. In this section I'll explain the most fundamental functions and operators. If you're reading the [reactive-banana 0.5 haddocks](http://hackage.haskell.org/package/reactive-banana-0.5.0.0) there are a few things to keep in mind. The first is that what I've called an event box in the previous section is called a Behaviour in reactive-banana. To avoid confusion I'll stop using the term event box from here on. In the reactive-banana haddocks you'll find a lot of references to time-varying functions and lists involving time variables. Just ignore those, they're important but we'll get to them later. As a general rule just ignore what you don't understand. You'll also notice a `t` parameter on the `Event` and `Behavior` types. It's basically similar to the `s` parameter for `STRef`, it's a trick to use the type system to prevent constructs that would result in undefined or incorrect behavior. Just ignore it. For understanding the next sections you'll need to know about a basic subset of reactive-banana which I'll explain here. First up: event streams. Events ------ Event streams are represented by the type Event in reactive-banana. The type `Event t Int` means a stream of events carrying Int values. There are three basic things you can do with just event streams. You can transform the events in them, you can filter in events in them and you can combine the event streams. Transforming an event stream means changing the values carried by the events in them. As this is *Functional* Reactive Programming the streams themselves are not changed. When you transform a stream you create a new stream. Whenever an event in the old stream is fired an event in the new stream is also fired, but with a different value. Transforming an event stream is done primarily by good old fmap. The expression ``show `fmap` eInt`` (or with the (`<$>`) operator `show <$> eInts`) with *eInt* having the type `Event t Int` creates a new event stream of the type `Event String` with the int in every event in the original stream being a string in the new stream. To replace the value of an event (if the event doesn't carry a useful value) just use (`<$`): `"MOO!" <$ eWhatever` causes every value in the stream eWhatever to be replaced by MOO!. Like (`<$>`) this is an operator from Control.Applicative. Filtering is done using the `filterE` function. When you filter an event stream you create a new event stream with the same associated values but which doesn't contain all the events from the original stream. To only deal with events with positive integers you can create a filtered stream using ``filterE (>= 0) eInt``. Combining event streams creates a new event stream with all the events from both streams. So if you combine *eOne* and *eTwo* into *eThree* there will be an event in *eThree* for every event in *eOne* and for every event in *eTwo*. Combining is done with the union function: ``eThree = eOne `union` eTwo``. Beware however that when events come in at the same time things can get a little tricky, you'd have to wonder in what order the events are processed. Reactive-banana contains several functions to handle simultaneous events. For the purpose of this document we'll do the easiest thing and ignore simultaneous events. In real world code you would need to think about it. Behaviors --------- To create a behavior (event box) in reactive-banana you'll typically use one of two functions: `stepper` and `accumB`. Both work with an initial value and an event stream. The difference is that when an event occurs `stepper` changes the value of the behavior to the value in the event while `accumB` applies the function in the event to the value of the behavior. eNewVal :: Event t Int bSet :: Behavior t Int bSet = stepper 0 eNewVal eUpdater :: Event t (Int -> Int) bUpdated :: Behavior t Int bUpdated = accumB 0 eUpdater The expression `bSet = stepper 0 eNewVal` creates a behavior named *bSet* with initially value 0. Once an event from the *eNewVal* stream comes in the value of *bInt* changes to the value in that event. So if an event comes in with value 2 the value of bSet becomes 2. On the other hand the expression `bUpdated = accumB 0 eUpdater` makes *bUpdated* a behavior with initially the value 0 but which gets updated (modified) whenever an event comes in. If an event comes in with value (+1) (a slice, so `\x -> x + 1`) and the current value of *bUpdated* is 1 the new value becomes 2. That's basically it for behaviors. Well, there's a third way to create behaviors: using `pure`. To create a behavior with the value 1 which doesn't change at all use `pure 1`. In case you didn't know, for applicative functors (which behaviors are) `pure` is what `return` is for monads. To create a behavior that's depends on old behaviors (`f3 := get(f1) + get(f2)` in our old formula box syntax) we have to use applicative functor functions in reactive-banana. There is unfortunately no option to use monad syntax. To express that the value of *b3* is the sum of the value of *b1* and the value of *b2* we write: `b3 = (+) <$> b1 <*> b2`. Example: The Worlds Worst Synthesizer ===================================== Now for an example. We'd like to create a synthesizer. The synthesizer will use our keyboard for input, which we notice through a stream of events called *eKey* with as associated value a Char containing the key that was pressed. Something outside our program (and scope of discussion) samples the behavior *bNote* every 100ms and plays the tone currently in there until the next sample time. To avoid getting caught up in music theory (read: I'm lazy and can't be bothered to look up tone frequencies) the note to play is expressed as an algebraic data type. type Octave = Int data Pitch = PA | PB | PC | PD | PE | PF | PG data Note = Note Octave Pitch -- Type signature for the key event, it comes from outside our -- system. eKey :: Event t Char You'll notice the octave. To change the octave we'll use the '-' and '+' keys. To set the pitch we'll use the 'a'..'g' keys on the keyboard. Never mind that it's really annoying to play with those keys as they're scattered all over the keyboard, this is about the FRP logic not practicality. Those chars in the *eKey* event stream need to be translated to pitches. Here's one way to do that. ePitch :: Event t Pitch ePitch = (PA <$ filterE (=='a') eKey) `union` (PB <$ filterE (=='b') eKey) `union` ... (PG <$ filterE (=='g') eKey) The "trouble" here is that we're filtering the stream multiple times, not very efficient. Here's a better way. table = [('a', PA), ('b', PB), ..., ('g', PG)] ePitch = filterJust $ (\e -> lookup e table) <$> eKey The `filterJust` function is a simple helper in reactive-banana. It filters out `Nothing` events and returns the value inside the `Just` constructor for `Just` events. To get *ePitch* we first look up the characters in the translation table and then remove all events who's chars aren't in the table, removing the `Just` wrapper from events who's chars are in the table at the same time. The *bNote* behavior will not use these events directly, instead *bOctave* and *bPitch* will each store part of the note and *bNote* will combine the information. eOctUp, eOctDown :: Event t Char eOctUp = filterE (=='+') eKey eOctDown = filterE (=='-') eKey bOctave :: Behavior t Octave bOctave = accumB 0 $ ((+1) <$ eOctUp) `union` ((subtract 1) <$ eOctDown) bPitch :: Behavior t Pitch bPitch = stepper PC ePitch bNote :: Behavior t Note bNote = Note <$> bOctave <*> bPitch If you understand what's going on here you should have a basic idea of what FRP is in practice. There are of course considerations in the real world that we've skipped over here, such as how to get the keyboard event and how to play the sounds. To get a better idea of what FRP in the real world looks take a look at the [reactive-banana examples](http://www.haskell.org/haskellwiki/Reactive-banana/Examples), they should be easy to follow. When following those examples you'll come across the (`<@`) and (`<@>`) operators. I'll give a short introduction here to make it easier to understand the examples. The (`<@`) operator is used like this: `e2 = b1 <@ e1`, if an event in stream *e1* comes in the value of that event is replaced in the *e2* stream by whatever value is in *b1* at the time. The (`<@>`) operator is used in much the same way, but it doesn't replace the value from *e1* outright but uses it to compute a new value. bOne :: Behavior t Int bOne = pure 1 bPlusOne :: Behavior t (Int -> Int) bPlusOne = pure (+1) eAlwaysOne, ePlusOne :: Event t Int eAlwaysOne = bOne <@ eWhatever ePlusOne = bPlusOne <@> eInt Time-varying values and functions ================================= If you've read about FRP before you're likely to have come across the term "time-varying function". This sounds difficult, but once you understand the basics of behaviors and events it's really no big deal. Here's the clue: a behavior contains a value, but the value can change. Therefore at different points in time a behavior can have different values. So we could say that a behavior has a value that varies in time. We could also throw away the concept of boxes and say a behavior *is* a value that varies in time. This is more correct, those boxes are helpful as teaching concepts but once we talk directly about time they are no longer needed. So, a time-varying value is simply a behavior as behaviors can have different values at different points in time. A time-varying function is also just a behavior, one where the value is a function (functional programming 101: the clue to every riddle is that functions are values). To go further down the rabbit hole a time-varying value can actually be thought of as a function by making time explicit. If a behavior has value 1 up to the 30th's second and from that point forward value 2 we could express the behavior as: `\t -> if t < 30 then 1 else 2`. This is important: by making time explicit we can reason about behaviors as if they were pure functions. While in practice we're dealing with applicative functors (or in other libraries monads or arrows) we can think of behaviors as pure functions. Real world behaviors aren't as simple as from 30 seconds onwards change to value 2. They interact with events. So to express such behaviors as pure functions events need to be expressed in a way that works for pure functions. This is where the `[(t,e)]` type comes in. We can see events as a list of values at certain points in time, for example `[(10, 1), (20, 2), (30, 3)]` for events that occur on second 10, 20 and 30 with values 1, 2 and 3 respectively. When viewing events in such a way it becomes easy to create a behavior that changes to whatever value was last: type Time = Int stepped :: [(Time, Int)] -> Time -> Int stepped es t = case takeWhile (\(t', _) -> t' <= t) es of [] -> 0 xs -> snd (last xs) For once this is actually runnable code. If we invoke it as `stepped [(10,1),(20,1),(30,1)] 2` the result is 0, if we invoke it as `stepped [(10,1),(20,1),(30,1)] 12` the result is 1, as expected. Stepped sounds a lot like stepper and we can create that function by making a few small adjustments. type Time = Int stepper :: a -> [(Time, a)] -> (Time -> a) stepper d es = \t -> case takeWhile (\(t', _) -> t' <= t) es of [] -> d xs -> snd (last xs) If you understand this bit, why behaviors and events can be expressed by making time explicit you have a good intuition of what FRP is. Good luck on your endeavors in FRP land.

6 12

GSOC Proposal 2012 : HDBC
by pranjal pandit 04 Apr '12

04 Apr '12

Hi, I would like to work on improving the HDBC as a GSOC project 2012. I have a previous working experience with Django and its ORM and I had a look at Amnesia (http://amnesia.sourceforge.net/user_manual/manual.html) which is a SQL database interface for Erlang. Few of the features of both include: 1 ) Database operation are supported through Language Native types. 2 ) Direct table creation from native language constructs. (models.py in Django and *tablename*.hrl in Amnesia) I would like to make developement in HDBC so that all Database interactions are made through Haskell Native data type. For eg - In using Erlang Database interface through Amnesia on would write (Quoting example from Amnesia Documentation) populate() -> {ok, Pid} = amnesia:open(sales), %% adding customer {ok, Cust1} = amnesia:add_new (Pid, #customer {customer_code = 102341, name = "John", address = "XXXXX", email = "john@xxx"}), %% adding product {ok, P1} = amnesia:add_new (Pid, #product { product_code = "001", description = "CPU Intel", price = 231.10 }), %% now let's add an order for customer "Cust2" {ok, Order} = amnesia:add_new (Pid, #orders { order_number = 30, order_date = {2008, 7, 17}, customer = Cust1 }), Here each Erlang record (#customer, #product and #orders) are responsible for different Database Tables. So writing the first statement inserts into database and return an object Cust1 that can be used late down the line to create an order table object. In Django through Python one would have written: customer = Customer.objects.create(customer_code=102341, name = "John", address = "XXXXX", email = "john@xxx" ) order = Orders.objects.create(order_number = 30, order_date = {2008, 7, 17}, customer = customer) Writing everything through Language type increases more readability inside the code. Additionally this helps in abstracting the logic in code from the underlying SQL being executed. In addition to the support for select, insert, update queries the my work would extend support for Joins, aggregations etc all in Haskell Native Types. I would also like to work to handle the database queries from wire formats/ binaries instead of strings as is the case currently. I would like to close down these two features as a GSOC project during the summer of 2012 and I would your feedback on the same. -- Regards Pranjal Pandit Don't communicate by sharing memory; share memory by communicating.

3 2

Conduits: Is Source a valid instance of Monad?
by Aristid Breitkreuz 04 Apr '12

04 Apr '12

Hi all, As you may have noticed, Michael Snoyman has been working on an alternative approach to I/O, called conduits. You can find it here: https://github.com/snoyberg/conduit When looking at the Source type (explained here: http://www.yesodweb.com/blog/2011/12/conduits) I noticed that they seem to behave "like lists", and naturally wondered if I could write a Monad instance for them. But first, let's have a brief look at the definition of Source: data SourceResult a = Open a | Closed data PreparedSource m a = PreparedSource { sourcePull :: ResourceT m (SourceResult a) , sourceClose :: ResourceT m () } newtype Source m a = Source { prepareSource :: ResourceT m (PreparedSource m a) } ResourceT deals with resource acquisition and releasing (making sure that all resources are released), and provides a an abstraction over IORef/STRef. For our purposes here, ResourceT is probably close enough to IO. So now the question again is, can we write a Monad instance for this? I have been able to write join (concatenate) and return (a source with a single non-repeated) element. https://gist.github.com/1525471 I _think_ it behaves properly like a Monad, but I'm not quite sure, and neither was Michael. Greg Weber then suggested bringing the question to this forum. What made the question difficult for me is that this would be a stateful Monad transformer, so I'm not quite sure how to test the Monad laws properly. There's a second part to this question: If Source turns out not to be a Monad, is it possibly a ZipList-like Applicative? And either way, which is more useful: The list-like or the ziplist-like instances (of Applicative/Monad)? Thank you, Aristid

4 4

GSOC Proposal 2012 : HDBC
by Greg Weber 04 Apr '12

04 Apr '12

Hi Pranjal, We are glad you are interested in the GSoC. Please take a look at persistent: http://www.yesodweb.com/book/persistent It performs queries and serialization based on Haskell records. It also uses native drivers rather than HDBC. I created a proposal outline [1] and there is a student submission for it [2] [1] http://hackage.haskell.org/trac/summer-of-code/ticket/1605 [2] http://hackage.haskell.org/trac/summer-of-code/ticket/1605 Let me know if you are interested in that or need help coming up with a proposal Thanks, Greg Weber

1 0

mueval leaving behind tmp files
by Johannes Waldmann 04 Apr '12

04 Apr '12

The following program prints Right ("test","Bool","True") as it should, but it leaves behind in /tmp two files (name is a long string of digits) and an empty directory (name is ghcNNNNN_N). ... and it deletes the input file (/tmp/Main.hs). That's not nice. Ideally, I would want to read input from a String (instead of the file), and not write to disk at all. But cleaning up properly would be OK as a work-around. import Language.Haskell.Interpreter import Mueval.Interpreter import Mueval.ArgsParse main = do writeFile "/tmp/Main.hs" "test = True" result <- runInterpreter $ interpreter $ Options { timeLimit =1, modules =Just ["Prelude"], expression ="test" , loadFile ="/tmp/Main.hs", user="what", printType =True , extensions =False,namedExtensions = [] , noImports =False, rLimits =False, help=True } print result ghc --version The Glorious Glasgow Haskell Compilation System, version 7.4.1 ghc-pkg list| egrep 'mueval|hint' hint-0.3.3.4 mueval-0.8.1.1 uname -a Linux octopus 3.0.0-16-generic #29-Ubuntu SMP Tue Feb 14 12:48:51 UTC 2012 x86_64 x86_64 x86_64 GNU/Linux

2 2

GSoC proposal: Units for GHC
by Nils Schweinsberg 04 Apr '12

04 Apr '12

Hi Haskell-Cafe & GHC-users! I'm looking to apply for the GSoC and since I've worked on GHC before I'd like to continue to do so. My proposal would be something that tempted me (as a physics student) for a while: Units for Haskell/GHC. This project has been suggested for a long time on the GHC wiki, and there is already a lot of work done for other languages like ML, F# etc[1]. I have tried to implement e.g. the unification algorithm from the "Types for Units-of-Measure in F#" talk[2] for an abstract syntax tree[3] and it was pretty much straight forward. As I see it, the project would consist of: 1.) Find appropriate rules/algorithms for unit analysis. Most (if not all?) of this should be covered in those papers/talks on [1]. 2.) Applying the rules to the Haskell syntax tree used in GHC. I have approximately 3 years of experience with Haskell, I worked for the database research group[4] at the University of Tübingen (Germany) on the Database Supported Haskell[5] library. I've done most of the coding for the monad comprehension[6] extension, which has been added to the latest GHC release version. I'm already quite familiar with the GHC internals of the compiler/typechecker, and even though I'd have to look up how exactly type interference etc. works in GHC (as I've only *used* it, but never tried to understand/modify it) I'm confident that the work on GHC itself should be doable in the given timeframe. So my questions would be: Do you think this is a appropriate GSoC project? What should I include in the application/project proposal? Anything else? Opinions, suggestions? I realize that I'm kind of late and probably should have written this email a long time ago. But there are still 2 days left for the student application and hopefully I'll get some good feedback by then. - Nils [1]: http://research.microsoft.com/en-us/um/people/akenn/units/index.html [2]: http://research.microsoft.com/en-us/um/people/akenn/units/MLWorkshop2008.pdf [3]: https://github.com/mcmaniac/units/blob/master/src/Unification.hs [4]: http://db.inf.uni-tuebingen.de/team [5]: http://hackage.haskell.org/package/DSH [6]: http://db.inf.uni-tuebingen.de/files/giorgidze/haskell2011.pdf

3 3

Re: [Haskell-cafe] GSoC proposal: Units for GHC
by George Giorgidze 04 Apr '12

04 Apr '12

Implementing this proposal in GHC, as opposed to the library-only approach, would allow for generation of much more useful and user friendly error messages. I believe this aspect is important when it comes to type systems supporting physical units. Cheers, George > This sounds pretty cool and useful. How much of this can be implemented in a library and how much of this would need to be supported on a compiler level? Ideally, most of this would be solved on the library level.

1 0

ANNOUNCE: fast-tags-0.0.1
by Evan Laforge 04 Apr '12

04 Apr '12

A while back I was complaining about the profusion of poorly documented tags generators. Well, there is still a profusion of poorly documented tags generators... I was able to find 5 of them. So, that said, here's my contribution to the problem: fast-tags, haskell tag generator #6. Why not use one of the other 5? Two of them use haskell-src which means they can't parse my code. Two more use haskell-src-exts, which is slow and fragile, breaks on partially edited source, and doesn't understand hsc. Then there's the venerable hasktags, but it's buggy and the source is a mess. I fixed a bug where it doesn't actually strip comments so it makes tags to things inside comments, but then decided it would be easier to just write my own. fast-tags is fast because it has a parser that's just smart enough to pick out the tags. It can tagify my entire 300 module program in about a second. But it's also incremental, so it only needs to do that the first time. I have vim's BufWrite autocommand bound to updating the tags every time a file is written, and it's fast enough that I've never noticed the delay. It understands hsc directly (that's trivial, just ignore the # lines) so there's no need to run hsc2hs before tagifying. The result is tags which are automatically up to date all the time, which is nice. If people care about lhs and emacs tags then it wouldn't be hard to support those too, and at that point I could replace hasktags and we'd be back down to 5 again. But I'm not even sure anyone uses hasktags, since surely someone would have noticed that comment bug. Anyway, it's been working great for me for a couple weeks so I uploaded it to hackage: http://hackage.haskell.org/package/fast-tags

5 9

A Modest Records Proposal
by Gershom B 02 Apr '12

02 Apr '12

The records discussion has been really complicated and confusing. But I have a suggestion that should provide a great deal of power to records, while being mostly[1] backwards-compatible with Haskell 2010. Consider this example: data A a = A{a:a, aa::a, aaa :: a -> A (a -> a)} data B a = B{aaa :: a -> A (a -> a), a :: A} Now what is the type of this? aaaa aaaaa a aa = aaaaa{a = a, aaa = aa} Using standard Haskell typeclasses this is a difficult question to answer. The types of aaaa for A and B do not unify in an obvious way. However, while they are intensionally quite distinct, they unify trivially extensionally. The obvious thing to do is then to extend the type system with extensional equality on record functions. Back when Haskell was invented, extensional equality was thought to be hard. But purity was thought to be hard too, and so were Monads. Now, we know that function existentionality is easy. In fact, if we add the Univalence Axiom to GHC[2], then this is enough to get function existensionality. This is a well-known result of Homotopy Type Theory[3], which is a well-explored approach that has existed for at least a few years and produced more than one paper[4]. Homotopy Type Theory is so sound and well understood that it has even been formalized in Coq. Once we extend GHC with homotopies, it turns out that records reduce to mere syntactic sugar, and there is a natural proof of their soundness (Appendix A). Furthermore, there is a canonical projection for any group of fields (Appendix B). Even better, we can make "." into the identity path operator, unifying its uses in composition and projection. In fact, with extended (parenthesis-free) section rules, "." can also be used to terminate expressions, making Haskell friendly not only to programmers coming from Java, but also to those coming from Prolog! After some initial feedback, I'm going to create a page for the Homotopy Extensional Records Proposal (HERP) on trac. There are really only a few remaining questions. 1) Having introduced homotopies, why not go all the way and introduce dependent records? In fact, are HERP and Dependent Extensional Records Proposal (DERP) already isomorphic? My suspicion is that HERP is isomorphic, but DERP is not. However, I can only get away with my proof using Scott-free semantics. 2) Which trac should I post this too? Given how well understood homotopy type theory is, I'm tempted to bypass GHC entirely and propose this for haskell-prime. 3) What syntax should we use to represent homotopies? See extend discussion in Appendix C. HTH HAND, Gershom [1] To be precise, 100% of Haskell 2010 programs should, usually, be able to be rewritten to work with this proposal with a minimal set of changes[1a]. [1a] A minimal set of changes is defined as the smallest set of changes necessary to make to a Haskell 2010 program such that it works with this proposal. We can arrive at these changes by the following procedure: 1) Pick a change[1b]. 2) Is it minimal? If so keep it. 3) are we done? If not, make another change. [1b] To do this constructively, we need an order. I suggest the lo mein, since noodles give rise to a free soda. [2] I haven't looked at the source, but I would suggest putting it in the file Axioms.hs. [3] http://homotopytypetheory.org/ [4] http://arxiv.org/ *Appendix A: A Natural Proof of the Soundness of HERP Take the category of all types in HERP, with functions as morphisms. Call it C. Take the category of all sound expressions in HERP, with functions as morphisms. Call it D. Define a full functor from C to D. Call it F. Define a faithful functor on C and D. Call it G. Draw the following diagram. F(X)----F(Y) | | | | | | G(X)----G(Y) Define the arrows such that everything commutes. *Appendix B: Construction of a Canonical Projection for Any Group of Fields. 1) Take the fields along the homotopy to an n-ball. 2) Pack them loosely with newspaper and gunpowder. 3) Project them from a cannon. In an intuitionistic logic, the following simplification is possible: 1) Use your intuition. *Appendix C: Homotopy Syntax Given that we already are using the full unicode set, what syntax should we use to distinguish paths and homotopies? At first, I thought we could avoid providing any syntax for homotopies at all. Haskell is a language with type inference, so we should just be able to infer paths and homotopies behind the scenes by adding homotopies to the type system. That's a very nice answer in theory. But in the real world, when we're writing code that solves actual problems, theoretical niceties break down. What if a user wants to use a nonstandard homotopy? Why should we stop them just because we're too lazy to come up with a good syntax? I then realized that we keep running out of syntax because we've limited ourselves to unicode. Instead, I propose we add a potentially infinite universe of identifiers: youtube videos. For example, the higher inductive type for a circle can be written as: homotopyType http://www.youtube.com/watch?v=dQw4w9WgXcQ where Base ::: http://www.youtube.com/watch?v=dQw4w9WgXcQ Loop ::: http://www.youtube.com/watch?v=J---aiyznGQ Base Base Note that the urls do not use SSL. For portability reasons, I propose that SSL only be enabled as an optional extension.

8 9

(no subject)
by Mark Snyder 02 Apr '12

02 Apr '12

<a href="http://dreadscottart.com/mynewwebsite/wp-content/plugins/extended-comment-o…"> http://dreadscottart.com/mynewwebsite/wp-content/plugins/extended-comment-o…</a>

1 0