User loginNavigation 
Type TheoryKleisli Arrows of Outrageous FortuneKleisli Arrows of Outrageous Fortune
I discovered this Googling around in an attempt to find some decent introductory material to Kleisli arrows. This isn't introductory, but it's a good resource. :) The good introductory material I found was this. By Paul Snively at 20110514 15:19  Category Theory  Functional  Type Theory  6 comments  other blogs  13874 reads
Asynchronous Proof Processing with Isabelle/Scala and Isabelle/jEditAsynchronous Proof Processing with Isabelle/Scala and Isabelle/jEdit. Makarius Wenzel, UITP 2010.
I thought this was a nice paper on the pragmatics of incremental, interactive proof editing. I've suspected for a while that as programming languages and IDEs grow more sophisticated and do more computationallyintensive checks at compile time (including but not limited to theorem proving), it will become similarly important to design our languages to support modular and incremental analysis. However, IDE designs also need more experimentation, and unfortunately the choice of IDEs to extend seem to be limited to archaic systems like Emacs or industrial behemoths like Eclipse or Visual Studio, both of which constrain the scope for new design  Emacs is too limited, and the API surface of Eclipse/VS is just too big and irregular. (Agdamode for Emacs is a heroic but somewhat terrifying piece of elisp.) By neelk at 20110422 15:06  Implementation  Software Engineering  Type Theory  4 comments  other blogs  11171 reads
Typechecking Modular Multiple Dispatch with Parametric Polymorphism and Multiple InheritanceTypechecking Modular Multiple Dispatch with Parametric Polymorphism and Multiple Inheritance. Eric Allen, Justin Hilburn, Scott Kilpatrick, Sukyoung Ryu, David Chase, Victor Luchangco, and Guy L. Steele Jr. Submitted for publication, December 2010.
So it's Sunday, and I'm researching the interaction of multiple dispatch, typechecking, and parametric polymorphism, when Google spits out this new paper by the Fortress team. Scott Kilpatrick's Master's Thesis Ad Hoc: Overloading and Language Design puts it into perspective:
All of this is a bit over my head, unfortunately, but I find it very interesting nevertheless. And it's heartening that the somewhat neglected multiple dispatch (and multiple inheritance!) is further developed by such a high caliber team. By Manuel J. Simoni at 20110320 16:28  Paradigms  Type Theory  6 comments  other blogs  10074 reads
The Triumph of Types: Principia Mathematica's Impact on Computer Science
The Triumph of Types: Principia Mathematica's Impact on Computer Science. Robert L. Constable
The role the ideas of Principia Mathematica played in type theory in programming languages is often alluded to in our discussions, making this contribution to a meeting celebrating the hundredth anniversary of WhiteheadandRussell's opus provocative. To get your juices going here is a quote from page 3:
...I will discuss later our efforts at Cornell to create one such type theory, Computational Type Theory (CTT), very closely related to two others, the Calculus of Inductive Constructions (CIC) implemented in the Coq prover and widely used, and Intuitionistic Type Theory (ITT) implemented in the Alf and Agda provers. All three of these efforts, but especially CTT and ITT, were strongly influenced by Principia and the work of Bishop presented in his book Foundations of Constructive Analysis. Generative Type Abstraction and Typelevel ComputationGenerative Type Abstraction and Typelevel Computation (Extended Version), by Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, Steve Zdancewic:
Typelevel computation is becoming more common and more elaborate, thanks to recent extensions such as type families. Other nonparametric features allow the developer to reason about the concrete types used in a computation. Unfortunately, something as simple as a typebased dispatch can be unsound when combined with coercion lifting. This paper solves the tensions between these two useful features using a kind system extended with "roles". In fact, this isn't the first time coercion lifting has caused trouble. In capability security terminology, coercion lifting is a "rights amplification" operation, and there are previously known examples of seemingly innocuous coercion lifting across an abstraction/implementation boundary resulting in Confused Deputies. There's no discussion of this connection in the paper, and the paper cannot solve the problem discussed at that link, which exposes a much deeper issue than confusing parametric/nonparametric contexts. Omega  Language of the FutureWhen I discovered Tim Sheard's Languages of the Future, I realized that PLs do indeed have a future (beyond asymptotically approaching CLOS and/or adding whimsical new rules to your type checker). Compared to languages like Lisp, pregenerics Java, and Python, the "futuristic" languages like Haskell and O'Caml seemed to mainly offer additional static verification, and some other neat patterns, but the "bang for the buck" seemed somewhat low, especially since these languages have their own costs (they are much more complex, they rule out many "perfectly fine" programs). Ωmega seems like a true revolution to me  it shows what can be done with a really fancy typesystem, and this seems like the first astounding advancement over existing languages, from Python to Haskell. Its mantra is that it's possible to reap many (all?) benefits of dependent programming, without having to suffer its problems, by adding two much more humble notions to the widely understood, ordinary functional programming setting: GADTs + Extensible Kinds. Sheard and coworkers show that these two simple extensions allow the succinct expression of many dependentlytyped and related examples from the literature. Fine examples are implementations of AVL and redblack trees that are always balanced by construction  it's simply impossible to create an unbalanced tree; this is checked by the typesystem. It seems somewhat obvious that sooner than later all code will be written in this (or a similar) way. How to understand this stuff: my route was through the generics of Java and C# (especially Featherweight Generic Java, FGJ_{ω}, and A. Kennedy's generics papers). Once you understand basic notions like type constructors, variance, and kinds, you know everything to understand why GADTs + Extensible Kinds = Dependent Programming (and also esoteric stuff like polytypic values have polykinded types for that matter). It is my belief that you must understand Ωmega now! Even if you're never going to use it, or something like it, you'll still learn a whole lot about programming. Compared to Ωmega, other languages are puny. ;P By Manuel J. Simoni at 20100925 00:49  Fun  MetaProgramming  Paradigms  Type Theory  23 comments  other blogs  72017 reads
Type Classes as Objects and ImplicitsType Classes as Objects and Implicits
Martin Odersky and team's design decisions around how to do type classes in a unified OO and FP language continue to bear fascinating fruit. Implicits look less and less like "poor man's type classes," and more and more like an improvement upon type classes, in my opinion given a quick read of this paper. By Paul Snively at 20100804 22:25  Implementation  ObjectFunctional  Scala  Type Theory  50 comments  other blogs  29965 reads
An intuitionistic logic that proves Markov's principleâ€œAn intuitionistic logic that proves Markov's principleâ€, Hugo Herbelin, LICS 2010.
Markov's principle is an axiom of "Russian constructivism". It says that if P is a decidable predicate (i.e., the formula ∀x. P(x) or ¬P(x) is constructively provable), then if we know that P is not always false (ie ¬(∀x. ¬P(x))), then there exists an x such that P holds (ie ∃x. P(x)). One operational way of understanding this axiom is that it says is that if we know P is not always false (on, say, the natural numbers), we can find an element for which it is true with a whileloop: check to see if 1 is true, and then check to see if 2 is true, and so on, stopping when you hit a number for which it holds. This means that Markov's principle is a principle of unbounded search, and as a result it has controversial status in intuitionistic mathematics  should we regard a program with a nonconstructive termination proof as a constructively terminating program? (The answer is, as usual, "it depends": in different applications you can want it or not.) However, just chucking an axiom like ¬(∀x. ¬P(x)) → ∃x. P(x) into your proof rules is not very nice from a prooftheoretic perspective. It mixes up a bunch of different logical connectives, and adding it as an axiom will break things like the cutelimination theorem for sequent calculus. In this paper, Herbelin exploits (a) the fact that Markov's principle is a (mildly) classical principle of reasoning, and (b) the fact that classical logic is connected with control operators like continuations, to give a logic which is prooftheoretically wellbehaved, but which supports Markov's principle. The trick is to add firstclass continuations, but only for value types (ie, you can throw products and sums, but not functions). What I find surprising is that this same class of restriction also arises in another paper on control operators at LICS  Noam Zeilberger's paper "Polarity and the Logic of Delimited Continuations" uses it too. (This paper deserves a post here too.) Adding Type Constructor Parameterization to JavaVincent Cremet and Philippe Altherr: Adding Type Constructor Parameterization to Java, JOT vol. 7, no. 5.
FGJ_{Ï‰} is a simple extension of (Featherweight) Java's generics, where type parameters may be type constructors (functions from types to types). This very readable paper finally made me understand GADTs. (Previously: Generics of a Higher Kind on Scala's support for the same idea.) By Manuel J. Simoni at 20100524 20:49  Software Engineering  Type Theory  34 comments  other blogs  20255 reads
Objects to Unify Type Classes and GADTsObjects to Unify Type Classes and GADTs, by Bruno C. d. S. Oliveira and Martin Sulzmann:
A very interesting paper on generalizing and unifying type classes and GADTs. Classes are now firstclass values, resulting in a language that resembles a traditional, albeit more elegant, objectoriented language, and which supports a form of firstclass "lightweight modules". The language supports the traditional use of implicit type class dispatch, but also supports explicit dispatch, unlike Haskell. The authors suggest this could eliminate much of the duplication in the Haskell standard library of functions that take a type class or an explicit function, eg. insert/insertBy and sort/sortBy, although some syntactic sugar is needed to make this more concise. Classes are open to extension by default, although a class can also be explicitly specified as "sealed", in which case extension is forbidden and you can pattern match on the cases. Furthermore, GADTs can now also carry methods, thus introducing dispatch to algebraic types. This fusion does not itself solve the expression problem, though it does ease the burden through the firstclass support of both types of extension. You can see the Scala influences here. I found this paper via the Haskell subreddit, which also links to a set of slides. The authors acknowledge Scala as an influence, and as future work, suggest extensions like type families and to support more modulelike features, such as nesting and opaque types. By naasking at 20100222 21:51  Functional  ObjectFunctional  OOP  Theory  Type Theory  19 comments  other blogs  19579 reads

Browse archivesActive forum topics 
Recent comments
2 days 7 hours ago
3 days 8 hours ago
3 days 9 hours ago
3 days 9 hours ago
4 days 15 hours ago
4 days 16 hours ago
5 days 10 hours ago
5 days 12 hours ago
5 days 12 hours ago
6 days 4 hours ago