November 2011
1 post
2 tags
Social intuitionistic logic
Does anyone know of any efforts to develop a form of intuitionism wherein “proof” is actually a trust network that establishes, under some threshold, the truth of a proposition? I suppose such a system would resemble access control logics, where $p~\mathsf{says}~\phi$ is a formula meaning that principal $p$ has stipulated the truth of formula $\phi$. In my head, a proof term is now an...
October 2011
2 posts
3 tags
Module identity in modular packages
Update at the bottom!
In the last post I described Haskell’s current, limited notion of module identity. (It was none too exciting.) Now I’ll expand on that notion in our new package language. With a richer, more careful semantics of identity, we grant packages with the power of generic reusability!
This post builds on the examples of the last, so I suggest a quick refresher. For...
2 tags
Module identity and equivalence in Haskell
In first-order module languages such as Haskell’s, the identity of a module is given solely by its programmer-written name, e.g. Http. When dealing with packages, the identity is augmented with that of its defining package, e.g. httplib-4.1:Http. These names induce a straightforward equivalence relation on modules: modules P1:M1 and P2:M2 are equivalent iff P1=P2 and M1=M2.
Why does module...
August 2011
1 post
3 tags
A modular package language for Haskell
What’s the difference between a “package” and a “module”? Though modules have evolved beyond their low-level origins into richly composable, type-based abstractions, packages are largely stuck in a Linux-like land of version ranges and imprecise specifications.
How can we bring packages up to speed with contemporary module systems? For my first big project,...
May 2011
1 post
4 tags
Toward a categorical interpretation of extensible...
Ben Delaware is thinking about mixin modules for Coq as a means of modularly extending data types, theorems, and proofs. (This is a dramatic departure from the mixin modules of (Dreyer and Rossberg, 2008), where (inductive data) types may not be extended once defined. In MixML two type exports only link together if one is a subtype of the other, according to some notion of core subtyping.)
...
April 2011
2 posts
1 tag
Aside: Explicit rule for `let` in MixML
In MixML $\mathtt{let}$ binding of one module inside another is defined as syntactic sugar:
This definition highlights the minimalism of MixML (along with other definitions): one can express the entire ML module system in it. Unfortunately, the compactness of the language can hinder one’s understanding of these “macro-expressible” constructs. For my own benefit I wrote out the...
2 tags
Principal types and impredicativity
In the last post I discussed the ambiguity and incompleteness of the Hindley-Milner type system with type classes. I also mentioned that I would follow it up with an idea I was pursuing, which, as it turns out, I’m no longer pursuing. This time I’ll motivate the idea by explaining why I was led to it in the first place. The last post describes, really, the post hoc motivation for it,...
March 2011
1 post
2 tags
Hindley-Milner, principal types, and type classes
Update: Now using MathJax to render mathy things nicely.
$\newcommand{\int}{\mathrm{int}}\newcommand{\bool}{\mathrm{bool}}\newcommand{\string}{\mathrm{string}}$In this post I provide background information on an idea that I’ll explain in the next post. People familiar with Hindley-Milner and type classes won’t get much out of this, except maybe the last part.
Hindley-Milner: the...
February 2011
5 posts
1 tag
Peter Aczel. An Introduction to Inductive... →
Fritz mentioned referred to this as a primer on inductive definitions, inference rules, and the like. I had seen it before but passed it up as too dense; now that I’m reading it, I like Aczel’s presentation. Although the low exposition-to-definition ratio reminds me of my old real analysis textbook.
Sorry for the ScienceDirect link.
EDIT: Oy, okay, my brain can’t handle...
1 tag
On understanding "coinduction" rules
Thanks again to Aaron for correcting a misconception I had about the (perhaps most general) principle of coinduction in the comments of the last post. He pointed out that a mixture of inductive and coinductive rules in an inference system gives rise to mixed fixed points, which come up in the mu calculus, for example.
At this point, though, I am ready to retire my pursuit.
It all started with...
1 tag
Paperlog: Coinduction and FP
Andrew D. Gordon. A Tutorial on Co-induction and Functional Programming, 1994. (@MSR)
* * *
Aaron Turon recommended this paper in the comments of the last post.
Gordon briefly defines coinduction as a proof principle using greatest fixpoints of monotonic functions — the usual thang — and then builds up a small call-by-name functional language. Divergence is defined coinductively and...
1 tag
Paperlog: Coinduction
Jacobs and Rutten. A Tutorial on (Co)Algebras and (Co)Induction, 1997. (pdf)
* * *
I’ve been trying to brush up on my knowledge of coinduction (in the general sense). In the last paper, the authors make use of a coinductively interpreted inference rule to do some magic with fixed points and recursion. Not knowing what the hell that meant, I needed some background.
This paper, loaded with...
1 tag
Paperlog (POPL'11)
Henglein and Nielsen. Regular expression containment: coinductive axiomatization and computational interpretation, POPL 2011. (ACM)
* * *
Primarily, I like this paper as further elucidation of the propositions-as-types principle. They didn’t originate the idea of regexps as types, but they did connect terms of those types to the parse trees (i.e. proofs) that form various strings in a...
January 2011
1 post
1 tag
Compile LaTeX source without the trash
When compiling LaTeX documents pdflatex generates .aux and .log files in the process of generating the output .pdf. These auxiliary files are only mildly annoying, but when writing a LaTeX document in a Dropbox-synced directory, those files are synchronized every time you compile — what was mildly annoying becomes wasteful garbage. Since currently Dropbox does not support file exclusion,...
August 2010
1 post
1 tag
Programming in Standard ML: Day One
As my first concrete assignment at the Max Planck Institute for Software Systems, I am implementing the F-ing modules translation in SML/NJ. The point is the means, not the ends: I’ve never really programmed with modules before, so this will learn me a thing or two.
There’s no data structure for a mapping in the standard Basis library? Not even association lists?! What the hell kind...
April 2010
2 posts
1 tag
POPL?
POPL 2011 convenes in Austin next January: we must get a Fortress paper in. The PLRG team has been itching to get something into POPL, and apparently there is outside interest in such work. Eric is convinced that our work on generic overloading — primarily from last summer — is novel enough for a submission, which means we’re in crunch mode for a few months to hammer out the...
Grad school part deux
Since my last post I’ve accepted the offer to join the doctoral program at the Max Planck Institute for Software Systems with Derek Dreyer. I’ll be starting there around August of this year.
February 2010
1 post
2 tags
Reading list
As per William’s suggestion, reading through Felleisen’s “On the expressive power of programming languages” (1991) to help me understand how to compare metaclasses and type classes.
Otherwise, lately I have been thinking of what the core subject of my thesis should be. I think I will do a few things:
Slightly extend Eric’s MCJ to support some kind of conditional...
January 2010
3 posts
2 tags
A theory of metaclasses
The past few days I have began thinking about metaclasses from a type-theoretic perspective. What is a metaclass? Is it a type? Is it a kind? Is it both at once? I hope to get a handle on this soon. Maybe this would make a more riveting master’s thesis than extending Fortress with metaclasses and showing the type class behavior.
1 tag
An issue with my v1 proposal
A static type parameter T of the form `T extends U` can be instantiated with an intersection, union, arrow, or tuple type. The variable T ranges over all different types that are subtypes of U. We hope that if T is a static type parameter of some function then the arguments and context of a call to that function uniquely determine the actual type for T (statically).
However, if T is a static type...
1 tag
Fortress with metatraits, v1 →
(The title of this post is also the link to the file.)
Very first draft of a quick explanation of my extension to Fortress, with examples. For the uninitiated, I’m extending Fortress to support metaclasses in order to express certain structures and operations more like Haskell type classes. Hopefully this serves as a decent solution to the binary method problem (all our binary operations...
December 2009
1 post
3 tags
Type inference for GADTs, and for Fortress?
I downloaded this a while back but just now getting to it: Tom Schrijvers, Simon Peyton-Jones, et al. Complete and decidable type inference for GADTs, ICFP 2009. I’m trying to think of ways to adapt their type inference algorithm for GADTs for use in Fortress. Their handling of implication constraints for type inference seems analogous to our problem of incorporating type inference and...
November 2009
3 posts
2 tags
Subtype + type inference + parametric polymorphism...
I’ve generally been a big fan of Fortress’ multiple dynamic dispatch. Although it complicates overloading, it provides a lot of room for specialization through polymorphism that is unseen in just about every other OO language. This summer, when Justin and I were coming up with the semantics for overloading generic and non-generic functions, we punted on the issues that arise from...
Google's Go language
Consensus among Fortress team: eh. Looks like a nice replacement for systems programmers who don’t need pointer arithmetic. I definitely dig their interfaces.
3 tags
Some early-morning thoughts on Fortress Skype chat
These came as a result of reading through Cardelli and Wegner. On understanding types, data abstraction, and polymorphism. (1985) and Cook. On Understanding Data Abstraction, Revisited. (2009).
I’m starting to realize how much we are blending the notions of ADTs and objects by virtue of functional methods
What Cardelli and Wegner call “inclusion polymorphism,” that gotten from...
October 2009
3 posts
1 tag
Traits paper
Was nice to see a formal explanation of traits. My complete ignorance of Smalltalk made a lot of the examples and usages hard to follow. There’s also some mention of metaclasses that might come in handy.
As they admit at the end, a static type system makes them a lot harder to deal with, so some of the simple treatment here was frustrating. For example, how would you abstract over all the...
2 tags
Max Planck and modular type classes
In my search for Ph.D. programs I came upon (via everybody’s favorite Italian, Lorenzo Alvisi) the Type Systems and Functional Programming group at the newish Max Planck Institute for Software Systems in Saarbruecken, Germany. The web page for Derek Dreyer, the head of that group, was particularly revealing:
[ … ] I showed how to extend ML with support for overloading and ad hoc...
1 tag
Ducasse et al. "Traits: A mechanism for... →
Finally reading this to better understand the concept of a trait, rather than shaping it into whatever is convenient for my work.
September 2009
10 posts
1 tag
Abstraction ideas, cont'd
Fortress imposes a restriction on abstraction that’s a sizable departure from the OO type system in Java: Objects, the only “classes” with actual data, cannot be extended. That is, in Fortress, every class that contains an actual structural representation is like a final class in Java.
Here’s where this could go wrong: Say I wrote some library code that involved the...
3 tags
Monoid and List example code →
Code for interface Monoid, trait List, trait ConsList, object Cons, object Nil, and object ArrayList. Some sample application code that involves solving implementation constraints at the bottom. http://dl.getdropbox.com/u/386692/thesis/monoid_list.txt
2 tags
Abstraction ideas
An interface I is a definable abstraction over an entire class of further, orthogonal abstractions. In general, two different implementations T1 and T2 of an interface I are completely unrelated; notably, one is not substitutable for the other. It describes operations and fields on each kind of implementing structure T that must be provided by such a T. The operations and fields supported by a T...
4 tags
Numeric hierarchy
My current concrete task is to investigate the use cases of the numeric hierarchy of Fortress. My motivation thus far has been the use of trait declarations like `trait Eq[\T extends Eq[\T\]\]` — a pretty broad concern since this pattern is used throughout the libraries.
All along the way though, this has been tied very closely to the numeric hierarchy since Num is another trait defined...
3 tags
On interfaces
In Java, interfaces differ from classes primarily in a lack of inheritance: declarations are “inherited” but not in the same sense that methods are inherited between classes. Interface implementation is a matter of concern only to the Java type system, whereas with class inheritance the runtime environment needs to be aware of the inherited methods. This leads to the extra dimension of...
1 tag
Just had a thought: Fortress APIs and components are like abstract data types (ADTs). The API is the signature of the ADT and the component is the representation. You can’t access anything about an ADTs representation (component); you are restricted to using its signature (API).
3 tags
Expression problem thoughts
Today in our reading group we discussed William’s essay “On Understanding Data Abstraction, Revisited” (2009) and Odersky’s “Independently Extensible Solutions to the Expression Problem” (2005). Both papers discuss the expression problem to an extent, which is also a key subject of my research.
In his paper, Odersky gives a solution to the expression problem in...
What good have proofs ever done anyway?
Gonna stop reading through Mark P. Jones’ “Qualified types” cover to cover. From now on, I’ll read only the more applications-oriented sections that might bear more relevance on my thesis. After all, my research is more about design and implementation than theory, which is what MPJ emphasizes in his dissertation.
2 tags
Fortress: Coercion lifting
UPDATE AT BOTTOM!
The following is a pretty long post detailing my proposal for dealing with user-defined coercions in Fortress. It has nothing to do with my research really, but it sure took a long time to type up!
During disambiguation of any compilation unit, if there is a trait Foo[\T\] with a coercion declared as `coercion[\U\](…)`, create a new top-level function `coerce_Foo[\T,...
Hello World
Writing my research updates on here now, as Twitter’s 140 character limit was really killing my soul.