Version 7 (modified by simonpj@…, 6 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.

- Need to allow infix notation in contexts
f :: (a >> b) => bla blah

- Watch out for code like this (http://hackage.haskell.org/trac/ghc/ticket/1727)
infixr 5 `Foo` infixr 6 `Bar` data a `Foo` b = a `FOO` a `Bar` b data a `Bar` b = a `BAR` b

## References

- Infix type constructors, classes, and type variables in the GHC User's Guide.

## 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.