infix-type-constructors.md

@@ -2,56 +2,51 @@
 
 ## Brief Explanation
 
+**First proposal**: allow infix notation in types, in two forms:
 
-GHC allows type constructors to be infix operators (conops, beginning with `:`, but not including `:` itself).
+- 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.
-
-
-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)
-```
+Yuk. **So I propose that varsyms can be used as type constructors, and not as type variables.**
 
 
-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.
 
 
 You may say that is inconsistent, 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 (beginning with type synonyms) defines things that begin with a capital letter, but which (unlike data constructors) are not head normal forms.  By the time we have full type-synonym families, they really are \*functions\* as much as any value-level function is.
 
 
-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.
 
 
 I can't think of any down-sides, except the slight loss of consistency ("the hobgoblin of tiny minds").
@@ -71,6 +66,15 @@ 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.