Opened 7 years ago

Closed 3 years ago

Last modified 10 months ago

#2431 closed feature request (fixed)

Allow empty case analysis

Reported by: RalfHinze Owned by:
Priority: low Milestone:
Component: Compiler Version: 6.8.3
Keywords: empty case analysis Cc: id@…, eir@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: deSugar/should_compile/T2431
Blocked By: Blocking:
Related Tickets: Differential Revisions:

Description (last modified by simonpj)

Using -XEmptyDataDecls I can declare an (almost) empty data type.

  data Void

However, I can't use an empty case to discriminate values of the empty type.

This does not work:

  get :: Void -> a

Only the type signature, but no body. [This would be useful also in other circumstances.]

  get :: Void -> a
  get v = case v of { }

An empty case in the body.

Change History (15)

comment:1 Changed 7 years ago by simonpj

  • Description modified (diff)
  • difficulty set to Unknown

Why is this useful? The only value of type Void is bottom.

Simon

comment:2 Changed 7 years ago by NeilMitchell

This would be somewhat useful for the Derive tool (http://www.cs.york.ac.uk/fp/darcs/derive), and in general for program generation. Consider the automatically derived instance for Show, on an empty data type. What you are likely to get is:

instance Show Void where

i.e. the complete absense of anything. If you changed the generator to make a case statement, you could get:

instance Show Void where
    show x = case x of {}

Which is a more accurate reflection of what was intended, and I think the point Ralf is trying to make. Derive probably goes wrong with empty data types, but if it didn't, this extension would be helpful.

I tried to construct an empty case with Template Haskell, and crashed GHC:

C:\Neil\Temp>ghci -fth
GHCi, version 6.8.2: http://www.haskell.org/ghc/  :? for help
Loading package base ... linking ... done.
Prelude> :m Language.Haskell.TH
Prelude Language.Haskell.TH> $(caseE (litE $ CharL 'a') [])
: panic! (the 'impossible' happened)
  (GHC version 6.8.2 for i386-unknown-mingw32):
        readFilledBox t_a1b5{tv} [box]

Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

comment:3 Changed 7 years ago by Isaac Dupree

  • Cc id@… added

Of course, with the correct warning flags enabled, empty case of a non-empty type will produce an "incomplete pattern match" warning: exactly when we want a warning for using this construct.

I suppose the effect is to throw a pattern-match error that is independent of the case'd value, as consistent with all patterns of any other case statement failing? (rather than using it if it's _|_, as of course it will be if it's an empty type: because, unlike in GHC Core, source-Haskell 'case' does not introduce strictness)

+1, I've occasionally wanted this to be possible

comment:4 Changed 7 years ago by igloo

  • Milestone set to 6.12 branch

Perhaps this would be better proposed for Haskell'?

comment:5 Changed 7 years ago by simonpj

  • Milestone changed from 6.12 branch to _|_
  • Priority changed from normal to low

OK so I don't like GHC crashing, ever, so I have done the following:

  • In the renamer and typechecker, I allow empty HsCase.
  • In Core I still don't allow empty Case. I have no idea what stuff would break if empty Case was allowed; but even finding the type of an expression might become impossible. (Yes, at the moment Case records its result type, but with the new FC stuff that's not necessary and I may remove it.) And I see no reason to support it.
  • In the desugarer, I desguar empty HsCase to a call to error. (The simplifier already does this if it can figure out that a case is empty; see Simplify.rebuildCase.)

So now Neil's TH example works instead of crashing. The parser prevents you doing this in source code, so I have not added a flag.

To go the full distance we still need:

  • Parser to accept empty case expressions (currently rejected by parser)
  • -X flag to control this language extension
  • Test somewhere (in renamer) to check that empty case only happens when flag is on.
  • User manual docs
  • Regresssion tests in test suite.

All easy but tiresome. If you care about this, send a patch! I've done the slightly-tricky bits. So I'll leave this bug open at low priority, milestone bottom.

Simon

comment:6 follow-up: Changed 7 years ago by malcolm.wallace@…

I tried to think of how parsing might go wrong. Consider the following (contrived) example:

case foo of
  [] ->
    case bar of
  (x:xs) ->
    baz

