#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: | ----------------------------------------+----------------------------------- Changes (by simonpj): * difficulty: => Unknown Comment: Can you say ''why'' you strongly support it? It looks very marginal to me. The only reason it vaguely makes sense is that it's easy to implement. But if you have {{{ isPrime :: RiemannHypothesis => Integer -> Bool isPrime = ... blah... }}} then the chances are that this will also compile {{{ isPrime :: Integer -> Bool isPrime = ... blah... }}} because presumably the instance exists. To me it seems marginal, and at worst confusing. Simon -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7642#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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

#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

#7642: Nullary type classes ----------------------------------------+----------------------------------- Reporter: shachaf | Owner: Type: feature request | Status: patch 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: | ----------------------------------------+----------------------------------- Changes (by monoidal): * status: new => patch Comment: Patches attached. I could not directly use shachaf's detabbing patch, git gave me error about trailing whitespace. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7642#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#7642: Nullary type classes ------------------------------------------------------------------------------------------+ Reporter: shachaf | Owner: Type: feature request | Status: closed Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.6.1 Resolution: fixed | Keywords: Os: Unknown/Multiple | Architecture: Unknown/Multiple Failure: None/Unknown | Difficulty: Unknown Testcase: typecheck/should_fail/TcNoNullaryTC,TcNullaryTcFail, should_run/TcNullaryTC | Blockedby: Blocking: | Related: ------------------------------------------------------------------------------------------+ Changes (by simonpj): * status: patch => closed * testcase: => typecheck/should_fail/TcNoNullaryTC,TcNullaryTcFail, should_run/TcNullaryTC * resolution: => fixed Comment: OK, I've committed. I'm not convinced it's going to be useful to many, but you convinced me that it's a simple non-invasive change that removes restrictions, and I agree that is good. Thanks! Simon -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7642#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler