Opened 6 years ago

Closed 6 years ago

#7642 closed feature request (fixed)

Nullary type classes

Reported by: shachaf Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 7.6.1
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: typecheck/should_fail/TcNoNullaryTC,TcNullaryTcFail, should_run/TcNullaryTC
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

GHC supports MultiParamTypeClasses with two or more parameters, but it explicitly rejects classes with no parameters. There doesn't seem to be a good reason for that.

Some example uses that came up in IRC:

isPrime :: RiemannHypothesis => Integer -> Bool

unsafePerformIO :: Unsafe => IO a -> a

The main reason to allow it is probably that it's a pointless restriction, like EmptyDataDecls. In fact, the simplest implementation for this patch consists of deleting one line of code. The attached patch is slightly bigger because it also fixes error messages (I also included a detabbing patch).

If necessary this can be made a separate LANGUAGE flag -- this patch just folds it into MultiParamTypeClasses.

Attachments (5)

0001-Nullary-type-classes.patch (2.4 KB) - added by shachaf 6 years ago.
0002-Detab-TcTyClsDecls.hs.patch (49.1 KB) - added by shachaf 6 years ago.
p0001-detab-TcTyClsDecl.patch (71.4 KB) - added by monoidal 6 years ago.
Detabbing
p0002-nullary-type-classes.patch (7.8 KB) - added by monoidal 6 years ago.
p0003-Tests-for-nullary-type-classes.patch (4.8 KB) - added by monoidal 6 years ago.

Download all attachments as: .zip

Change History (15)

Changed 6 years ago by shachaf

Changed 6 years ago by shachaf

comment:1 Changed 6 years ago by monoidal

I strongly support this feature, but another change is needed.

{-# LANGUAGE MultiParamTypeClasses #-}
class A where
  f :: a -> a


H.hs:2:1:
    The class method `f'
    mentions none of the type variables of the class A
    When checking the class method: f :: forall a. a -> a
    In the class declaration for `A'
Failed, modules loaded: none.

comment:2 Changed 6 years ago by simonpj

difficulty: Unknown

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

comment:3 in reply to:  2 Changed 6 years ago by DerekElkins

The idea is that there wouldn't necessarily be an instance. The final application code would make the instance, in that case, if they were willing to rely on results that rely on the truth of the Riemann Hypothesis. Similarly for Unsafe. Until that instance was made, it would be a compile error (an unresolvable constraint), so you'd be notified if you inadvertently relied on it, and it would be explicit in the signatures of all functions that used the features.

Another use-case is statically configurable parameters, e.g. class Modulus where modulus :: Integer. With this, applications can configure such parameters just by specifying some instances, say in their Main module.

comment:4 Changed 6 years ago 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.

comment:5 Changed 6 years ago by simonpj

Do implicit parameters not serve this purpose rather well?

Simon

comment:6 in reply to:  5 Changed 6 years ago 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.

comment:7 Changed 6 years ago by simonpj

OK, fine. I can't say I find the motivation very persuasive, but I agree in general that lifting restrictions is a Good Thing provided it does not have knock-on consequences. Maybe this doesn't.

Do you feel like augmenting your patch?

  • We need an extension flag -XNullaryTypeClases.
  • Test the flag when needed (you know the place)
  • Document the flag in the usar manual
  • Perhaps a test case or two

If you do that, I'll drop it in. Thanks!

Simon

Changed 6 years ago by monoidal

Detabbing

Changed 6 years ago by monoidal

Changed 6 years ago by monoidal

comment:8 Changed 6 years ago by monoidal

Status: newpatch

Patches attached. I could not directly use shachaf's detabbing patch, git gave me error about trailing whitespace.

comment:9 Changed 6 years ago by simonpj@…

commit 5319ea79fa1572b7d411548532031f9d19b928c6

Author: Simon Peyton Jones <simonpj@microsoft.com>
Date:   Wed Mar 13 21:10:20 2013 +0000

    Implement nullary type classes (#7642)
    
    This is a slightly refined version of a patch by shachaf,
    done by Krzysztof Gogolewski <krz.gogolewski@gmail.com>.

 compiler/main/DynFlags.hs           |    2 +
 compiler/typecheck/TcTyClsDecls.lhs |   17 +-
 compiler/typecheck/TcValidity.lhs   | 2481 ++++++++++++++++++-----------------
 docs/users_guide/flags.xml          |    6 +
 docs/users_guide/glasgow_exts.xml   |   29 +
 5 files changed, 1292 insertions(+), 1243 deletions(-)

comment:10 Changed 6 years ago by simonpj

Resolution: fixed
Status: patchclosed
Test Case: typecheck/should_fail/TcNoNullaryTC,TcNullaryTcFail, should_run/TcNullaryTC

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

Note: See TracTickets for help on using tickets.