## User login## Navigation |
## Type Theory## Conservation laws for free!In this year's POPL, Bob Atkey made a splash by showing how to get from parametricity to conservation laws, via Noether's theorem:
By Ohad Kammar at 2014-10-28 07:52 | Category Theory | Fun | Functional | Lambda Calculus | Scientific Programming | Semantics | Theory | Type Theory | 5 comments | other blogs | 6990 reads
## Luca Cardelli FestschriftEarlier this week Microsoft Research Cambridge organised a Festschrift for Luca Cardelli. The preface from the book:
Hopefully the videos will be posted soon. By Ohad Kammar at 2014-09-12 10:10 | Category Theory | Lambda Calculus | Misc Books | Semantics | Theory | Type Theory | 4 comments | other blogs | 4360 reads
## Howard on Curry-HowardPhilip Wadler posts his exchange with William Howard on history of the Curry-Howard correspondence. Howard on Curry-Howard. ## Type soundness and race freedom for MezzoType soundness and freedom for Mezzo, Full paper
The Mezzo programming language has been mentioned recently on LtU. The article above is however not so much about the practice of Mezzo or justification of its design choices (for this, see Programming with Permissions in Mezzo, FranÃ§ois Pottier and Jonathan Protzenko, 2013), but a presentation of its soundness proof. I think this paper is complementary to more practice-oriented ones, and remarkable for at least two reasons: - It is remarkably simple, for a complete soundness proof (and race-freeness) of a programming language with higher-order functions, mutable states, strong update, linear types, and dynamic borrowing. This is one more confirmation of the
*simplifying effect*of mechanized theorem proving. - It is the first soundness proof of a programming language that is strongly inspired by Separation Logic. (Concurrent) Separation Logic has been a revolution in the field of programming logics, but it had until now not be part of a full-fledged language design, and this example is bound to be followed by many others. I expect the structure of this proof to be reused many times in the future.
## Backpack: Retrofitting Haskell with a Module System, at last
By gasche at 2014-01-05 16:59 | Type Theory | login or register to post comments | other blogs | 8266 reads
## Pure Subtype SystemsPure Subtype Systems, by DeLesley S. Hutchins:
A thought-provoking take on type theory using subtyping as the foundation for all relations. He collapses the type hierarchy and unifies types and terms via the subtyping relation. This also has the side-effect of combining type checking and partial evaluation. Functions can accept "types" and can also return "types". Of course, it's not all sunshine and roses. As the abstract explains, the metatheory is quite complicated and soundness is still an open question. Not too surprising considering type checking Type:Type is undecidable. Hutchins' thesis is also available for a more thorough treatment. This work is all in pursuit of Hitchens' goal of feature-oriented programming. By naasking at 2013-11-08 23:53 | Lambda Calculus | Object-Functional | OOP | Type Theory | 39 comments | other blogs | 13161 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 first-class 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 almost-but-not-quite generalizations of existing concepts, like "onions" which are kind of a type-indexed 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 First-Class Messages with Match-Functions. 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 "match-functions". 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 first-class 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 index-passing 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 2013-09-04 16:57 | Meta-Programming | Object-Functional | Theory | Type Theory | 42 comments | other blogs | 15471 reads
## Dependently-Typed Metaprogramming (in Agda)Conor McBride gave an 8-lecture 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 2013-08-30 07:34 | Category Theory | Functional | Lambda Calculus | Meta-Programming | Paradigms | Semantics | Teaching & Learning | Theory | Type Theory | 5 comments | other blogs | 11393 reads
## 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 | 23413 reads
## Mixed-Site VarianceRoss Tate is calling for "Industry Endorsement" for his paper Mixed-Site Variance.
Abstract: Java introduced wildcards years ago. Wildcards were very expressive, and they were integral to updating the existing libraries to make use of generics. Unfortunately, wildcards were also complex and verbose, making them hard and inconvenient for programmers to adopt. Overall, while an impressive feature, wildcards are generally considered to be a failure. As such, many languages adopted a more restricted feature for generics, namely declaration-site variance, because designers believed its simplicity would make it easier for programmers to adopt. Indeed, declaration-site variance has been quite successful. However, it is also completely unhelpful for many designs, including many of those in the Java SDK. So, we have designed mixed-site variance, a careful combination of definition-site and use-site variance that avoids the failings of wildcards. We have been working with JetBrains to put this into practice by incorporating it into the design of their upcoming language, Kotlin. Here we exposit our design, our rationale, and our experiences. Mention of it is also at Jetbrain's Kotlin blog. |
## Browse archives## Active forum topics |

## Recent comments

2 hours 27 min ago

2 hours 36 min ago

2 hours 54 min ago

2 hours 59 min ago

3 hours 17 min ago

3 hours 26 min ago

3 hours 30 min ago

3 hours 34 min ago

3 hours 40 min ago

3 hours 47 min ago