Write a function with an empty case without case

user_1378868 0
Viewed 154

I can write something impossible with an empty case, and use it with Decision, for example.

{-# LANGUAGE DataKinds, EmptyCase, LambdaCase, TypeOperators #-}

import Data.Type.Equality
import Data.Void

data X = X1 | X2

f :: X1 :~: X2 -> Void
f = \case {}
-- or
-- f x = case x of {}

Is there a way to write the equivalent without using case by directly pattern-matching the parameter?

f :: X1 :~: X2 -> Void
f ???
haskell
3 Answers

Well, you can use a horrible CPP hack:

{-# LANGUAGE CPP #-}
#define Absurd      = \case {}

f :: X1 :~: X2 -> Void
f Absurd   -- expands to "f = case {}"

However, if you're looking for a solution using pure Haskell syntax, I'm pretty sure the answer is no. Unlike with an empty case, you can't define f using pattern syntax without at least one pattern. And, there's no pattern that GHC understands as secret code for a term of uninhabited type. (Even if there was, there's no syntax that allows you define an f pat without a right-hand side.)

user_72030160

Here's an attempt using pattern synonyms. It is not completely satisfactory and probably not what you really want. It only achieves in moving the \case{} away from your eye. We still need to use absurd in some points.

{-# LANGUAGE PatternSynonyms, ViewPatterns, GADTs #-}
{-# LANGUAGE DataKinds, EmptyCase, LambdaCase, TypeOperators #-}

import Data.Type.Equality
import Data.Void

data X = X1 | X2

pattern Abs :: Void -> a
pattern Abs x <- (\case{} -> x)

f :: 'X1 :~: 'X2 -> Void
f (Abs x) = x

g :: 'X1 :~: 'X2 -> a
g (Abs x) = absurd x

{-
    Pattern match(es) are non-exhaustive
    In an equation for `h':
        Patterns of type 'X1 :~: 'X1 not matched: Refl
-}
h :: 'X1 :~: 'X1 -> Void
h (Abs x) = x

Another alternative could be exploiting Template Haskell.

user_32349590

I think if you want to imitate this, the simplest way is akin to an answer posted in the comments:

f _ = undefined

However, this is lazy:

f (error "aw beans")  -- undefined

While the empty case is strict:

(\ case {} :: X1 :~: X2 -> Void) (error "aw beans")  -- beans

So a better replacement would use seq:

impossible :: a -> Void
impossible x = x `seq` impossible x

Or BangPatterns:

{-# Language BangPatterns #-}

impossible :: a -> Void
impossible !x = impossible x

Whereupon you can just write f = impossible, which seems pretty good to me. (The quantifier on a is logically more like “for any” than “for all”, but oh well.) You could of course throw something slightly more descriptive instead of going into an infinite loop in case the situation isn’t actually impossible—error "the impossible was possible after all".

This should also work with the old-fashioned definition of Void as data Void = Void !Void or newtype Void = Void Void in the void package.

user_2468860
Related