Type reduction infinite loop

Question

My aim is to eliminate () from terms, like this:

(a, b)       -> (a, b)
((), b)      -> b
(a, ((), b)) -> (a, b)
...

And this is the code:

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module Simplify where

import Data.Type.Bool
import Data.Type.Equality

type family Simplify x where
  Simplify (op () x) = Simplify x
  Simplify (op x ()) = Simplify x
  Simplify (op x y)  = If (x == Simplify x && y == Simplify y)
                          (op x y)
                          (Simplify (op (Simplify x) (Simplify y)))
  Simplify x         = x

However, trying it out:

:kind! Simplify (String, Int)

...leads to an infinite loop in the type checker. I'm thinking the If type family should be taking care of irreducible terms, but I'm obviously missing something. But what?

Answer 1

Type family evaluation isn't lazy, so If c t f will evaluate all of c, t, and f. (In fact, type family evaluation order isn't really defined at all right now.) So it's no wonder you end up with an infinite loop – you always evaluate Simplify (op (Simplify x) (Simplify y)), even when that's Simplify (op x y)!

You can avoid this by splitting the recursion and the simplification apart, like so:

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module Simplify where

import Data.Type.Bool
import Data.Type.Equality

type family Simplify1 x where
  Simplify1 (op () x) = x
  Simplify1 (op x ()) = x
  Simplify1 (op x y)  = op (Simplify1 x) (Simplify1 y)
  Simplify1 x         = x

type family SimplifyFix x x' where
  SimplifyFix x x  = x
  SimplifyFix x x' = SimplifyFix x' (Simplify1 x')

type Simplify x = SimplifyFix x (Simplify1 x)

The idea is:

1. Simplify1 does one step of simplification.
2. SimplifyFix takes x and its one-step simplification x', checks if they're equal, and if they aren't does another step of simplification (thus finding the fixed point of Simplify1).
3. Simplify just starts off the SimplifyFix chain with a call to Simplify1.

Since type family pattern matching is lazy, SimplifyFix correctly delays evaluation, preventing infinite loops.

And indeed:

*Simplify> :kind! Simplify (String, Int)
Simplify (String, Int) :: *
= (String, Int)

*Simplify> :kind! Simplify (String, ((), (Int, ())))
Simplify (String, ((), (Int, ()))) :: *
= ([Char], Int)