Lawyering the Lexical Scoping Principle

Learn
1

GHC Proposal 378 (Design for Dependent Types) and other related proposals have been referring to the ‘Lexical Scoping Principle’, defined as:

Lexical Scoping Principle (LSP). For every occurrence of an identifier, it is possible to uniquely identify its binding site, without involving the type system.

378 goes on to describe how this interacts with punning, and the places where types and terms are expected to appear. In type and class declarations, after :: in signatures, after @ in visible type applications, and after the type explicit namespace marker, names are first looked up in the type namespace, and then the term namespace; elsewhere, the term namespace has priority. The LSP comes into play with language features like visible forall, where the type system would need to be involved in order to resolve names in the forall argument from the type namespace first, since that is not one of those four type-syntax locations.

So, for example, this is an error:

{-# LANGUAGE RequiredTypeArguments #-}

import GHC.Exts (List)

newtype Age = Age Int

foo :: forall a -> List a
foo _ = []

bar :: List Age
bar = foo Age

The type checker expects the Age in foo Age to get an argument, because the name Age was resolved to the data constructor and not the type. The fix is foo (type Age), and this is sadly necessary to comply with the LSP. (foo Int would have been fine, because Int is not punned.)

All that is prelude. My question is, does the LSP preclude GHC from being smarter about switching into type syntax based purely on the namespace in which other names are found?

For example:

bar :: List (Maybe Age)
bar = foo (Maybe Age)

This is also an error. But would GHC be allowed to do better, by noticing that Maybe resolves to a name in the type namespace, and so its argument can be interpreted under type-syntax rules? That’s not involving the type system, right? Would that be undesirable for other reasons on the DH roadmap? (Presumably, the current system favors DH programs that interleave types and terms frequently, while the rule I’m considering would favor DH programs in which types and terms tend to stick together. Right now, due to the lack of true dependent types, the latter are necessarily much more common; will they still predominate in the DH future, do we think?)

3 Likes
2

switching into type syntax based purely on the namespace in which other names are found?

To answer your question directly: this would be conformant with the LSP.

A separate point to address is whether “smarter” equals “better” here. I generally lean towards “stupid” being “better” in such cases, because it is more predictable.

For example, should your rule apply in the opposite direction with DataKinds? E.g. in

type T = Just Age

would you expect Age to refer to the data constructor because it’s an argument of Just?

1 Like
3

That’s a good point; DataKinds has certainly trained me to think that I’d need to quote both Age and Just if I wanted them both to be promoted values. And if I want [1, 2, 3] to be a type-level (promoted) list of type-level naturals (‘punned’ with term-level Num as?), I wouldn’t want to have to mark each of 1, 2, and 3 as ‘demoted’ somehow.

On the other hand, if DH advances to the point where we can use general terms in types, and foo is a term-level function, I do think I’d expect foo Ctor to prefer pulling Ctor from the term namespace, even if foo Ctor is a term that appears in types. But maybe the way that ends up working is that the way to embed foo Ctor in a type is using an explicit namespace sigil dual to type, like type T a = Vec (data (foo Ctor)) a, and then at least it’s symmetrical, if clunky. Maybe I’d get used to it.