Data.Yoko.SmartPreciseCase

Using some McBride "Faking It" style trickery to make precise_case polyvariadic in the ad-hoc cases.

E.g.

 precise_case x (\(C_ a b) -> special_case a b) (Default $ \x -> generic_function x)

and

 precise_case x (\(C_ a b) -> special_case a b) (\(D_ x) -> special_case2 x) (Default $ \x -> generic_function x)

both work.

Documentation

class Error_precise_case_requires_at_least_1_special_case a

data AdHoc dcs dt r

Constructors

AdHoc dt (dcs -> r)

Instances

(DT dt, ~ * dt (Codomain dcs), ~ * dt (Codomain (DCs dt)), Partition (DCs dt) dcs (:-: (DCs dt) dcs), ~ * x (:-: (DCs dt) dcs -> r), ~ * final r) => Builder (AdHoc dcs dt r) (Default x -> final)

(~ * dt (Codomain dc), ~ * dt (Codomain dcs), ~ * r r', Builder (AdHoc (:+: dcs (N dc)) dt r) bldr) => Builder (AdHoc dcs dt r) ((dc -> r') -> bldr)

newtype Default a

Constructors

Default a

Instances

Error_precise_case_requires_at_least_1_special_case () => Builder (Start dt) (Default a -> b)

(DT dt, ~ * dt (Codomain dcs), ~ * dt (Codomain (DCs dt)), Partition (DCs dt) dcs (:-: (DCs dt) dcs), ~ * x (:-: (DCs dt) dcs -> r), ~ * final r) => Builder (AdHoc dcs dt r) (Default x -> final)

class Builder adhoc bldr where

Methods

precise_case_ :: adhoc -> bldr

Instances

(~ * dt (Codomain dc), Builder (AdHoc (N dc) (Codomain dc) r) bldr) => Builder (Start dt) ((dc -> r) -> bldr)

Error_precise_case_requires_at_least_1_special_case () => Builder (Start dt) (Default a -> b)

(DT dt, ~ * dt (Codomain dcs), ~ * dt (Codomain (DCs dt)), Partition (DCs dt) dcs (:-: (DCs dt) dcs), ~ * x (:-: (DCs dt) dcs -> r), ~ * final r) => Builder (AdHoc dcs dt r) (Default x -> final)

(~ * dt (Codomain dc), ~ * dt (Codomain dcs), ~ * r r', Builder (AdHoc (:+: dcs (N dc)) dt r) bldr) => Builder (AdHoc dcs dt r) ((dc -> r') -> bldr)

newtype Start dt

Constructors

Start dt

Instances

(~ * dt (Codomain dc), Builder (AdHoc (N dc) (Codomain dc) r) bldr) => Builder (Start dt) ((dc -> r) -> bldr)

Error_precise_case_requires_at_least_1_special_case () => Builder (Start dt) (Default a -> b)

precise_case :: Builder (Start dt) bldr => dt -> bldr