# 7. Constructor removal/transformation¶

Removing constructors from an EADT is equivalent to transforming every instance of these constructors into other constructors of another EADT.

We consider 3 cases:

Fixed input EADT type; fixed list of constructors to act on

Generic input EADT type; fixed list of constructors to act on

Generic input EADT type; extensible list of constructors to act on

Note in the 3 cases we need to specify the resulting EADT type as it could be anything fulfilling the constraints.

## 7.1. Fixed input, fixed matches¶

If the type of the input EADT is fixed, we can use safe pattern-matching as follows:

```
-- replace Even and Odd constructors with a Cons constructor
removeOddEven l = l >:>
(\(EvenF a r) -> Cons a r
,\(OddF a r) -> Cons a r
,\NilF -> Nil
)
eo :: EADT '[EvenF Int, OddF Int, NilF]
eo = Even (10 :: Int) $ Odd (5 :: Int) $ Odd (7 :: Int) Nil
> eadtShow (cata removeOddEven eo :: List Int)
"10 : 5 : 7 : Nil"
```

Note that `removeOddEven`

only works on a specific EADT. If we want it to work on
any EADT that contains `Even`

and `Odd`

constructors, read the following
sections.

## 7.2. Generic input, fixed matches¶

If we want `removeEvenOdd`

to work on input EADTs of any type, we can extract
the constructors that we are interested in with `splitVariantF`

and lift the
left-over constructors with `liftVariantF`

as follows:

```
removeOddEven x = case splitVariantF @'[EvenF Int, OddF Int] x of
-- replace Even and Odd constructors with a Cons constructor
Right v -> v >:>
( \(EvenF a l) -> Cons a l
, \(OddF a l) -> Cons a l
)
-- do nothing to the other constructors
Left leftovers -> EADT (liftVariantF leftovers)
eo1 :: EADT '[EvenF Int, OddF Int, NilF]
eo1 = Even (10 :: Int) $ Odd (5 :: Int) $ Odd (7 :: Int) Nil
> eadtShow (cata removeOddEven eo1 :: List Int)
"10 : 5 : 7 : Nil"
-- additional `ConsF Int` constructor
eo2 :: EADT '[ConsF Int, EvenF Int, OddF Int, NilF]
eo2 = Even (10 :: Int) $ Cons (5 :: Int) $ Odd (7 :: Int) Nil
> eadtShow (cata removeOddEven eo2 :: List Int)
"10 : 5 : 7 : Nil"
```

## 7.3. Generic input, extensible matches¶

If we want the `removeOddEven`

pattern match to be extensible, we can use
type-classes with an overlappable instance handling the generic case (i.e. that
only transfers constructors from one EADT to another without modifying them).

```
class RemoveOddEven ys (f :: * -> *) where
removeOddEven :: f (EADT ys) -> EADT ys
-- replace Odd and Even with Cons
instance ConsF a :<: ys => RemoveOddEven ys (OddF a) where
removeOddEven (OddF a l) = Cons a l
instance ConsF a :<: ys => RemoveOddEven ys (EvenF a) where
removeOddEven (EvenF a l) = Cons a l
-- handle the combinator
instance
( AlgVariantF (RemoveOddEven ys) (EADT ys) xs
) => RemoveOddEven ys (VariantF xs)
where
removeOddEven = algVariantF @(RemoveOddEven ys) removeOddEven
-- handle remaining constructors
instance {-# OVERLAPPABLE #-} f :<: ys => RemoveOddEven ys f where
removeOddEven = VF -- keep the other constructors unmodified
```

Test:

```
eo :: EADT '[EvenF Int, OddF Int, NilF]
eo = Even (10 :: Int) $ Odd (5 :: Int) $ Odd (7 :: Int) Nil
> eadtShow (cata removeOddEven eo :: List Int)
"10 : 5 : 7 : Nil"
-- EADT with an additional `ConsF Int` constructor
eo2 :: EADT '[ConsF Int, EvenF Int, OddF Int, NilF]
eo2 = Even (10 :: Int) $ Odd (5 :: Int) $ Cons (7 :: Int) $ Odd (7 :: Int) Nil
> eadtShow (cata removeOddEven eo2 :: List Int)
"10 : 5 : 7 : 7 : Nil"
-- EADT with an additional `ConsF String` constructor
eo3 :: EADT '[ConsF Int, EvenF Int, OddF Int, ConsF String, NilF]
eo3 = Even (10 :: Int) $ Cons "Test" $ Odd (5 :: Int) $ Cons (7 :: Int) $ Odd (7 :: Int) Nil
> eadtShow (cata removeOddEven eo3 :: EADT '[ConsF Int, ConsF String, NilF])
"10 : \"Test\" : 5 : 7 : 7 : Nil"
```

We can extend `removeOddEven`

to support other constructors by adding new
instances of `RemoveOddEven`

for them.