infix-type-constructors.md

@@ -23,6 +23,39 @@ And `type` gets an extra production:
 
 (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)
+```
+
+
+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
+
+```wiki
+        data a + b = Left a | Right b
+```
+
+
+That is, we want to define the type *constructor*`(+)`.  Currently we have to use the clumsy `:+` notation:
+
+```wiki
+        data a :+ b = Left a | Right b
+```
+
+
+Yuk. **So I propose that varsyms can be used as type constructors, and not as type variables.**
+
+
+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.
+
+
+I can't think of any down-sides, except the slight loss of consistency ("the hobgoblin of tiny minds").
+
 ## 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.