Lens.Family.Total

This module lets you exhaustively pattern match on types using Lenses, Traversals, or Prisms.

Here's an example use of this library:

import Lens.Family.Total
import Lens.Family.Stock

total :: Either Char Int -> String       -- Same as:
total = _case                            -- total = \case
    & on _Left  (\c -> replicate 3  c )  --     Left  c -> replicate 3 c
    & on _Right (\n -> replicate n '!')  --     Right n -> replicate n '!'

Our total function pattern matches exhaustively on the Either type using the _Left and _Right prisms:

>>> total (Left 'X')
"XXX"
>>> total (Right 2)
"!!"

The types ensure that the above function is total. For example, if you omit the _Right branch:

partial :: Either Char Int -> String
partial = _case
    & on _Left  (\c -> replicate 3  c )

... then you will get the following type error:

No instance for (Empty Int) arising from a use of ‘_case’
In the first argument of ‘(&)’, namely ‘_case’
In the expression: _case & on _Left (\ c -> replicate 3 c)
In an equation for ‘partial’:
    partial = _case & on _Left (\ c -> replicate 3 c)

That type error means that you didn't pattern match on the branch with the Int.

You can also implement exhaustive pattern matching for your own data types with Traversals or Prisms. However, this only works if you have one type variable for each branch of your type:

{-# LANGUAGE DeriveGeneric   #-}
{-# LANGUAGE TemplateHaskell #-}

import Control.Lens.TH
import GHC.Generics (Generic)
import Lens.Family.Total

data Example a b c = C1 a | C2 b | C3 c deriving (Generic)

makePrisms ''Example

instance (Empty a, Empty b, Empty c) => Empty (Example a b c)

example :: Example String Char Int -> String  -- Same as:
example = _case                               -- example = \case
    & on _C1 (\s -> s              )          --     C1 s -> s
    & on _C2 (\c -> replicate 3  c )          --     C2 c -> replicate 3  c
    & on _C3 (\n -> replicate n '!')          --     C3 n -> replicate n '!'

There is no way to prove that the pattern match is exhaustive unless there is a type parameter for every branch. This is because each successive pattern match Voids out that branch's type parameter to prove that the branch no longer needs to be handled. _case just verifies that all type parameters are Void.

You can still write an inexhaustive pattern match so long as you provide a default:

example :: Example Int String Float -> String
example = _default "default"
    & on _C2 (\s -> s)

You can even pattern match using Lenses, too:

example :: (Int, Char) -> String     -- Same as:
example = _case                      -- example = \case
    & on _1 (\n -> replicate n '1')  --     (n, _) -> replicate n '1'

... and of course the identity lens (id) works, too:

example :: (Int, Char) -> String        -- Same as:
example = _case                         -- example = \case
    & on id (\(n, c) -> replicate n c)  --     (n, c) -> replicate n c

Documentation

class Empty a where

A type class for uninhabited types

Minimal complete definition

Nothing

Methods

impossible :: a -> x

impossible :: (Generic a, GEmpty (Rep a)) => a -> x

Instances

Empty Void

Defined in Lens.Family.Total

Methods

impossible :: Void -> x

(Empty a, Empty b) => Empty (Either a b)

Defined in Lens.Family.Total

Methods

impossible :: Either a b -> x

Empty a => Empty (a, b)

Defined in Lens.Family.Total

Methods

impossible :: (a, b) -> x

class GEmpty f where

Methods

gimpossible :: f a -> x

Instances

GEmpty (V1 :: Type -> Type)

Defined in Lens.Family.Total

Methods

gimpossible :: V1 a -> x

Empty a => GEmpty (K1 i a :: Type -> Type)

Defined in Lens.Family.Total

Methods

gimpossible :: K1 i a a0 -> x

(GEmpty a, GEmpty b) => GEmpty (a :+: b)

Defined in Lens.Family.Total

Methods

gimpossible :: (a :+: b) a0 -> x

GEmpty a => GEmpty (a :*: b)

Defined in Lens.Family.Total

Methods

gimpossible :: (a :*: b) a0 -> x

GEmpty a => GEmpty (M1 i c a)

Defined in Lens.Family.Total

Methods

gimpossible :: M1 i c a a0 -> x

_case :: Empty a => a -> x

Synonym for impossible, used to check if a pattern match is exhaustive

_default :: x -> a -> x

Synonym for const, used to provide a default if a pattern match is inexhaustive

on :: ((a -> Either a Void) -> s -> Either a r) -> (a -> o) -> (r -> o) -> s -> o

Pattern match on a Traversal

(&) :: a -> (a -> b) -> b infixl 1

& is a reverse application operator. This provides notational convenience. Its precedence is one higher than that of the forward application operator $, which allows & to be nested in $.

>>> 5 & (+1) & show
"6"

Since: base-4.8.0.0

Re-exports

data Void

Uninhabited data type

Since: base-4.8.0.0

Instances

Eq Void

Since: base-4.8.0.0

Defined in Data.Void

Methods

(==) :: Void -> Void -> Bool

(/=) :: Void -> Void -> Bool

Data Void

Since: base-4.8.0.0

Defined in Data.Void

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Void -> c Void

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Void

toConstr :: Void -> Constr

dataTypeOf :: Void -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Void)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Void)

gmapT :: (forall b. Data b => b -> b) -> Void -> Void

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Void -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Void -> r

gmapQ :: (forall d. Data d => d -> u) -> Void -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Void -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Void -> m Void

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Void -> m Void

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Void -> m Void

Ord Void

Since: base-4.8.0.0

Defined in Data.Void

Methods

compare :: Void -> Void -> Ordering

(<) :: Void -> Void -> Bool

(<=) :: Void -> Void -> Bool

(>) :: Void -> Void -> Bool

(>=) :: Void -> Void -> Bool

max :: Void -> Void -> Void

min :: Void -> Void -> Void

Read Void

Reading a Void value is always a parse error, considering Void as a data type with no constructors.

Since: base-4.8.0.0

Defined in Data.Void

Methods

readsPrec :: Int -> ReadS Void

readList :: ReadS [Void]

readPrec :: ReadPrec Void

readListPrec :: ReadPrec [Void]

Show Void

Since: base-4.8.0.0

Defined in Data.Void

Methods

showsPrec :: Int -> Void -> ShowS

show :: Void -> String

showList :: [Void] -> ShowS

Ix Void

Since: base-4.8.0.0

Defined in Data.Void

Methods

range :: (Void, Void) -> [Void]

index :: (Void, Void) -> Void -> Int

unsafeIndex :: (Void, Void) -> Void -> Int

inRange :: (Void, Void) -> Void -> Bool

rangeSize :: (Void, Void) -> Int

unsafeRangeSize :: (Void, Void) -> Int

Generic Void

Defined in Data.Void

Associated Types

type Rep Void :: Type -> Type

Methods

from :: Void -> Rep Void x

to :: Rep Void x -> Void

Semigroup Void

Since: base-4.9.0.0

Defined in Data.Void

Methods

(<>) :: Void -> Void -> Void

sconcat :: NonEmpty Void -> Void

stimes :: Integral b => b -> Void -> Void

Exception Void

Since: base-4.8.0.0

Defined in Data.Void

Methods

toException :: Void -> SomeException

fromException :: SomeException -> Maybe Void

displayException :: Void -> String

Empty Void

Defined in Lens.Family.Total

Methods

impossible :: Void -> x

type Rep Void

Since: base-4.8.0.0

Defined in Data.Void

type Rep Void = D1 (MetaData "Void" "Data.Void" "base" False) (V1 :: Type -> Type)