

# Naming types in Haskell









Haskell currently allows you to use the same name for



a type and a data constructor, thus






```wiki



data Age = Age Int



```









In any context, it is clear which is meant, thus






```wiki



foo :: Age > Int  Type constructor Age



foo (Age i) = i  Data constructor Age



```









However, as we extend Haskell's type system (or at least



GHC's), there are occasions in which the distinction is



less clear. This page summarises the issues, and proposes



solutions.









NB: the whole page is purely about *syntax*.









Please comment on glasgowhaskellusers@…, or



by adding notes to this page.






## The issues









There are several distinct ways in which the type/value



distinction is becoming blurred.






**Type operators**. With `XTypeOperators`, GHC already allows this






```wiki



data a :+: b = Left a  Right b



```









However, I really want to allow this too:






```wiki



data a + b = Left a  Right b



```









That is, allow oprerators like `(+)` to be type constructors.



You can find discussion of the merits of this proposal here.



At first it seems fairly straightforward; for example, it is



quite clear that in a type signature






```wiki



f :: (a + b) > a



```









the `(+)` must be the type constructor not the valuelevel



multiplication. But there's a problem with export lists:






```wiki



module Foo( foo, (+), bar ) where ..



```









Is this export list exporting the type `(+)` or the value `(+)`?









There is a very similar issue with fixity declarations






```wiki



infix 5 +, :+:



```









In these two contexts we need to disambiguate whether we mean



the typelevel or valuelevel identifier.






**Proper kinding**. At the moment you see a lot of this



kind of nonsense:






```wiki



data Zero



data Succ a



data List :: * > * > * where



Cons :: a > List n a > List (Succ n) a



...etc...



```









The indexed data type `List` is only supposed to get



`Zero` or `Succ` as its first arugments,



the stupid type `(List Int Int)` is, alas,



well kinded. Obviously what we want is to give a proper



kind to `List`. My current proposal is to allow valuelevel



data constructors to be reused at the type level, thus:






```wiki



data Nat = Zero  Succ Nat



data List :: Nat > * > * where



Cons :: a > List n a > List (Succ n) a



```









Again, I don't want to elaborate all the details here, but



the point is that a data constructor (`Succ`) is being used



in a type. If there also happened to be a type constructor



`Succ`, it'd be unclear which you meant, and you really might



want either.






**Typelevel lists and tuples**. Folllowing on from the



preceding thought, we can presumably reuse tuples at the



type level. So if we write the type `(T (Int,Bool))` do



mean that






 `T :: * > *`, and we are instantiating it with the type `(Int,Bool) :: *`?



 `T :: (*,*) > *`, and we are instantiating it with the pair types `Int::*` and `Bool::*`?









If you write it prefix, thus `(T ((,) Int, Bool))`, we can



see that this the same as the `Succ` question above:



in this type do we mean to name the *type* constructor `(,)`



or the *data* constructor `(,)`.









Exactly same questions can be asked about the special purpose



list syntax `[a,b,c]`. When we write `(T [])` do we mean



the type constructor `[]` or the data constructor `[]`?



But there is a bit more here, because `[a,b,c]` is



syntactic sugar.






## Proposals









I make two proposals:






 Disambiguation in export lists and fixity declarations



 Disambiguation in types






### Proposal 1: disambiguation in export lists and fixity declarations






 Extend export lists and fixity declarations to permit the



disambiguating specifier `data`, `type`, and `class`.



 The specifier is always permitted, but only required if the



situation would otherwise be ambiguous.



 The specifier must match the corresponding declaration, except that



the specifier `data` matches a `newtype` declaration too. (This



"except" is arguable. The idea is that someone looking at the



export list doesn't need to know whether the type is declared with



`data` or `newtype`, whereas for `type` synonyms they do need to



know.)









Thus you can say






```wiki



module Foo( data T(T1,T2), S, class C ) where



data T = T1  T2



data S = S1  S2



class C a where ...



```









In this case the `data` and `class` specifiers are both optional.



But they are not always optional (that is the point):






```wiki



module Foo( data (%%%)(...) ) where



infix 4 data (%%%)  The type constructor



infix 6 (%%%)  The function



data a %%% b = a :%%% b



a %%% b = a :%%% b



```









Looking just at the export lists, you can see this proposal as a



baby step towards the export list becoming a proper module signature.






### Proposal 2: disambiguation in types






 Valuelevel data constructors in types may be disambiguated by a shift operator `%`.



 This disambiguation is compulsory only if there is a likenamed type constructor in scope.









Suppose the following data types are available






```wiki



data Nat = Zero  Succ Nat



data Succ = A  B



data List :: Nat > * where ...



data T :: [Nat] > * where ...



```









Now here are the interpretation of various types






```wiki



List Zero :: *  Zero means the data constructor



 (since there is no type constructor Zero)



List (Succ Zero)  Succ means the type constructor



 hence illkinded



List (%Succ Zero) :: *  %Succ means the data constructor



List (%Succ %Zero) :: *  %Zero is also legal to mean the data constr






T []  [] means the list type constructor



 hence illkinded



T %[] :: *  %[] means the data constructor []






T [Zero]  [..] means the list type



 hence illkinded



T %[Zero] :: *  %[..] means list syntax (Zero : [])






[(Int,Bool)] :: *  The ordinary H98 type



[%(Int,Bool)]  Ill kinded



%[%(Int,Bool)] :: [(*,*)]



() :: *  The ordinary H98 type



%() :: ()



```









The principles are






 Just as with Haskell 98, if the lexical binding is unambiguous,



there is no need for a disambiguating shift operator (although one



is always permitted)






 Just as with Haskell 98, disambiguation is purely lexical; it does



not take advantage of kind checking.









Whether "`%`" is the best notation isn't clear to me, but the



notation must be reasonably quiet.






### Alternatives to proposal 2






 One alternative would be simple but brutal: simply have



no "`%`" escape notation. In the above examples, saying



`Succ` at the the type level would mean the data type `Succ`,



and there would be no way to get to the data constructor.



You lose.






 Another alternative would be to allow the type name to



disambiguate. Thus `Nat.Succ` would name the data construtor.



(Obvious question: the overlap with the module qualifiers.)






 Not every data type type can be lifted to the kind level; for



example, existentials and GADTS! It seems messy to have this done



or not done silently; perhaps there should be some indication in



the data type declaration to say "make this available as a kind



too". Or perhaps the whole idea of automatic lifting isn't worth



the candle, and we should should provide explicit `datakind`.









None of these alternatives seem compatible with lists and



tuples at the type level. Maybe they can still use the "`%`" notation? 