Did you spot that the second alternative is indented with a tab rather than spaces, (with editor tab width set to 2 instead of 8)? So although I _intended_ to have the two alternatives for the outer case, and the inner case empty, in fact the second pattern is indented further than the first, and so there is a single alternative for each of the inner and outer cases?

Well, I did say it was contrived. -fwarn-incomplete-patterns would catch it.

comment:7 in reply to: ↑ 6 Changed 7 years ago by simonmar

Replying to [email protected]:

I tried to think of how parsing might go wrong. Consider the following (contrived) example:

case foo of
  [] ->
    case bar of
  (x:xs) ->
    baz

Did you spot that the second alternative is indented with a tab rather than spaces, (with editor tab width set to 2 instead of 8)?

I realise the example is contrived, but I don't think we need to consider it. The Haskell report defines tab stops to be 8 characters apart, so you should always have your editor set to use 8-character tab stops when editing Haskell code, because that's how the compiler sees it. Anything else will cause confusion, in many more ways than just the example above. If you don't like 8-char tabs then fine: use spaces instead, and -fwarn-tabs, but you should still set your editor to use 8-char tabs so that you can read other people's code.

comment:8 Changed 7 years ago by simonmar

  • Architecture changed from Unknown to Unknown/Multiple

comment:9 Changed 7 years ago by simonmar

  • Operating System changed from Unknown to Unknown/Multiple

comment:10 Changed 3 years ago by goldfire

  • Cc eir@… added
  • Type of failure set to None/Unknown

Now that GHC is getting more dependently typed features, an empty case seems more useful. For example, I would like to define the following:

data a :==: b where
  Refl :: a :==: a

data EmptySet
type Not a = a -> EmptySet

type DecidableEquality (a :: k) (b :: k) = Either (a :==: b) (Not (a :==: b))

data SBool :: Bool -> * where
  SFalse :: SBool False
  STrue :: SBool True

eqBoolDec :: SBool a -> SBool b -> DecidableEquality a b
eqBoolDec SFalse SFalse = Left Refl
eqBoolDec STrue STrue = Left Refl
eqBoolDec SFalse STrue = Right (\case {})
eqBoolDec STrue SFalse = Right (\case {})

Even if empty pattern matches were allowed, I recognize that this would just produce an (erroneous) incomplete pattern match warning, because of bug #3927. But, once that is fixed, empty pattern matches would have a new lease on life.

comment:11 Changed 3 years ago by simonpj

  • Summary changed from allow empty case analysis to Allow empty case analysis

I didn't find the above entirely clear, so Richard elaborates: consider:

data a :~: b where
  Refl :: a :~: a

absurd :: True :~: False -> a

Now, I want to write a term binding for absurd. Here are two candidates:

absurd x = error "absurd"    -- (A)
absurd x = case x of {}      -- (B)

