Home » forums » LtU Forum

Question about the Scalina calculus

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

By Tess Foley at 2009-12-16 05:23 | LtU Forum | previous forum topic | next forum topic | other blogs | 3895 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

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.

By James Iry at Wed, 2009-12-16 16:28 | login or register to post comments

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.

By Tess Foley at Wed, 2009-12-16 17:18 | login or register to post comments

I might be wrong, but

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

By James Iry at Thu, 2009-12-17 23:19 | login or register to post comments

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.

By Tess Foley at Fri, 2009-12-18 17:17 | login or register to post comments