Skip to content

Changes

Page history
Edit InfixTypeConstructors authored by ross@soi.city.ac.uk's avatar ross@soi.city.ac.uk
Hide whitespace changes
Inline Side-by-side
infix-type-constructors.md
View page @ 603b9ecb
# 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`).
# Infix Type Constructors
**Second proposal**, make *both* varsyms *and* consyms be type *constructors*.
That would allow us to say this:
```wiki
data a + b = Left a | Right b
```
## Brief Explanation
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:
```wiki
data a :+ b = Left a | Right b
```
GHC allows type constructors to be infix operators (conops, beginning with `:`, but not including `:` itself).
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](composition-as-dot) is adopted, but roughly speaking we add
```wiki
qtycon -> qconid | ( qconsym )
qtyconop -> qconsym | ` qconid `
......@@ -35,6 +23,7 @@ Changes to the syntax may depend on whether [CompositionAsDot](composition-as-do
And `type` gets an extra production:
```wiki
type -> btype qtyconop type
```
......@@ -42,110 +31,26 @@ And `type` gets an extra production:
(modulo [FixityResolution](fixity-resolution)). 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:
```wiki
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( type (+) ) 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
```wiki
f :: (a >> b) => bla blah
```
- Watch out for code like this ([ http://hackage.haskell.org/trac/ghc/ticket/1727](http://hackage.haskell.org/trac/ghc/ticket/1727))
```wiki
infixr 5 `Foo`
infixr 6 `Bar`
data a `Foo` b = a `FOO` a `Bar` b
data a `Bar` b = a `BAR` b
```
## Lexical ambiguity
The second proposal—-to treat all infix operators as type constructors—-leads to an ambiguity in import/export declarations:
```wiki
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
- export lists
- import lists
- fixity declarations
- GHC's RULEs (see [ http://hackage.haskell.org/trac/ghc/ticket/2600](http://hackage.haskell.org/trac/ghc/ticket/2600)) and ANN annotations
### 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:
```wiki
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:
```wiki
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
- [ Infix type constructors, classes, and type variables](http://www.haskell.org/ghc/docs/latest/html/users_guide/type-extensions.html#infix-tycons) in the GHC User's Guide.
## Tickets
<table><tr><th>[\#78](https://gitlab.haskell.org//haskell/prime/issues/78)</th>
<td>Add infix type constructors</td></tr></table>
## 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
## Pros
- 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.
- This is a straightforward generalisation, doesn't break any existing code, and improves the consistency of the syntax.
```wiki
data T (~>) = MkT (Int ~> Int)
```
## Cons
We'd have to use a type variable in back-quotes instead.