Add empty data proposal

[quchen]

Rendered version: https://github.com/quchen/rfcs/blob/empty-data/texts/0000-empty-data.rst

[quchen]

Interesting, @hvr. But the Report does not specify what the extension does, is that correct? This would degenerate this proposal to a to-do marker to add this properly to the spec.

[goldfirere]

Haskell 2010 includes empty data declarations (what's missing in the spec? They're just data declarations with no constructors) but not empty case. So I believe this degenerates to an inclusion of empty case. Do you agree?

[goldfirere]

We also must specify that the empty-case must always be strict in the scrutinee. Otherwise,

let v :: Void
    v = error "blargh"
in case v of {}

will yield an incomplete pattern-match exception instead of blargh, as it should.

[quchen]

case v :: Void of {}

will yield an incomplete pattern-match exception

Although it would not be incorrect to throw an incomplete pattern exception here, I’m assuming what you want is the “right” exception?

[goldfirere]

Yes, that's right. Evaluating the scrutinee gives the more informative exception, in my opinion... because the pattern-match is actually complete. This is what GHC already does today; I just wanted to clarify the proposal.

[quchen]

So is it correct that the following rule would have the desired properties, @goldfirere? What should we do if v is not nullary?

Section 3.17.3, Formal semantics of pattern matching

case v of {}
  = v

where v is a value of an uninhabited type

[goldfirere]

Not quite. I propose

Section 3.17.3, Formal semantics of pattern matching

case v of {}
  = v `seq` error "No match"

I believe that covers all cases.

While we're here, I noticed a bug in the report: The first sentence of 3.17.2 is "Patterns are matched against values." But this is false! case undefined of _ -> () evaluates to (), matching the pattern _ against the non-value undefined. This is handled correctly in the formal semantics.

[quchen]

@goldfirere That translation isn’t correct yet, since the compiler may arbitrarily choose which argument of seq to force first, thus yielding the less helpful “No match” error in all cases. More info here.

[cartazio]

I recall some remarks or discussion somewhere that seq should perhaps have the semantics of pseq, or something to that effect. Is that relevant for this ?

On Friday, August 26, 2016, David Luposchainsky notifications@github.com wrote:

@goldfirere https://github.com/goldfirere That translation isn’t correct yet, since the compiler may arbitrarily choose which argument of seq to force first. More info here. https://github.com/quchen/articles/blob/master/fbut.md#seq-does-not-specify-an-evaluation-order

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/haskell/rfcs/pull/5#issuecomment-242753890, or mute the thread https://github.com/notifications/unsubscribe-auth/AAAQwoVQaZo7Z0aRUV1MujS_m4DGPpcaks5qjvqkgaJpZM4JgPgh .

[goldfirere]

