User loginNavigation 
Type TheoryBackpack: Retrofitting Haskell with a Module System, at last
By gasche at 20140105 16:59  Type Theory  login or register to post comments  other blogs  10491 reads
Pure Subtype SystemsPure Subtype Systems, by DeLesley S. Hutchins:
A thoughtprovoking 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 sideeffect 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 featureoriented programming. By naasking at 20131108 23:53  Lambda Calculus  ObjectFunctional  OOP  Type Theory  39 comments  other blogs  21219 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  20724 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  15420 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  33354 reads
MixedSite VarianceRoss Tate is calling for "Industry Endorsement" for his paper MixedSite 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 declarationsite variance, because designers believed its simplicity would make it easier for programmers to adopt. Indeed, declarationsite 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 mixedsite variance, a careful combination of definitionsite and usesite 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. 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  27856 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 lot going on here. Personally, I see parallels with "lambda with letrec" and "callbypushvalue," although making the connection with the latter takes some squinting through some of Levy's work other than his CBPV thesis. Study this to understand OCaml type inference and/or MLF, or for insights into region typing, or, as the title suggests, for suggestive analogies between polymorphism and garbage collection. By Paul Snively at 20130310 16:25  Functional  Implementation  Type Theory  1 comment  other blogs  16254 reads
Records, sums, cases, and exceptions: Rowpolymorphism at workVideo: Records, sums, cases, and exceptions: Rowpolymorphism at work, Matthias Blume.
Found this to be an enjoyable and thorough overview of MLPolyR, a language created for a PL course that goes allout on various dimensions of row polymorphism, resulting in a small yet powerful language. (previously) By Manuel J. Simoni at 20121101 10:12  Implementation  Type Theory  4 comments  other blogs  17475 reads
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 20120816 05:40  Functional  Software Engineering  Type Theory  3 comments  other blogs  19963 reads

Browse archivesActive forum topics 
Recent comments
9 hours 10 min ago
11 hours 27 min ago
13 hours 18 min ago
16 hours 57 min ago
1 day 6 hours ago
1 day 9 hours ago
1 day 15 hours ago
2 days 1 hour ago
2 days 2 hours ago
2 days 4 hours ago