## User login## Navigation |
## Functional## Extensible Effects -- An Alternative to Monad TransformersExtensible Effects -- An Alternative to Monad Transformers, by Oleg Kiselyov, Amr Sabry and Cameron Swords:
A follow-up to Oleg's delimited continuation adaptation of Cartwright and Felleisen's work on Extensible Denotational Language Specifications, which is a promising alternative means of composing effects to the standard monad transformers. This work embeds a user-extensible effect EDSL in Haskell by encoding all effects into a single effect monad using a novel open union type and the continuation monad. The encoding is very similar to recent work on Algebraic Effects and Handlers, and closely resembles a typed client-server interaction ala coroutines. This seems like a nice convergence of the topics covered in the algebraic effects thread and other recent work on effects, and it's more efficient than monad transformers to boot. By naasking at 2013-07-29 14:53 | Functional | Logic/Declarative | Theory | Type Theory | 22 comments | other blogs | 27895 reads
## How OCaml type checker works -- or what polymorphism and garbage collection have in commonHow OCaml type checker works -- or what polymorphism and garbage collection have in common
As usual with Oleg, there's a By Paul Snively at 2013-03-10 16:25 | Functional | Implementation | Type Theory | 1 comment | other blogs | 14720 reads
## Visi.ioVisi.io comes from David Pollak and aims at revolutionizing building tablet apps, but the main attraction now seems to be in exploring the way data flow and cloud computing can be integrated. The screencast is somewhat underwhelming but at least convinces me that there is a working prototype (I haven't looked further than the website as yet). The vision document has some nice ideas. Visi.io came up recently in the discussion of the future of spreadsheets. By Ehud Lamm at 2012-10-27 09:36 | Functional | Logic/Declarative | Parallel/Distributed | 2 comments | other blogs | 11564 reads
## Milner Symposium 2012The Milner Symposium 2012 was held in Edinburgh this April in memory of the late Robin Milner.
The programme consisted of academic talks by colleagues and past students. The talks and slides are available online. I particularly liked the interleaving of the personal and human narrative underlying the scientific journey. A particularly good example is Joachim Parrow's talk on the origins of the pi calculus. Of particular interest to LtU members is the panel on the future of functional programming languages, consisting of Phil Wadler, Xavier Leroy, David MacQueen, Martin Odersky, Simon Peyton-Jones, and Don Syme. By Ohad Kammar at 2012-10-16 17:31 | Functional | General | History | Parallel/Distributed | Semantics | Theory | 3 comments | other blogs | 12762 reads
## CUFP 2012 TutorialsIf you are in Denmark in September you should attend. If not, raise a glass to salute what is now abundantly clear: FPLs are conquering the ("real") world. ## Koka a function oriented language with effect inference
Koka extends the idea of using row polymorphism to encode an effect system and the relations between them. Daan Leijen is the primary researcher behind it and his research was featured previously on LtU, mainly on row polymorphism in the Morrow Language. So far there's no paper available on the language design, just the slides from a Lang.Next talk (which doesn't seem to have video available at Channel 9), but it's in the program for HOPE 2012. By Daniel Yokomizo at 2012-08-16 05:40 | Functional | Software Engineering | Type Theory | 3 comments | other blogs | 16904 reads
## Mechanized Î»<sub>JS</sub>Mechanized Î»
More work on mechanizing the actual, implemented semantics of a real language, rather than a toy. By Paul Snively at 2012-06-27 15:28 | Functional | Javascript | Lambda Calculus | Semantics | 6 comments | other blogs | 12193 reads
## How to Make Ad Hoc Proof Automation Less Ad HocHow to Make Ad Hoc Proof Automation Less Ad Hoc
If you've ever toyed with Coq but run into the difficulties that many encounter in trying to construct robust, comprehensible proof scripts using tactics, which manipulate the proof state and can leave you with the "ground" of the proof rather than the "figure," if you will, in addition to being fragile in the face of change, you may wish to give this a read. It frankly never would have occurred to me to try to turn Ltac scripts into By Paul Snively at 2012-06-22 15:41 | Functional | Implementation | Logic/Declarative | Type Theory | 9 comments | other blogs | 8097 reads
## Validating LR(1) parsers
I've always been somewhat frustrated, while studying verified compiler technology, that the scope of the effort has generally been limited to ensuring that the AST and the generated code mean the same thing, as important as that obviously is. Not enough attention has been paid, IMHO, to other compiler phases. Parsing: The Solved Problem That Isn't does a good job illuminating some of the conceptual issues that arise in attempting to take parsers seriously as functions that we would like to compose etc. while maintaining some set of properties that hold of the individuals. Perhaps this work can shed some light on possible solutions to some of those issues, in addition to being worthwhile in its own right. Note the pleasing presence of an actual implementation that's been used on the parser of a real-world language, C99. By Paul Snively at 2012-06-18 15:15 | DSL | Functional | Implementation | Theory | 4 comments | other blogs | 8700 reads
## Programming with Algebraic Effects and HandlersProgramming with Algebraic Effects and Handlers. Andrej Bauer and Matija Pretnar, arXiv preprint.
Eff has been discussed here before, and it's nice to see some more progress and a much more complete introduction. The paper is intended for a general audience (well, a general audience of PL enthusiasts). It's quite clear and contains a wealth of examples. |
## Browse archives## Active forum topics |

## Recent comments

2 hours 37 min ago

3 hours 13 min ago

3 hours 13 min ago

4 hours 6 min ago

7 hours 50 min ago

8 hours 20 min ago

8 hours 22 min ago

8 hours 55 min ago

9 hours 46 min ago

10 hours 8 min ago