Added conclusions

I've added a short conclusions section. See what you think and if you can fill in the missing citation.

Also, getting our names on this paper might be nice.

I've taken care of all the high-priority items left, I'm happy to have it turned in pretty much as-is if you have no further issues with my section. So I'm leaving it alone until you tell me something needs fixing.

--Carl

deltas to termpaper.*

Just so you know, I'll be making changes throughout the day today. I did some changes to Carl's section this morning; I'm probably going to focus on my section and the introduction for what remaining time I spend on this.

Please try to:

1. look at svn diff's
2. look at the log
3. finish your section
4. write a (smallish) conclusion.

Sometimes I'll be putting margin notes in (when I want to push a topic onto you to be sure it gets accounted for), but for the most part I'll be putting thoughts and commentary into the svn log. Since I may make changes to stuff in your area, its important that you sanity check those changes. Thus, svn diff, si vous plait!

I'll try to flesh out the introduction some more. But I'd like your feedback on whats already there. I'm trying to figure out how I would justify the study of type theory to the average algorithmicist, automata theoretician, or programmer.

tyeps, type constraint systems, strings, etc

I'll be checking in my notes shortly, but I figured that this wasn't going to fit into a margin...

In section 10.2, you discuss the correspondence between type constraint systems and non-deterministic finite automata.

It seemed from my reading that a type can be read as a (potentially infinite) tree, which in turn can be read as the set of strings that describe all paths from the root to the leaves of the tree. Thus, a type corresponds to a set of strings, or a single language.

In section 10.2, you say that there is a correspondence between type constraint systems and NFAs. But to me, a type constraint system describes not just one type, but rather a (potentially empty) set of types. Therefore, a type constraint system (TCS) corresponds to a set of languages, while an NFA corresponds to a single language.

Can you resolve this confusion for me (preferably by amending the paper with some sort of clarifying note)?

feedback

Okay, I spent an hour or so going back over the paper, trying to put special focus on the new additions on Recursive Subtype Constraint Entailment.

