infix-type-constructors.md

@@ -8,56 +8,52 @@
 
 
 
-GHC allows type constructors to be infix operators (conops, beginning with `:`, but not including `:` itself).
+**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`). 
 
-Changes to the syntax may depend on whether [CompositionAsDot](composition-as-dot) is adopted, but roughly speaking we add
+
+**Second proposal**, make *both* varsyms *and* consyms be type *constructors*.  
+That would allow us to say this:
 
 
 ```wiki
- qtycon   -> qconid  | ( qconsym )
- qtyconop -> qconsym | ` qconid `
+        data a + b = Left a | Right b
 ```
 
 
-And `type` gets an extra production:
+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
- type    -> btype qtyconop type
+        data a :+ b = Left a | Right b
 ```
 
 
-(modulo [FixityResolution](fixity-resolution)).  Also, there are obvious changes to the grammar for `type`, `data`, and `newtype` declarations.
-
-
+Yuk. **So I propose that varsyms can be used as type constructors, and not as type variables.**
 
-Secondly, I propose to allow varsyms to be used as type *constructors*.  For example, currently "+" is a varsym, so at the type level it'd behave like a type *variable*
 
 
-```wiki
-        data T (+) = MkT (Int + Int)
-```
-
-
-It's not impossible that this might be useful, although the binding site looks clumsy.  But it misses a much more useful opportunity.  What we *want* is to say
+Changes to the syntax may depend on whether [CompositionAsDot](composition-as-dot) is adopted, but roughly speaking we add
 
 
 ```wiki
-        data a + b = Left a | Right b
+ qtycon   -> qconid  | ( qconsym )
+ qtyconop -> qconsym | ` qconid `
 ```
 
 
-That is, we want to define the type *constructor* `(+)`.  Currently we have to use the clumsy `:+` notation:
+And `type` gets an extra production:
 
 
 ```wiki
-        data a :+ b = Left a | Right b
+ type    -> btype qtyconop type
 ```
 
 
-Yuk. **So I propose that varsyms can be used as type constructors, and not as type variables.**
+(modulo [FixityResolution](fixity-resolution)).  Also, there are obvious changes to the grammar for `type`, `data`, and `newtype` declarations.
 
 
 
@@ -65,7 +61,7 @@ You may say that is inconsistent, because at the value level you have to start d
 
 
 
-Some people use Haskell as a laboratory in which to write their cunning type ideas. In mathematics, operators are invariably top-level type constructors (think of the type a+b).  Mirroring this in Haskell would make the transcription more elegantly direct.
+Some people use  constructors (think of the type a+b).  Mirroring this in Haskell would make the transcription more elegantly direct.
 
 
 
@@ -94,11 +90,25 @@ I can't think of any down-sides, except the slight loss of consistency ("the hob
 ## 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.
+
+  ```wiki
+          data T (~>) = MkT (Int ~> Int)
+  ```
+
+
+We'd have to use a type variable in back-quotes instead.
+
+
 ## Observations
 
 
 - 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.)