Naming types

[Simon Marlow]

Manuel M T Chakravarty wrote:
> Ian Lynagh:
>> On Fri, Sep 26, 2008 at 06:25:53PM +0100, Simon Peyton-Jones wrote:
>>> |
>>> | But then you wouldn't be able to write the current meaning of
>>> |     Chan (Int ? Bool ! Emp)
>>> | with infix type variables.
>>>
>>> I am proposing a *change* from current behavior
>>
>> I realise that, I'm just not convinced that completely removing the
>> ability to use infix type variables is a good change.
> 
> Have you ever seen a program that makes use of that ability?  (I haven't.)
> 
>>> | You might say that people don't want to generalise over type
>>> | constructors, but I am not so sure.
>>>
>>> Oh, they certainly do.  My proposal is that it's (much) more 
>>> important to be able to use (+) for type constructors than for type 
>>> variables.
>>
>> I'd have thought that good infix syntax was more important for data
>> constructors than type constructors, and we manage with a : prefix for
>> data constructors.
> 
> Right, but the case rules for identifiers in H98 are not orthogonal in 
> one point: type synonyms are arguably functions on types (they are very 
> simple functions though, as there is no facility for case 
> distinctions).  So, if the rules for the type and value level really 
> were consistent, then names of type synonyms should start with a lower 
> case letter.
> 
> This flaw in H98 leeds to more serious consequences now that we are 
> adding facilities for more serious type-level computations.  In 
> particular, type synonym families -of which vanilla type synonyms are a 
> special case- also use upper case identifiers for consistency.  That's 
> awkward as we use type families as type functions.
> 
> So, I think the Either example from the wiki page is not ideal.  I 
> think, it is perfectly reasonable to have
> 
>   data a :+: b = Left a | Right b
> 
> with analogy to the situation with data constructors.  However, I really 
> would like to be able to write:
> 
>   data Nat = Zero | Succ Nat
> 
>   type family (a::Nat) + (b::Nat) :: Nat
>   type instance Zero     + b = b
>   type instance (Succ a) + b = Succ (a + b)

I think type functions should be lower-case too.  But the problem is that 
type variables are implicitly quantified, whereas term variables are not. 
If type functions were lower case, then presumably an occurrence of that 
name in a type signature would refer to the type function (rather than an 
implicitly-quantified type variable), so defining a new type function might 
break type signatures anywhere within its scope.

Cheers,
	Simon