User loginNavigation 
TheoryCopatterns: the final approach to codata?Andreas Abel and Brigitte Pientka's WellFounded Recursion with Copatterns; a Unified Approach to Termination and Productivity is one of my highlights of the justfinished ICFP 2013, but it makes sense to focus on the first paper on this work, published at POPL back in January.
Codata has been often discussed here and elsewhere. See notably the discussion on Turner's Total Functional Programming (historical note: this 2004 beautification of the original 1995 paper which had much of the same ideas), and on the categorytheoryinspired Charity language. Given those precedents, it would be easy for the quick reader to "meh" on the novelty of putting "observation" first (elimination rather than introduction rules) when talking about codata; yet the above paper is the first concrete, usable presentation of an observation in a practical setting that feels right, and it solves longstanding problem that current dependentlytyped languages (Coq and Agda) have. Coinduction has an even more prominent role, due to its massive use to define program equivalence in concurrent process calculi; the relevant LtU discussion being about Davide Sangiorgi's On the origins of Bisimulation, Coinduction, and Fixed Points. The POPL'13 paper doesn't really tell us how coinduction should be seen with copatterns. It does not adress the question of termination, which is the topic of the more recent ICFP'13 paper, but I would say that the answer on that point feels less definitive. The SizeChange Termination Principle for Constructor Based LanguagesThe SizeChange Termination Principle for Constructor Based Languages, by Pierre Hyvernat:
Looks like a relatively straightforward and complete description of a termination checker based on a notion of 'sized types' limited to firstorder programs. LtU has covered this topic before, although this new paper doesn't seem to reference that particular Abel work. By naasking at 20130919 01:59  Functional  Theory  login or register to post comments  other blogs  12935 reads
Types for Flexible ObjectsTypes for Flexible Objects, by Pottayil Harisanker Menon, Zachary Palmer, Alexander Rozenshteyn, Scott Smith:
An interesting paper I stumbled across quite by accident, it purports quite an ambitious set of features: generalizing previous work on firstclass cases while supporting subtyping, mutation, and polymorphism all with full type inference, in an effort to match the flexibility of dynamically typed languages. It does so by introducing a host of new concepts that are almostbutnotquite generalizations of existing concepts, like "onions" which are kind of a typeindexed extensible record, and "scapes" which are sort of a generalization of pattern matching cases. Instead of approaching objects via a record calculus, they approach it using its dual as variant matching. Matching functions then have degenerate dependent types, which I first saw in the paper Type Inference for FirstClass Messages with MatchFunctions. Interesting aside, Scott Smith was a coauthor on this last paper too, but it isn't referenced in the "flexible objects" paper, despite the fact that "scapes" are "matchfunctions". Overall, quite a dense and ambitous paper, but the resulting TinyBang language looks very promising and quite expressive. Future work includes making the system more modular, as it currently requires whole program compilation, and adding firstclass labels, which in past work has led to interesting results as well. Most work exploiting row polymorphism is particularly interesting because it supports efficient compilation to indexpassing code for both records and variants. It's not clear if onions and scapes are also amenable to this sort of translation. Edit: a previous paper was published in 2012, A Practical, Typed Variant Object Model  Or, How to Stand On Your Head and Enjoy the View. BigBang is their language that provides syntactic sugar on top of TinyBang. Edit 2: commas fixed, thanks! By naasking at 20130904 16:57  MetaProgramming  ObjectFunctional  Theory  Type Theory  42 comments  other blogs  21321 reads
DependentlyTyped Metaprogramming (in Agda)Conor McBride gave an 8lecture summer course on Dependently typed metaprogramming (in Agda) at the Cambridge University Computer Laboratory:
The lecture notes, code, and video captures are available online. As with his previous course, the notes contain many(!) mind expanding exploratory exercises, some of which quite challenging. By Ohad Kammar at 20130830 07:34  Category Theory  Functional  Lambda Calculus  MetaProgramming  Paradigms  Semantics  Teaching & Learning  Theory  Type Theory  5 comments  other blogs  15619 reads
Extensible Effects  An Alternative to Monad TransformersExtensible Effects  An Alternative to Monad Transformers, by Oleg Kiselyov, Amr Sabry and Cameron Swords:
A followup 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 userextensible 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 clientserver 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 20130729 14:53  Functional  Logic/Declarative  Theory  Type Theory  22 comments  other blogs  33855 reads
Heap space analysis for garbage collected languagesHeap space analysis for garbage collected languages, by Elvira Albert, Samir Genaim, Miguel GÃ³mezZamalloa:
Similar work has been covered here in the past. By naasking at 20130629 15:01  Implementation  Theory  login or register to post comments  other blogs  13354 reads
Dependent Types for JavaScriptDependent Types for JavaScript, by Ravi Chugh, David Herman, Ranjit Jhala:
Some good progress on inferring types for a very dynamic language. Explicit type declarations are placed in comments that start with "/*:". /*: xâˆ¶Top â†’ {Î½ âˆ£ite Num(x) Num(Î½) Bool(Î½)} */ function negate(x) { if (typeof x == "number") { return 0  x; } else { return !x; } } By naasking at 20130323 15:08  ObjectFunctional  Theory  Type Theory  128 comments  other blogs  28369 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 PeytonJones, and Don Syme. By Ohad Kammar at 20121016 17:31  Functional  General  History  Parallel/Distributed  Semantics  Theory  3 comments  other blogs  14107 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 realworld language, C99. By Paul Snively at 20120618 15:15  DSL  Functional  Implementation  Theory  4 comments  other blogs  10076 reads
Interactive Tutorial of the Sequent CalculusInteractive Tutorial of the Sequent Calculus by Edward Z. Yang.
The tool behind this nice tutorial is Logitext. By Manuel J. Simoni at 20120531 14:48  Fun  Javascript  Logic/Declarative  Teaching & Learning  Theory  28 comments  other blogs  16100 reads

Browse archivesActive forum topics 
Recent comments
2 days 2 hours ago
2 days 3 hours ago
2 days 20 hours ago
6 days 15 hours ago
6 days 21 hours ago
6 days 23 hours ago
1 week 9 hours ago
1 week 2 days ago
1 week 3 days ago
1 week 3 days ago