I was pretty happy with most of what I read (or maybe I'm just desparate to declare this thing finished), but I found myself going back over section 10.1 several times because I was confused by two things that looked like distinct conflicting "definitions" for the subtyping relation, <:

At one point, there is a line "The subtyping relation on T_Sigma is defined as follows. t <: t' iff ..."
and later there is the paragraph on Nonstructural subtyping which fixes Sigma = { \times, \to, \top, \bot } with latice ordering \bot <: \sigma, \sigma <: \top for all \sigma in \Sigma.

Did you mean to use the same "<:" in both places? Or are the second set of "<:"'s really analogous to the <:_B base type relation (or perhaps I should be calling it <:_\Sigma here)? I was confused by that, but ended up deciding that you must have not intended for the two notations to collide.

There are other changes to suggest, but they are merely suggestions or minor details, so I'll either make them directly myself or add "margin notes" for them.

Finished preliminaries on recursive subtyping.

I have finished writing up (and will momentarily commit) the preliminaries to the section on recursive subtype entailment - the next thing to be added will be the "meat" of the reduction from a PSPACE-complete problem. It bothers me to discover that the problem is established as PSPACE-complete in "personal communications" with the authors, but if they were willing to publish that then we can report it.

The "other" two systems presented in this paper are slight modifications on the original and based on the same reduction and automata equivalence. I think after presenting one it should be sufficient to merely mention the others, and get around to cleaning up the presentation and transitions in our papers. I should be able to finish the bulk of the material tomorrow (Tuesday), leaving us some time to polish it depending on when you want to hand in by.

Let me know what schedule works for you. I can put in more time tomorrow while other Santa Barbara folks are working if you're worried about pushing too close to the "end of the month" deadline, but I figured Thursday or Friday would be fine for submission.

--Carl

Moving on: Recursive subtyping

I began the recursive subtyping section with a motivation of and definition of constraint entailment, then began a description of the type system involved. Some of the definitions will be repeats of the foundations at the top of the paper - there's some overlap in the selftype section too. We can fix that up as we go, it's easier just to lay out what I want to say as I say it for now.

Felix, let me know if there's more work I need to be doing on selftypes first, but it looked technically complete enough to start work on the next paper.

--Carl

Tuesday work

I tightened up some of the explanations of the restrictions on grammars and the explanations about types and grammars. I also put in real ellipsis notations some places it was missing and changed the constraint forms figure to show grammar productions.

I'll be getting up early tomorrow morning to move my car, I'll put in an hour or two before work.

Starting cleanup

I very hastily closed off the technical discussion in my section, then went through and addressed all but one of our margin notes. The last margin note says things are very "hand-wavy", and they are. The next step will be to stop waving my hands and to point at some real details.

HUNGRY

felix hungry for blog entry!

seriously, if you're planning on having this thing done by the end of this weekend, i'd like to know where you are right now.

duelling theorists...

Jim and Palsberg add the syntax selftype, and deliberately choose to add this syntax, "rather than binding a name for selftype in each object type." They state that the desired meaning can always be recovered, because each occurrence of selftype comes with its context.

This bothers me, because of the following example: in Jim and Palsberg's system, what is the meaning of the type expression [makeref : [ref : selftype]] ?

I see two possible (informal) interpretations of the above type expression: either selftype represents some subtype of the entire type expression, or it represents some subtype of the type subexpression [ref : selftype] alone. I'm guessing that the former interpretation is correct, but I have not taken the time to go through the rules to verify this.

Assuming one of these interpretations is correct, is there a way to express the other interpretation? Or is this a useless goal? It seems to me that if we were to actually bind some name to each selftype for the type subexpressions, then we could unambiguously express either option.

Reduction to type inference; end of month plans

I've begun the section on type inference after going over it in the paper.

My plans to visit Santa Barbara have moved up from the 4th of July week to a week earlier; I'll be flying out on the 24th. This limits our time to work, so I plan to finish up the "first draft" phase of writing by the end of this weekend - whatever it takes - and then spend the rest of the following week on filling in details and touching up presentation.

If you want to meet to do some of the weekend work we can do that.

Morning productivity

I've added the definition of the constraint variables and constraint system for a boolean formula, and a rough sketch of the equivalence between SAT solutions and CS solutions of these systems. More detail needs to be added, but it's a beginning.

I think I'll try to do more morning work from now on, the afternoons in this heat are exhausting.

varsigma : lambda :: ___ : arrow

(figured I'd have put this question here, since its something that we may go back and forth on, and the latex document is not for that)

This is regarding the following interaction:

\fmarnote{What/where is some arrow type $\leadsto$ such that
  $\varsigma$:$\lambda$::$\leadsto$:$\to$?  It seems it may be $[l_i : B_i]$,
  since label reference \emph{is} invocation.  If true, we may do well to
  explicitly point this out.}

\cmarnote{What the heck are you talking about?  I don't understand this at all.}

My point was this: in the type systems for the lambda calculus, there is the very important type constructor, arrow, which is the essence of how we abstract over the behavior of an actual term, by describing it as belong to a "function space." So that's what the arrow type constructor is for.

My question was, what is the corresponding essential type constructor in Jim and Palsberg system? The object language doesn't have the same sort of beta reduction that we're used to seeing (its there, sort of, its just hidden). So it wasn't immediately clear to me what the corresponding type constructor was.

My current hypothesis is that $[l_i : B_i]$ is the type I'm looking for; this describes an object which, when asked for the result of its l_i method, will return an object of type B_i. But this is only a hypothesis, and while it makes things clearer for me, you're the one writing this section, so I thought I'd ask you about it (and suggest that you add some sort of explanation along these lines, so that the reader can use their knowledge of the lambda calculus as leverage in understanding the varsigma calculus).

If you think such an analogy hurts more than it helps, that is fine. It was just a stray thought I had while on the plane, and it took me long enough to come up with an answer I was happy with that I thought I should bring it up.

understanding object calculi

So, Abadi and Cardelli came up with an object calculus.

b ::= x 
   | [ l = \varsigma (x) b ... ] 
   | a.l 
   | (a.l <= \varsigma (x) b)

When I was digesting this, at some point I wondered, "is the fourth production just sugar for the second?" And I played around with it and decided, "no, its not just sugar, because at the point of update, we don't know all of the implementations that our self might be currently carrying. So this is a fundamental operation; it is not macro-expressible in terms of the other forms in the language."

However, this led me to consider the other direction: "is the second production just sugar for the fourth?" This is obviously false; without the second production, we'd have no base case capable of defining a closed term, and we'd be screwed. BUT, there is a much simpler formuation, where you predefine a constant Useless which dies on any attempt to use any of its methods (and it has every method in our label set defined). Then, it seems to me that we could define the second production in terms of the fourth production and Useless. Why didn't they go down this route, which would appear to simplify things?

If you're not happy about having an object that is magic (in that it has every method "implemented", though the implementation seems to match exactly what Abadi and Cardelli's model would have done in such situations), then instead we could not use Useless, but instead simplify the second production to [l_1 ... l_n], and now this defines an object which has l_1 through l_n predefined with some default implementation (like returning self). Again, this seems like it would simplify the calculus, since there's now really only that fourth production in the grammar where all the power is lurking.

But maybe I'm crazy.

Boolean Encodings

Added section on boolean encodings.

Ugh, it's hot. Fucking lack of air conditioning.

Core selftype constraints defined.

I've added the definitions of the constraints now.

My projected timeline for this weekend through the next:

This weekend: finish writing the sections I've read so far.
Saturday - kill off boolean encodings, start the next reduction.
Sunday - finish reduction from SAT to CS constraints.

Next week: read up on the next reduction, fill it in.

Next weekend: start reading up on next paper (recursive subtyping).

Comments welcome as always.

--Carl

Type rules added

I've added the type rules to the paper.

Picking up where I left off.

I finished writing the outline (in the tex file) for the section I have absorbed; this is most of the selftypes paper. I have copied over the introductory writeup I did before and touched up the presentation to be a little less formal and a little clearer.

Let me know how it looks.

Today was a short day because of kung fu practice. Tomorrow will be longer.

Transitioning to write-up

I finished my workup of a mock example and partially verified its correctness (it is very formulaic, I have little doubt the rest follows suit). I have started considering what intuitions to present and have begun work in the actual TeX file. Real writeup can begin soon; I should be able to get 1/2 to 2/3 of the selftypes writeup done without reverting to reading mode. Hopefully I can also get an outline of the rest of that section done and simply fill in details from the paper; we'll see how comprehensible the final section is.

Conceptual progress

Today's exercise: (starting) work on an example formula to grind through the constraint/SAT solution. After writing out lots of tedious copy-paste formulae by hand (I thought pencil/paper would let me "play with" the constraint system more directly, and once I'm done writing things out it might, but ugh...), I've come to the following conclusion (writing by hand may not have been a bad idea, tedious writing means lots of time to just stare and ponder):

The type constraints use types with no GLB to express boolean incompatibility - a boolean variable may not be T and F; a type variable may not have an upper bound of both [m : []] and [m : [m : []]]. Selftypes and the context operator are used for conditional - if a variable U is selftype, then U{V} becomes V; otherwise it stays as U. Chains of subtype relations are setup with U{V} (for various Us and Vs) at each intermediate step, terminating in various incompatible upper bounds. The variable constrained at the bottom is given one upper bound or the other depending on which intervening U variables are assigned to selftype in the constraint solution. Hence, selftype corresponds to falsehood and all other types to truth in the correspondence between SAT and the core selftype constraints. (Choice of falsehood vs truth is most likely just convenience.)

This still does not provide the solution to SAT, but does demonstrate the underlying correspondence between the type system and this NP-complete problem: both the type system and SAT formulae have underlying notions of conditionals and mutual exclusion, and not enough power to express much else.

More tomorrow. Nothing checked into SVN tonight, the above conclusions are my work-product.

Weekend 1

Difficulty motivating myself to delve into the details. I must find a better approach, or else Felix will invest in a cattle prod. I don't know if I want to have to explain scorch marks to my manager at Sun. "It's nothing. I walked into a door. An... electric door."

Worked out some more intuition into CS (core selftype) systems of constraints. The "context" construct in types (B{A} = A if B=selftype, B{A} = B otherwise) is used as conditional, so U_x <= VA_x if x = true, and U_x <= VB_x if x = false. These types are made incompatible; there is no T such that T <= VA_x and T <= VB_x. Constraint solutions for true and false are given, then used to construct a CS-solution from a SAT-solution for boolean formulae. Because false maps to selftype and true maps to record types, the reverse mapping is trivial (selftype |-> false; anything other type T |-> true).

ADDENDUM:
I wrote this Sunday night, but apparently forgot to hit Publish Post, so this is going up Monday night.
I am currently starting on my Monday work.

Day 2

Made progress on outline.
Mostly, made progress on understanding the proof. I had only the idea behind the proof of NP-completeness before, working now on details. A few points are questionable:
1) A couple of sections end with "it is straightforward..." I shall have to figure out this "straightforward" conclusion to be able to present it. I suspect that absorbing the correlation between constraints and boolean formulas will give this intuition.
2) The translation from constraints to inference relies on different variables of the same name always having the same type. I suspect this is valid in their presentation but a huge liability of their type system. It will be interesting to see if removing this restriction makes type inference easier or harder, but probably that conclusion is way outside our scope.

This weekend I should be able to pick up the pace on working this out, but I put in a solid hour on this tonight.

--Carl

Houston, we have achieved SVN COMMIT

Okay, I've committed my "night's work" - a brief outline of what I intend to put in the paper. There's more detail in the Selftypes section (vs the recursive subtyping section) because I've started writing that part up already. After fleshing out the outline more I will work on moving my TeX work into the existing files. (We should make sure the .tex files are checked in as non-binary so changes will get merged intelligently.)

TO DO on the outline:
- Felix, you can add anything for your unwritten sections that you want outlined. Heck, written sections too, but that's more obvious.
- Remove or cut down sections on upper bounds (algorithms)
- Flesh out second section

svn repository is up

I've put the LaTeX, BibTeX, and a Makefile for my draft into a shared space for Carl and I to work from.

Woot.

For grins, here is the contents of the Makefile:

termpaper.dvi: termpaper.tex termpaper.bib
        latex termpaper.tex
        bibtex termpaper
        latex termpaper.tex
        latex termpaper.tex

You see any problems with that? I bet there are some, but I don't know the right way to make make work with LaTeX.

First post!

I feel like I'm on slashdot.

i am eagerly awaiting Carl's first diary entry.