Changes between Version 4 and Version 5 of InfixTypeConstructors


Ignore:
Timestamp:
Oct 9, 2008 7:50:31 AM (6 years ago)
Author:
simonpj@…
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • InfixTypeConstructors

    v4 v5  
    44== Brief Explanation == 
    55 
    6 GHC allows type constructors to be infix operators (conops, beginning with {{{:}}}, but not including {{{:}}} itself). 
     6'''First proposal''': allow infix notation in types, in two forms: 
     7  * Regular names in back quotes.  This works for type constructors (eg {{{a `TyCon` b}}}) and type variables (eg {{{Int `a` Bool}}}) 
     8  * Operator symbols (e.g. (`a + b`), or (`a :+: b`).  
     9 
     10'''Second proposal''', make ''both'' varsyms ''and'' consyms be type ''constructors''.   
     11That would allow us to say this: 
     12{{{ 
     13        data a + b = Left a | Right b 
     14}}} 
     15That 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: 
     16{{{ 
     17        data a :+ b = Left a | Right b 
     18}}} 
     19Yuk. '''So I propose that varsyms can be used as type constructors, and not as type variables.''' 
    720 
    821Changes to the syntax may depend on whether CompositionAsDot is adopted, but roughly speaking we add 
     
    2134(modulo FixityResolution).  Also, there are obvious changes to the grammar for {{{type}}}, {{{data}}}, and {{{newtype}}} declarations. 
    2235 
    23 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'' 
    24 {{{ 
    25         data T (+) = MkT (Int + Int) 
    26 }}} 
    27 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 
    28 {{{ 
    29         data a + b = Left a | Right b 
    30 }}} 
    31 That is, we want to define the type ''constructor'' `(+)`.  Currently we have to use the clumsy `:+` notation: 
    32 {{{ 
    33         data a :+ b = Left a | Right b 
    34 }}} 
    35 Yuk. '''So I propose that varsyms can be used as type constructors, and not as type variables.''' 
     36 
    3637 
    3738You 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. 
    3839 
    39 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. 
     40Some people use constructors (think of the type a+b).  Mirroring this in Haskell would make the transcription more elegantly direct. 
    4041 
    4142I can't think of any down-sides, except the slight loss of consistency ("the hobgoblin of tiny minds"). 
     
    5455== Cons == 
    5556 
     57* 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. 
     58{{{ 
     59        data T (~>) = MkT (Int ~> Int) 
     60}}} 
     61We'd have to use a type variable in back-quotes instead. 
     62 
    5663== Observations == 
    5764 
    5865 * Note that classes can be infix too; this is useful. 
    59  
     66  
    6067 * If you say `module M( (+) ) where ...` are you exporting the type constructor `(+)` or the value `(+)`? Ditto import lists.  Possibilities: 
    6168   * 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.)