Linkdump

I'm working on a Ninjas/Nazis/Bavarian Illuminati/Aliens/Werewolves* movie, so I don't have as much time for PL geekery atm. Here are some interesting links I haven't checked out fully yet.

▶ Nested Refinements: A Logic For Duck Typing (via @swannodette)

Programs written in dynamic languages make heavy use of features — run-time type tests, value-indexed dictionaries, polymorphism, and higher-order functions — that are beyond the reach of type systems that employ either purely syntactic or purely semantic reasoning. We present a core calculus, System D, that merges these two modes of reasoning into a single powerful mechanism of nested re- finement types wherein the typing relation is itself a predicate in the refinement logic. System D coordinates SMT-based logical implication and syntactic subtyping to automatically typecheck sophisticated dynamic language programs. By coupling nested refinements with McCarthy’s theory of finite maps, System D can precisely reason about the interaction of higher-order functions, polymorphism, and dictionaries. The addition of type predicates to the refinement logic creates a circularity that leads to unique technical challenges in the metatheory, which we solve with a novel stratification approach that we use to prove the soundness of System D.

(See also The Shadow Superpower: the $10 trillion global black market is the world's fastest growing economy: "System D is a slang phrase pirated from French-speaking Africa and the Caribbean. The French have a word that they often use to describe particularly effective and motivated people. They call them débrouillards. To say a man is a débrouillard is to tell people how resourceful and ingenious he is.")

▶ Dart Talk @ Stanford (I think this is by Bracha. Haven't checked it out coz it's in some weird Windows format.)

▶ Things SQL needs: MERGE JOIN that would seek (Nice idea about using histograms to speed up index scans. I believe the new App Engine query planner does that or something similar. Also Understanding Histograms in Oracle.)

▶ I'm a big fan of the tagless-final approach! (This comment caught my interest, because it reminds me of Kernel: "everything in the language has to become both directly interpretable and available as an AST".)

▶ New extension to Haskell -- data types and polymorphism at the type level (Ωmega-like.)

▶ Evolution of DDD: CQRS and Event Sourcing (@dyokomizo hyped this weird-sounding stuff in response to Beating the CAP theorem).

(* As Rob Zombie says: "I feel that the Nazi movie is back. Once the trend comes back, the Nazi trends comes back, now you pervert it like crazy and you add werewolves. So, I don't know if we'll ever see that movie, but now is the time. The time is now to strike with this.")