Re: [GHC] #7642: Nullary type classes

7 Feb 2013

      #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 monoidal):

 The comment by Derek explained it nicely, I'll add a bit more.

 Here's a library:

 {{{
 module NumberTheory where

 class RiemannHypothesis where
   assumeRH :: a -> a

 isPrime :: RiemannHypothesis => Integer -> Bool
 isPrime x = assumeRH (x `elem` [2,3])             -- Miller test

 module NumberTheory.RH where

 import NumberTheory

 instance RiemannHypothesis where
   assumeRH = id
 }}}

 Users of the library import both modules. Note that the constraint from
 the signature of isPrime cannot be removed because the instance is
 unavailable.

 Making the assumption on RH explicit is important for mathematicians who
 might use result of a Haskell computation in a proof.

 It also gives a safety net: if RH is disproven you can just remove the
 import and fix compilation errors. A disproof of RH is unlikely - but what
 if the assumption is "MD5 is safe"?

 Here's another case. Suppose we have a large Haskell file containing very
 many calls to head. It sometimes crashes on the empty list. How to find
 the offending call? One solution is adding:

 {{{
 import Prelude hiding (head)

 class Partial where
   err :: String -> a

 head :: Partial => [a] -> a
 head [] = err "head of empty list"
 head (x:xs) = x

 --example
 main :: IO ()
 main = do x <- getLine
           print (head (read x :: [Int]))
 }}}

 Compile the file with -fdefer-type-errors. Each call to head is missing
 the Partial constraint. Defer-type-errors will place locations of those
 calls. Next time the program crashes you will see the offending call,
 something like this:

 {{{
 *E> main
 []
 *** Exception: E.hs:13:18:
     No instance for (Partial) arising from a use of `head'
     Possible fix: add an instance declaration for (Partial)
     In the first argument of `print', namely `(head (read x :: [Int]))'
     In a stmt of a 'do' block: print (head (read x :: [Int]))
     In the expression:
       do { x <- getLine;
            print (head (read x :: [Int])) }
 (deferred type error)
 }}}

 Currently this wouldn't work (#7668), but hopefully the idea is clear.
 Arguably this is a possible solution to #5273. Furthermore, you can place
 the constraint "Partial" in any partial function; a crash in the program
 will tell you the place where you called a partial function outside its
 domain from a supposedly total function.

 Of course this can be simulated with a single-parameter class, but it's
 less elegant.

 Another example: toy version of deprecation. Define

 {{{
 class Deprecated
 }}}

 and again compile with -fdefer-type-errors.

 You can deprecate things just by changing the type:

 {{{
 f :: Deprecated => a -> a
 f x = x
 }}}

 Calls to `f` will work as they did before, but with a compile-time
 warning.

 Nullary constraints allow to encode defects of values in their types -
 partiality, dependence on unproven conjectures, deprecation, unsafety. We
 already have mechanisms such as Safe Haskell and {-# DEPRECATED #-}, which
 are clearly superior in several aspects but their scope is limited.

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