[Haskell-cafe] Capitalization and associated type families

[Jonathan Cast]

On Mon, 2008-08-04 at 23:04 +0100, Brian Hulley wrote:
> Jonathan Cast wrote:
> > On Mon, 2008-08-04 at 19:51 +0100, Brian Hulley wrote:
> >> For example, why is there any distinction between a type "variable" and 
> >> a type "constant"?
> >>
> >> 	forall a b. (a -> b) -> List a -> List b
> >>
> >> Now this begs the question: why does "List" need to start with a 
> >> capital? (supposing that quantifiers were always written explicitly)
> > 
> > AFAIK, it doesn't; the variable/constant distinction is just there to
> > let the implementation put the foralls in for you.
> 
> Hi Jonathan - thanks - this confirms what I've been thinking. However 
> consider:
> 
> 	class Foo a where
> 
> 		f :: a -> b -> (a, b)
> 
> Here there is no capitalization distinction in the type of (f) but the 
> implementation can still insert the "forall b." since (a) is already in 
> scope. Therefore similarly, if type constructors like "List" were 
> instead written using lowercase, since they would already be in scope it 
> would be clear even without explicit quantifiers that (a) and (b), but 
> not (list), were to be quantified in the type of (map) (assuming of 
> course that there was no top level data decl for (a) or (b)).

Sure.  ML does it this way, in fact.  Not for type variables, but for
regular pattern variables.  So, IIRC, in ML the empty list is written
nil.  But (playing Devil's advocate) if you have a function declaration

f niil = ...

That's a variable pattern...

The Miranda capitalization rule (which Haskell adopted) is designed to
find such typos automatically, since now you have to write

f Niil

and Niil can't be a variable.

The fact that type signatures in Haskell type classes are subject to the
same problem is certainly a weakness of the design.  I think if new type
variables (universally quantified locally) had a different syntax, so
you said

f :: a -> 'b -> (a, 'b)

where a by itself meant a had better already be in scope, that would be
more consistent.  Then you could drop the capitalization convention
entirely.

> >  Similarly, if we had
> > explicit foralls on equations, we could say
> > 
> > forall n x xn. drop (n+1) (x:xn) = drop n xn
> > 
> > but
> > 
> > forall n. drop n nil = nil
> > 
> > and it would be perfectly clear that `nil' in the latter case was a
> > constructor.
> 
> Actually I quite like the above because it shows that pattern matching 
> can be understood in terms of universally quantified predicates.
> 
> Regarding the verbosity, patterns are something of a special case since 
> variables (that are introduced in the pattern) can only occur once and 
> there is no need to have higher rank quantification in value patterns 
> (disregarding explicit tests for _|_). Therefore special syntax could be 
> used to make the above shorter e.g. borrowing the '?' from Felix 
> (http://felix.sourceforge.net/doc/tutorial/introduction/en_flx_tutorial_top.html 
>   (section 2.11/2.17 etc)):
> 
> 	drop (?n + 1) (_ : ?xn) = drop n xn
> 	drop ?n nil = nil
> 
> (where glued prefix binds tighter than application).

I think this goes with ML's type variable syntax ('a), actually.

> > Of course, if you want to introduce this rule, you'd better start out
> > with it and be consistent --- require every variable to be explicitly
> > brought into scope.  I think you'd find it pretty annoying after trying
> > to program in your new language for a while, though.
> > 
> 
> I agree that there are many good points in favour of Haskell's use of a 
> case distinction, not the least being that it gives definite guidance on 
> when to use lower or upper case identifiers and therefore avoids the 
> mess you find in C++ programs where every programmer has their own 
> private conventions which can lead to confusion and useless debate.

Another system with this advantage would be to invalidate identifiers
beginning with upper case letters entirely :)  (If you really wanted to
go B&D, disallow underscores as well.  Then every identifier /has/ to be
camel-case.)

> However it still seems to me that the case distinction, at least on the 
> level of type constructors, becomes problematic and possibly 
> inconsistent especially if I consider the effects of trying to 
> incorporate something like the ML module system as well as type classes. 
> (For example the Moby language (http://moby.cs.uchicago.edu/ ), a 
> possible successor to SML, uses capitalization for type constructors 
> similar to Haskell which means that type parameters in functor 
> applications must be uppercase, which conflicts with the use of 
> lowercase type params for classes which are a special kind of functor... 
> (Moby itself doesn't encounter any difficulty since it doesn't have type 
> classes)).

It's weird.  ML-derived languages are functional languages at the value
level (and have regular lambda-bound variables in consequence), but are
logical languages at the type level (and have logical variables in
consequence).  So ordinary lambda-bound variables, like in ML-style
functors (parametrized modules) act more like type constants than like
type variables.

Food for thought --- thanks for that!

jcc