Sample infinite loop reduction

Question

My goal is to exclude () from terms, for example:

 (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 xy) = If (x == Simplify x && y == Simplify y) (op xy) (Simplify (op (Simplify x) (Simplify y))) Simplify x = x 

However, try:

 :kind! Simplify (String, Int) 

... leads to an infinite loop in type control. I think a family like If should take care of irreducible terms, but I'm obviously missing something. But what?

Answer 1

The type of family evaluation is not lazy, therefore If ctf will evaluate all c , t and f . (Actually, the order in which the family order is determined is not really defined right now.) Therefore, it is not surprising that you have finished an endless cycle - you always evaluate Simplify (op (Simplify x) (Simplify y)) , even when this Simplify (op xy) !

You can avoid this by splitting recursion and simplification into parts, for example:

 {-# 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 xy) = op (Simplify1 x) (Simplify1 y) Simplify1 x = x type family SimplifyFix xx' where SimplifyFix xx = x SimplifyFix xx' = SimplifyFix x' (Simplify1 x') type Simplify x = SimplifyFix x (Simplify1 x) 

The idea is this:

• Simplify1 takes one simplification step.
• SimplifyFix takes x and its one-step simplification x' , checks to see if they are equal, and if they do not take another simplification step (thus finding a fixed point Simplify1 ).
• Simplify just starts with the SimplifyFix chain with a call to Simplify1 .

Since matching patterns of a type family is lazy, SimplifyFix correctly delays the evaluation, preventing infinite loops.

And really:

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

Answer 2

I thought I would mention that, given that simplification has a fold structure, there is no need to construct this complex solution using a fixed point that crosses the expression over and over again.

It will be wonderful:

 {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} module Simplify where type family Simplify x where Simplify (op ab) = Op op (Simplify a) (Simplify b) Simplify x = x type family Op op ab where Op op () b = b Op op a () = a Op op ab = op ab