@quchen: Good point. :(

[quchen]

@goldfirere I think we only need to handle the other case, namely when the value is inhabited, as well. New rule suggestion:

case v of {} = v -- if v is an empty type
             = error "No match" -- otherwise

[goldfirere]

How do we know when a type is empty? For example:

data C where
   MkC :: 1 `NotIn` CollatzSequence n => Proxy n -> C

No human (to my knowledge) knows whether or not C is empty. We can't have our semantics depend on type inhabitation.

On the other hand, we could just say

case v of {}
  = v `pseq` error "No match"

That works. But it means we now need to specify pseq.

[cartazio]

Hrm, I think José and one or two other folks were in favor is formalizing pseq (though I guess I'm repeating myself)

Is the semantic difference of seq vs pseq articulated anywhere? When would code benefit from seq rather than pseq? My understanding is that seq provides a weaker order of reduction to whnf guarantee vs pseq, whereas pseq guarantees that the first Argument will be reduced to whnf BEFORE the result argument

On Tuesday, August 30, 2016, Richard Eisenberg notifications@github.com wrote:

How do we know when a type is empty? For example:

data C where MkC :: 1 NotIn CollatzSequence n => Proxy n -> C

No human (to my knowledge) knows whether or not C is empty. We can't have our semantics depend on type inhabitation.

On the other hand, we could just say

case v of {} = v pseq error "No match"

That works. But it means we now need to specify pseq.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/haskell/rfcs/pull/5#issuecomment-243532636, or mute the thread https://github.com/notifications/unsubscribe-auth/AAAQwu3Hn4g_aBew-60edlr95LC1tnozks5qlHTngaJpZM4JgPgh .

[augustss]

I really don't like the idea of case evaluating the scrutinee. It's totally irregular compared to how case is explained now.

On Tuesday, August 30, 2016, Richard Eisenberg notifications@github.com wrote:

How do we know when a type is empty? For example:

data C where MkC :: 1 NotIn CollatzSequence n => Proxy n -> C

No human (to my knowledge) knows whether or not C is empty. We can't have our semantics depend on type inhabitation.

On the other hand, we could just say

case v of {} = v pseq error "No match"

That works. But it means we now need to specify pseq.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/haskell/rfcs/pull/5#issuecomment-243532636, or mute the thread https://github.com/notifications/unsubscribe-auth/AFAInv5Onax_xRu8cmgZrnuybKBe_tikks5qlHTogaJpZM4JgPgh .

[goldfirere]

I don't like it from a theory standpoint, but I also don't like case (error "urk" :: Void) of {} throwing an incomplete-pattern-match exception. The pattern match most certainly is complete! Evaluating the scrutinee seems better from a user standpoint, even if I agree that it is a design wart.

[augustss]

I don't think we need to specify exactly what error we will get I that situation. Just as (error "a" + error "b") is non-deterministic, we can leave case on an empty type non-deterministic.

On Friday, September 2, 2016, Richard Eisenberg notifications@github.com wrote:

I don't like it from a theory standpoint, but I also don't like case (error "urk" :: Void) of {} throwing an incomplete-pattern-match exception. The pattern match most certainly is complete! Evaluating the scrutinee seems better from a user standpoint, even if I agree that it is a design wart.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/haskell/rfcs/pull/5#issuecomment-244396329, or mute the thread https://github.com/notifications/unsubscribe-auth/AFAInrv-2rNXj6kuy0r1nyv-NAbwUe32ks5qmDdcgaJpZM4JgPgh .

[goldfirere]

Isn't your suggestion precisely

case v of {}
  = v `seq` error "No match"

? Due to the lack of tight specification for seq, this should do what you just suggested. I feel I'm missing something here, though.

[quchen]

Good point, @goldfirere. Using seq might give implementors actually more flexibility here!

[augustss]

Excellent point.

On Friday, September 2, 2016, David Luposchainsky notifications@github.com wrote:

Good point, @goldfirere https://github.com/goldfirere. Using seq might give implementors actually more flexibility here!

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/haskell/rfcs/pull/5#issuecomment-244478122, or mute the thread https://github.com/notifications/unsubscribe-auth/AFAIntI5L0bmwnSc8d1djgci3zkV6GC0ks5qmIUYgaJpZM4JgPgh .

[wrengr]

@cartazio I believe it's articulated in the paper where pseq was first introduced. AFAICR: seq ensures that the left argument is forced some time before the whole seq expression returns a value (but this may be before, after, or interleaved with evaluation of the right argument), whereas pseq ensures that the left argument is forced (and finishes) before starting evaluation of the right argument.

The advantage of the weaker requirements on seq is, of course, that it gives compiler-writers more wiggle room and so could allow for better performance.

[quchen]

@wrengr seq does not even guarantee that: if seq x y finds out that y is bottom, then the result is bottom, regardless of x. The only way we can force a (sufficiently strange) compiler to check the x is by showing it that y is not bottom.

[yav]

What use case are we trying to support by adding the implicit seq to the translation of empty case?

[goldfirere]

Without the seq, then case (error "I have type Void" :: Void) of {} would reduce to error "Incomplete match", even thought the match is actually complete! It's the construction of a term of type Void that's the problem.

[yav]

Well, the error does not have to say "Incomplete match", it could be "Evaluated an empty case". I see that it might be preferable to pick the user error though. Hm.