Haskell has _three_ namespaces (?)

#1

Ref the DependentHaskell proposals to collapse together types and terms, consider …

data Labelled a = Label{unLabel :: a } deriving (Show, Eq)

xl = Label "xl"

foo unLabel = xl{unLabel = unLabel}

In the binding for foo, the unLabel to the right of = is a common-or-garden term variable. The unLabel to the left of embraced { ... = ... }:

  • is distinct from the term variable: there’s no confusion.
  • is distinct from the automatically-created accessor function unLabel :: Labelled a -> a – which is in termspace, and gets shadowed by the formal parameter to foo of the same name.
  • is declared in (brought into scope by) Label{unLabel :: a}.

So:

  • Which namespace is unLabel = ... in?
  • Is it a variable or a constant? (I suspect it’s a constant, but then why does it start lower case?) [:worried:] [ :upside_down_face:]
  • The Dependentistas want every name to have a unique quantification point. Then: where is that quantifier, and which quantifier is it?

[:worried:] To show that it’s a constant, and is distinct from the accessor function (which as of 9.2 can be suppressed), could we spell it Upper case?, with the field selector still lower case.

[:upside_down_face:] For comparison, Type Families/functions are not constants/constructors, but do start Upper case. So this is presumably to be consistently inconsistent (or do I mean inconsistently consistent?).

#2

This reminds me of Lisp1 vs. Lisp2 issue, and feels like an argument for less namespaces (or at least a clearly visible disambiguation).

I find the posted questions hard to understand. @AntC2 I wonder if you used machine translation? The artifacts like “common-or-garden”, “embraced” (cute pun?), “Dependentistas” and other peculiarities do take some mental effort to interpret.

#3

The syntactic separation is clear in my example, I don’t see that fewer namespaces would help:

  • following :: is in typespace.
  • in the decl Label{unLabel :: a }, Label outside the { ... } braces is in termspace; inside the { ... } embracing, to the left of :: is in labelspace, to the right of :: is in typespace.
  • in expression xl{unLabel = unLabel}, xl outside the { ... } is in termspace; inside the { ... } embracing, to the left of = is in labelspace, to the right of = is in termspace.

In the binding for foo unLabel = ..., foo is the function getting declared so has module-wide scope in termspace, unLabel is the formal parameter so has scope only to its right (and is therefore shadowing any module-wide unLabel. Haskell’s termspace has never distinguished functionspace vs variablespace as your linked Lisp proposal tries to (which seems a hangover from M-Lisp) – indeed that would be impossible in a language with higher-level functions.

common-or-garden

brace Noun sense 9 = Brit English ‘curly brackets’, Verb sense 8; ‘embracing’ compare ‘bracketing’ (‘bracing’ means something different).

‘Dependentistas’ links back to the first sentence – i.e. those embracing (Verb sense 2) this proposal, and a whole bunch of related design.

From what to what? (But the answer’s No.)

#4

This is a fair point in the sense that field assignments don’t fit into any of the namespaces, but I don’t think it’s fair to say that fields should fit into any namespace. Field assignments are syntactic sugar (for something not revealed otherwise in the language) and nothing else.

In order for the question " * Which namespace is unLabel = ... in?", it would have to be possible for the other namespaces to exist in the same context. However when I type:

foo = Bar { Baz = _ }

I get a syntax error at Bar because the field has to be a lower case. The proposal as I understand it separates namespaces for overloads at the term level. Since terms can clearly not be allowed on the left of the equals - your question doesn’t seem to affect the proposal as I understand it. For example:

Is it a variable or a constant?

Neither it’s a field assignment (I’m sure GHC maintainers have a term for this syntax but I don’t know it off-hand).

The Dependentistas want every name to have a unique quantification point. Then: where is that quantifier, and which quantifier is it?

I think this means that the introduction of a variable or type variable is uniquely observable (I’m sure your question is well-formed I’m just rusty rn). The field assignment language (separate from the term language) has one namespace: fields. I would assume they are bound by imports (implicitly or explicitly) or by the declaration of a datatype. Note that field assignments are not uniquely quantified as you might import same-named fields for different records.

Perhaps your question is an aesthetic one: should constants have one type of syntax versus another for variables? In that context I feel it’s a touchy issue. A pure language has a very loose separation of constant vs variable. Type constructors are just constant as fib is a constant. I think in general Haskell uses upper/lower to indicate “relating to types” more so than constant, but even that is fuzzy when considering type variables…

1 Like
#5

Thank you for clarifications - so it is my own comprehension and command of the language that were lacking, through no fault of yours.

You’ve mentioned “typespace”, “labelspace”, “termspace”.
The “termspace” is clear to me with foo and xl and other references to expressions.
The “typespace” presumably includes the capitalized types and classes e.g. Num, Int, Either
The 'labelspace" as demonstrated in the original example is confusing, I agree with @santiweight regarding syntactic sugar and I theorize that the left embraced unLabel is translated into something in “termspace”.

Now that I understand the observation, it does seem interesting to figure out how exactly it works under the hood, what namespaces there are and how are tokenized symbols handled in this situation.

#6

A couple of clarifications

In the o.p. Label (capitalised, data constructor) is in termspace.

Both typespace and termspace have both constructors (capitalized) and variables. It’s perhaps sloppy to call the capitalised thingies ‘constants’. The capitalized ones can appear in pattern matches – thinking of instance heads as typespace patterns.

But fib is different: it has local scope, it can be shadowed. Type and term variables can be shadowed. fib can’t be used to pattern match. (Or rather if you try, that’ll be taken as a fresh variable binding, shadowing the function decl.) Type constructors are necessarily at global scope, they can’t be shadowed. Data constructors are at global scope, they can’t be shadowed.

Labels (appearing syntactically in a label position) are at global scope, they can’t be shadowed. But the automatically-generated accessor function with the same name can be shadowed – as in the o.p. Labels can be pattern-matched on:

bar Label{ unLabel = label1 } Label{ unLabel = label2 } = ...

(More commonly you use punning, which is sugar for the above, but obscures the distinguishing syntax.)

That’s why it seems to me labels appearing in label position are more like constructors (they drive pattern matching) and should be capitalised. And should be distinguished from the accessor function, because that’s in a different namespace.

Oh, it’s revealed (in the Language Report) they’re sugar for positional access. This achieves the same as above:

bar (Label label1 ) (Label label2 ) = ...

which is happy if there’s only a single (or a few) fields.

You might import same-named type constructors or data constructors. Then Haskell means “uniquely quantified” up to qualified name/import prefix.

#7

@AntC2 if you want to find issues with Dependent Haskell-motivated namespace collapsing, I think a better smoking gun would be matchability capitalization, e.g.:

data t = c

c a = .... -- fun or pattern bind?

instane Foo (c a) -- what variables are bound?

There are not problems with current plans, IIRC, bu there are some residual philosophical kinks to work out.

#8

Thanks John, but I’ve done my dash with “find[ing] issues” there.

(In the back of my mind is: if field labels are more like constructors, could there be variables bound to labels? And what would that add to expressiveness? I think that would presume a language with anonymous records, like Purescript. And would need to continue the syntactic demaracation as to where labels can appear.)