[GHC] #7642: Nullary type classes

[GHC]

#7642: Nullary type classes
----------------------------------------+-----------------------------------
    Reporter:  shachaf                  |       Owner:                  
        Type:  feature request          |      Status:  new             
    Priority:  normal                   |   Milestone:                  
   Component:  Compiler (Type checker)  |     Version:  7.6.1           
    Keywords:                           |          Os:  Unknown/Multiple
Architecture:  Unknown/Multiple         |     Failure:  None/Unknown    
  Difficulty:  Unknown                  |    Testcase:                  
   Blockedby:                           |    Blocking:                  
     Related:                           |  
----------------------------------------+-----------------------------------

Comment(by DerekElkins):

 It handles the modulus example well, but I don't see how it handles any of
 the other examples at all.  If the purpose is to write an application that
 doesn't rely on the Riemann Hypothesis or Unsafe functions, you don't want
 a library to locally provide an instance by let binding an implicit
 parameter.  (I'm not even sure what these implicit parameters would be.)
 The nullary type class approach exploits the global nature of instances.
 Usually that causes modularity problems, but here we turn those problems
 into an advantage.  Any library that made the instance would break with
 any other library or application that did the same.  This would presumably
 include several applications effectively enforcing that only applications
 would make these instances.

 Conceptually, a nullary type class is just a type-level proposition which
 is certainly natural, and seems like a likely thing for tools that target
 the type-level logic programming system to occasionally produce.  Right
 now they'd have to use an encoding like the one demonstrated below which I
 used a couple of years ago to see how GHC would reduce these almost
 trivial constraints.  I believe, but have not demonstrated, that
 constraint kinds allow the start of some propositional algebra on these
 propositions.  I'm sure that there are other tricks that can be done with
 them to extend their expressiveness.

 class Unsafe a | -> a;  f :: Unsafe () => ...

 The history of this for me began a couple of years ago when I was
 appreciating the fact that Haskell rarely adds arbitrary restrictions, and
 as an example I wondered if nullary type classes were handled.  The answer
 in GHC (but not Hugs) is "no".  History has shown that these restrictions
 eventually chafe some people and in some cases get rectified.  For
 example, empty data declarations and empty case expressions.  On the flip
 side, I'm not aware of anyone complaining about the lack of arbitrary
 restrictions.  For example, I've never heard anyone complain about the
 completely useless but legal form (let in 3).  The only benefit of this
 construct is to simplify code generators; logic that applies to nullary
 type classes, empty data declarations, and empty cases as well.  For me,
 this restriction should be removed on principle even with no use cases.
 However, there are use cases, and I'm sure more will be discovered.  I
 don't see this causing any more confusing errors or confusing beginners
 any more or less than what is already possible with type classes.

-- 
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/7642#comment:6>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler