design/type-naming.md

+# 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 glasgow-haskell-users@…, 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 value-level
+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 type-level or value-level 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 value-level
+data constructors to be re-used 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.
+
+**Type-level lists and tuples**.  Folllowing on from the 
+preceding thought, we can presumably re-use 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
+
+- Value-level data constructors in types may be disambiguated by a shift operator `%`.
+- This disambiguation is compulsory only if there is a like-named 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 ill-kinded
+  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 ill-kinded
+  T %[] :: *                -- %[] means the data constructor []
+
+  T [Zero]                  -- [..] means the list type
+                            -- hence ill-kinded
+  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?