User loginNavigation |
ParadigmsDependently-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 | 18305 reads
Simple Generators v. Lazy EvaluationOleg Kiselyov, Simon Peyton-Jones and Amr Sabry: Simple Generators:
This is fascinating work that shows how to gain the benefits of lazy evaluation - decoupling of producers, transformers, and consumers of data, and producing only as much data as needed - in a strict, effectful setting that works well with resources that need to be disposed of once computation is done, e.g. file handles. The basic idea is that of Common Lisp signal handling: use a hierarchical, dynamically-scoped chain of handler procedures, which get called - on the stack, without unwinding it - to parameterize code. In this case, the producer code (which e.g. reads a file character by character) is the parameterized code: every time data (a character) is produced, it calls the dynamically innermost handler procedure with the data (it yields the data to the handler). This handler is the data consumer (it could e.g. print the received character to the console). Through dynamic scoping, each handler may also have a super-handler, to which it may yield data. In this way, data flows containing multiple transformers can be composed. I especially like the OCaml version of the code, which is just a page of code, implementing a dynamically-scoped chain of handlers. After that we can already write map and fold in this framework (fold using a loop and a state cell, notably.) There's more sample code. This also ties in with mainstream yield. By Manuel J. Simoni at 2013-02-21 13:30 | Fun | Paradigms | Software Engineering | 10 comments | other blogs | 26258 reads
Tiny Transactions on Computer Science
This is an interesting idea: CS papers whose body fits in 140 characters - the abstract may be longer, watering the concept down a bit. What does focusing tell us about language design?A blog post about Call-By-Push-Value by Rob Simmons: What does focusing tell us about language design?
Previously on Rob's blog: Embracing and extending the Levy language; on LtU: Call by push-value, Levy: a Toy Call-by-Push-Value Language. And let me also repeat CBPV's slogan, which is one of the finest in PL advocacy: Once the fine structure has been exposed, why ignore it? By Manuel J. Simoni at 2012-03-05 15:17 | Functional | OOP | Paradigms | 24 comments | other blogs | 17562 reads
Adding Delimited and Composable Control to a Production Programming EnvironmentAdding Delimited and Composable Control to a Production Programming Environment (add'l material), Matthew Flatt, Gang Yu, Robert Bruce Findler, Matthias Felleisen, ICFP 2007.
Another tour de force by the PLT folks. Does your language have delimited control, delimited dynamic binding, and exceptions? It's the new gold standard, and so far only Racket and O'Caml qualify (and maybe Haskell and Scala?) Racket's implementation is additionally interesting because it achieves backwards compatibility with code written using undelimited call/cc and dynamic-wind. The authors mention that a simpler solution would be possible without this compatibility - based on control filters from the Subcontinuations paper. By Manuel J. Simoni at 2012-03-02 19:09 | Implementation | Paradigms | 36 comments | other blogs | 13107 reads
Programming as collaborative referenceProgramming as collaborative reference (extended abstract and slides) by everybody's favorite PLT tag team, Oleg and Chung-chieh, from the Off-the-beaten track workshop affiliated with POPL 2012:
By Manuel J. Simoni at 2012-02-04 16:48 | Paradigms | Type Theory | 12 comments | other blogs | 11230 reads
A Semantic Model for Graphical User InterfacesNick Benton and Neel Krishnaswami, ICFP'11, A Semantic Model for Graphical User Interfaces:
This is an application of their (more squiggly) LICS'11 submission, Ultrametric Semantics of Reactive Programs. In both these cases, I find appealing the fact the semantic model led to a type system and a language that was tricky to find. By Ohad Kammar at 2011-09-10 20:25 | DSL | Fun | Functional | Paradigms | Semantics | Theory | 5 comments | other blogs | 16621 reads
Levy: a Toy Call-by-Push-Value LanguageAndrej Bauer's blog contains the PL Zoo project. In particular, the Levy language, a toy implementation of Paul Levy's CBPV in OCaml. If you're curious about CBPV, this implementation might be a nice accompaniment to the book, or simply a hands on way to check it out. It looks like an implementation of CBPV without sum and product types, with complex values, and without effects. I guess a more hands-on way to get to grips with CBPV would be to implement any of these missing features. The posts are are 3 years old, but I've only just noticed them. The PL Zoo project was briefly mentioned here. By Ohad Kammar at 2011-07-14 18:57 | Fun | Functional | Implementation | Lambda Calculus | Paradigms | Semantics | Teaching & Learning | Theory | 4 comments | other blogs | 33989 reads
Type-checking Modular Multiple Dispatch with Parametric Polymorphism and Multiple InheritanceType-checking 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, type-checking, 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 2011-03-20 16:28 | Paradigms | Type Theory | 6 comments | other blogs | 12361 reads
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, pre-generics 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 dependently-typed and related examples from the literature. Fine examples are implementations of AVL and red-black trees that are always balanced by construction - it's simply impossible to create an unbalanced tree; this is checked by the type-system. 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 2010-09-25 00:49 | Fun | Meta-Programming | Paradigms | Type Theory | 23 comments | other blogs | 85463 reads
|
Browse archives
Active forum topics |
Recent comments
12 weeks 1 day ago
12 weeks 1 day ago
12 weeks 1 day ago
34 weeks 2 days ago
38 weeks 4 days ago
40 weeks 2 days ago
40 weeks 2 days ago
42 weeks 6 days ago
47 weeks 4 days ago
47 weeks 4 days ago