This is the calculus introduced in the "Safe Type-level Abstractions in Scala" paper, and also used in "Generics of a Higher Kind." When I read the latter paper I saw something confusing, and just today I re-read the earlier paper to confirm that it contains the same thing.

In the rules for type expansion (Figure 7 in the paper I linked above), in the X_SEL case, one of the premises is (excuse my attempt to format this with ASCII):

Gamma |- [x -> T]S << R


From what I understand, x is a term-level variable, and T is a type. How can that substitution work, then? Wouldn't the result be syntactically invalid?

I wouldn't be surprised if I am missing some detail in the paper, so if anybody with a better understanding could point me in the right direction, I'd appreciate it.

Edit:
Thinking about it a bit, it seems like the premise ought to be, instead:

Gamma, x : T |- S << R


Comment viewing options

Notation

In his overview of the theory the notation

[x â†’ T ]S

is explained as "(meta) substitution replace x .type by T in S." I can't seem to find that in the published paper, though, and if it's not then that's probably an oversight since it doesn't seem singleton types are common enough for that kind of notation to be assumed.

Thanks

That explains the intention. I'm still not entirely un-confused, though. It seems like x could occur in S in forms other than x.type. For example, you could have a path containing x.l.type.

If the substitution only replaces occurrences of x.type, then it would seem to leave some free xs around. If it manages to replace them all, then some auxiliary rules seem needed, to explain how it substitutes inside of paths.

I hope its clear that I'm not just trying to pick nits in the paper. My current research requires that I learn more about path-dependent types, and trying to understand the theory behind Scala seems like a good way to go about it.

I might be wrong, but

It seems like the type of p.l is covered by T_SELPATH.

It's still simpler to drop the notation...

Aside: Thank you for taking the time to help me with this. I appreciate it.

I agree 100% with (what I perceive to be) your intuition - the operation being described doesn't act so much like "substitution" as it does like a typing derivation.

It seems, though, that you can't just use the Term Classification rules to compute the "substitution" [x -> T] S. Not only is that hiding a lot of magic behind the syntax (e.g. what context do you use?), but it also has the problem that the Term Classification rules include subsumption.

As per my update to the original post, it seems that the right approach is to interpret the occurences of [x -> T]S in the paper as adding x:T to the left side of the turnstile.

Using my revised interpretation, the offending line in X_SEL would read:

Gamma, x : T |- S << R

The case that worried me in X_SEL was when S contains a type like x.l.type. With the expanded context, though, it is clear that X_SINGSEL and X_SINGVAR will apply.