Type safety and singletons
I am continuing to make progress on the proof of soundness for Featherweight Scala, but the most significant difficulty I am encountering involves the rule that allows paths, expressions of the form x.l1.l2...ln
, to be given singleton types:
Γ ⊦ p: T

Γ ⊦ p: p.type 
It seems to make any defining any sort of useful inversion principle impossible. For example, the term x.l1
where x
has a field val l1 : Int = 3
will reduce to 3
. In the proof of preservation, you would expect to be able to use inversion to show that if x.l1
is well typed with some type T
that x
has a field l1
with type T
, or at least some subtype of T
. However, with singletons it is possible that the type of x.l1
is x.l1.type
. In that case, the only thing you can determine by inversions is that x
has a field called l1
and it has some type. Many similar problems arise determining what would be seemingly straightforward facts because it is impossible to relate two types in a meaningful way.
There must be a resolution to the problem, because I know there are other type systems that allow singletons in this fashion, but I have not been able to hit upon the lemma to prove that will allow smoothing over the discontinuities singletons introduce. For now I think I will try proving safety with the above typing rule omitted, and see whether there are any other problematic features of the language.
Dan Licata said,
January 25, 2008 @ 4:42 pm
Hi Geoff,
I haven’t looked at the pathdependent types in Scala, but here’s what happens with singletons in ML: the problem isn’t so much the singleton introduction rule at the constructor level, but the elimination rule, which induces an equality (see StoneHarper for details). The reason is that you then have a nonsyntaxdirected constructor equality (notated C1 = C2 :: K), with a rule that says equal constructors are equal classifiers:
M : A A = B :: type
———————
M : B
This rule is a problem for type safety because now all of your inversion and canonical forms lemmas go out the window. About 2/3s of the Twelf formalization of the SML IL is devoted to solving this problem; i.e., to proving that int isn’t equal to bool. The way you do this is to give an alternate algorithmic version of equality for which the necessary inversions are obvious. An alternative is to define equality algorithmically to begin with, but then you often need to show that most of the declarative rules (e.g. transitivity) are admissible for your proofs anyway.
How does type equality work in Scala? Does a singleton induce an equality?
washburn said,
January 25, 2008 @ 4:52 pm
@Dan: Featherweight Scala does not presently have a notion of type equality, it just has type subsumption. I would hope that type equivalence can be defined in terms of type subsumption, but it would be a good idea to verify that it will truly form an equivalence relation.
As for singletons inducing equalities, I would assume you mean “are there type subsumption rules concerning singletons”? Yes, there are two rules and they are quite similar to the ones that can be found in section 2.2 of “A Type System for HigherOrder Modules”. The rules I am using currently can be found in some slides from a lecture Martin recently gave.
In any event, I believe I have found a solution based upon how singletons were handled in the νObj calculus. However, it will require changing the operational semantics from what is given in the paper A Core Calculus for Scala Type Checking.
Andrew said,
January 26, 2008 @ 3:04 am
That also reminds me of dot notation. Though I don’t remember how people usually avoid that problem there.
washburn said,
January 27, 2008 @ 4:16 pm
@Andrew: Thanks, I’ll check that out and see if there is something useful in that work.