I much prefer (B). Why? Because GHC can figure out that (True :~: False) is an empty type. So (B) has no partiality and, (if #3927 is fixed) I should be able to compile with -fwarn-incomplete-patterns and -Werror.

On the other hand (A) looks dangerous, and GHC doesn't check to make sure that, in fact, the function can never get called.

The bottom line, for me at least, is that I want to avoid the partial constructs (incomplete patterns, undefined, etc) in Haskell as much as possible, especially when I'm leveraging the type system to a high degree. The lack of empty case statements forces me to use undefined where it isn't really necessary.

comment:12 Changed 3 years ago by igloo

What's the status of this? ac230c5ef652e27f61d954281ae6a3195e1f9970 from #6067 sounds like it implements this, but it looks like it only allows it in core, not Haskell?

comment:13 Changed 3 years ago by simonpj

Oh ok I'll join up the final dots... patch coming.

comment:14 Changed 3 years ago by simonpj

  • Resolution set to fixed
  • Status changed from new to closed
  • Test Case set to deSugar/should_compile/T2431

Here it is:

commit 3671e674757c8f82ec1f0ea9b7c1ed56340b55bc
Author: Simon Peyton Jones <[email protected]>
Date:   Fri Jan 4 10:27:38 2013 +0000

    Allow empty case expressions (and lambda-case) with -XEmptyCase
    
    The main changes are:
      * Parser accepts empty case alternatives
      * Renamer checks that -XEmptyCase is on in that case
      * (Typechecker is pretty much unchanged.)
      * Desugarer desugars empty case alternatives, esp:
          - Match.matchWrapper and Match.match now accept empty eqns
          - New function matchEmpty deals with the empty case
          - See Note [Empty case alternatives] in Match
    
    This patch contains most of the work, but it's a bit mixed up
    with a refactoring of MatchGroup that I did at the same time
    (next commit).

 compiler/deSugar/DsExpr.lhs       |   13 +-------
 compiler/deSugar/DsUtils.lhs      |    2 +-
 compiler/deSugar/Match.lhs        |   55 ++++++++++++++++++++++++++++---------
 compiler/deSugar/MatchCon.lhs     |    3 +-
 compiler/deSugar/MatchLit.lhs     |    2 +-
 compiler/main/DynFlags.hs         |    4 ++-
 compiler/parser/Parser.y.pp       |    2 +
 compiler/rename/RnBinds.lhs       |   18 ++++++++++--
 docs/users_guide/glasgow_exts.xml |   38 +++++++++++++++++++++++++
 9 files changed, 106 insertions(+), 31 deletions(-)

but it also needs the follow up

commit a8941e2a4fe3b000e6c085701e0c015c5316c6ee
Author: Simon Peyton Jones <[email protected]>
Date:   Fri Jan 4 10:30:14 2013 +0000

    Refactor HsExpr.MatchGroup
    
     * Make MatchGroup into a record, and use the record fields
    
     * Split the type field into two: mg_arg_tys and mg_res_ty
       This makes life much easier for the desugarer when the
       case alterantives are empty
    
    A little bit of this change unavoidably ended up in the preceding
    commit about empty case alternatives

 compiler/deSugar/Coverage.lhs    |   12 ++++++------
 compiler/deSugar/DsArrows.lhs    |   13 ++++++-------
 compiler/deSugar/DsExpr.lhs      |    8 ++++----
 compiler/deSugar/DsGRHSs.lhs     |   14 +++++++-------
 compiler/deSugar/DsMeta.hs       |   10 +++++-----
 compiler/hsSyn/HsExpr.lhs        |   28 +++++++++++++---------------
 compiler/hsSyn/HsUtils.lhs       |    2 +-
 compiler/parser/RdrHsSyn.lhs     |    8 ++++----
 compiler/rename/RnBinds.lhs      |    4 ++--
 compiler/rename/RnExpr.lhs       |    2 +-
 compiler/rename/RnTypes.lhs      |    2 +-
 compiler/typecheck/TcArrows.lhs  |    9 ++++++---
 compiler/typecheck/TcBinds.lhs   |    4 ++--
 compiler/typecheck/TcHsSyn.lhs   |    7 ++++---
 compiler/typecheck/TcMatches.lhs |   14 ++++++++------
 15 files changed, 70 insertions(+), 67 deletions(-)

and

commit 74d401860d6a28244b9a12fca844fe14a6a04274
Author: Simon Peyton Jones <[email protected]>
Date:   Fri Jan 4 10:30:53 2013 +0000

    Switch on -XEmptyCase when renaming derived declarations
    
    Compiler-generated code can have empty cases

>---------------------------------------------------------------

 compiler/typecheck/TcDeriv.lhs |    4 +++-
 1 files changed, 3 insertions(+), 1 deletions(-)

comment:15 Changed 10 months ago by Herbert Valerio Riedel <hvr@…>

In a97f90cecb6351a6db5a62c1551fcbf079b0acdd/ghc:

Add Data.Void to base (re #9814)

This adds the module `Data.Void` (formerly provided by Edward Kmett's `void`
package) to `base`.

The original Haskell98 compatible implementation has been modified to use
modern GHC features (among others this makes use of `EmptyCase` as
motivated by #2431), and `vacuousM` was dropped since it's redundant now
with the AMP in place.  Instances for classes not part of `base` had to be
dropped as well.

TODO: Documentation could be improved

Reviewed By: ekmett, austin

Differential Revision: https://phabricator.haskell.org/D506
Note: See TracTickets for help on using tickets.