|Version 5 (modified by guest, 7 years ago) (diff)|
Naming types in Haskell
Haskell currently allows you to use the same name for a type and a data constructor, thus
data Age = Age Int
In any context, it is clear which is meant, thus
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.
There are several distinct ways in which the type/value distinction is becoming blurred.
Type operators. With -XTypeOperators, GHC already allows this
data a :+: b = Left a | Right b
However, I really want to allow this too:
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
f :: (a + b) -> a
the (+) must be the type constructor not the value-level multiplication. But there's a problem with export lists:
module Foo( foo, (+), bar ) where ..
Is this export list exporting the type (+) or the value (+)?
There is a very similar issue with fixity declarations
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:
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:
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.
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
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):
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.
As you might imagine, if we're going to start tinkering with export lists, I'd like to push as far as possible in the direction of signatures. To me, this means (a) Let's not try to make signatures stand independently, but let's do try to change dramatically the format of the export list; (b) the material in the export list should be completely sufficient to know the types, kinds, sorts, classes, instances, and fixities of the things exported; (c) when complete information is available in the export list, it should not be necessary to duplicate the information in the module body. For example, it should be possible to migrate a type signature from the body to a "new-style" export list. ---Norman Ramsey
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
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
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.
If you want a lifting character I suggest "@" instead of "%" since the former is unused in types. -- Lennart
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?