wiki:InfixTypeConstructors

Version 11 (modified by simonpj@…, 3 years ago) (diff)

--

Infix Type Constructors

Brief Explanation

First proposal: allow infix notation in types, in two forms:

  • Regular names in back quotes. This works for type constructors (eg a `TyCon` b) and type variables (eg Int `a` Bool)
  • Operator symbols (e.g. (a + b), or (a :+: b).

Second proposal, make both varsyms and consyms be type constructors. That would allow us to say this:

        data a + b = Left a | Right b

That is, we want to define the type constructor (+). GHC's current choice (done for a pseudo-consistency with the value level) is to allow only consyms as type constructors. So we cannot give the declaration above (because (+) is a type variable. Instead we can say only this:

        data a :+ b = Left a | Right b

Yuk. So I propose that varsyms can be used as type constructors, and not as type variables.

Changes to the syntax may depend on whether CompositionAsDot is adopted, but roughly speaking we add

 qtycon   -> qconid  | ( qconsym )
 qtyconop -> qconsym | ` qconid `

And type gets an extra production:

 type    -> btype qtyconop type

(modulo FixityResolution). Also, there are obvious changes to the grammar for type, data, and newtype declarations.

Observations

  • You may say that it's inconsistent for (+) to range over type constructors, because at the value level you have to start data constructors with a ":". But the type level is already funny. The whole type-family idea (including H98 type synonyms) defines things that begin with a capital letter, but which (unlike data constructors) are not head normal forms. Looking further ahead, by the time we have full type-synonym families, they really are functions as much as any value-level function is. For example it would be silly to insist on a leading colon here:
      type family (+) :: * -> * -> *
      type instance Zero + n2 = n2
      type instance (Succ n1) + n2 = Succ (n1 + n2)
    
  • Note that classes can be infix too; this is useful.

  • If you say module M( (+) ) where ... are you exporting the type constructor (+) or the value (+)? Ditto import lists. Possibilities:
    • An ambiguous reference defaults to the locally-defined one. (If we did this we should do so consistently, including for unqualified names in the text of a module. I think this'd be a Good Thing. A warning flag could warn if you used it. It's just like shadowing.)
    • If the two (+) things are not both locally defined, you can disambiguate with a qualified name Prelude.(+) or M.(+). That does not help if you define both in M.
    • Use a keyword to distinguish; eg module M( data (+) ) where. There are design issues here (e.g. distinguish data and newtype?).
  • Can you set the fixity of a type constructor T differently than the data constructor T? This is a similar ambiguity to the one in export lists. Except that in this case it is very common to have a type constructor and data constructor with the same name.

Lexical ambiguity

The second proposal---to treat all infix operators as type constructors---leads to an ambiguity in import/export declarations:

module Test ( (+) ) where

This export declaration is ambiguous because it is not clear if we mean to export the value operator (+), the type constructor (+), or both. Exactly the same issue arises for

Solution A

One possible solution is to state that, when written on their own, infix operators in import/export specifications refer to the value level. So in the above example we would be exporting the value operator (+).

To import/export the type constructor one would have to use an explicit (possibly empty) sub-ordinate list:

module Test ( (+)() ) where

Unfortunately, such specifications look rather odd.

Solution B

Another solution would be to introduce a new piece of syntax which would translate to the same thing. Perhaps:

module Test ( type (+) ) where

The intention here is that type specifies the namespace of the following name, and not that it is a type synonym. Haskell already allows module M in export lists, for the same reason. It might make sense to allow class C as well.

Arguably value C would make sense too, meaning "the data constructor C" which currently cannot be mentioned in an export or import list except in the form T(C). But that would mean a new keyword, albeit only in this context.

References

Tickets

#78
Add infix type constructors

Pros

  • This is a straightforward generalisation, and doesn't break any existing code (except code that uses GHC extensions to have a type variable that is an operator).
  • It's very useful to write type expressions like (a + b).

Cons

  • If operators are type constructors, they can't also be type variables. I know one place where people use a type variable that is an operator. Something like this.
            data T (~>) = MkT (Int ~> Int)
    

We'd have to use a type variable in back-quotes instead.