Type reduction infinite loop

8
votes

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?

2
haskellinfinite-looptypecheckingtype-families
It seems you are assuming that type-level computation is lazy, hence that the second branch of the If won't be evaluated unless it is needed. I think that assumption is unwarranted. - Daniel Wagner
And by the way: being polymorphic over op is probably wrong. For example, Simplify (Either () Int) probably should not reduce to Int. - Daniel Wagner
What should the behaviour be on (String, (), Int)? Both solutions suggested so far reduce that to Int. I don't even know if it's possible to get (String, Int). - gallais
@gallais: That's fine, terms can be (nested) tuples only. - Philip Kamenarsky

2 Answers

10
votes

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)
3
votes

I thought I'd mention that given that the simplification has the structure of a fold, there is no need to build this complex solution involving a fixpoint which re-traverses the expression again and again.

This will do just fine:

{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE UndecidableInstances #-}
module Simplify where

type family Simplify x where
  Simplify (op a b) = Op op (Simplify a) (Simplify b)
  Simplify x        = x

type family Op op a b where
  Op op () b = b
  Op op a () = a
  Op op a b  = op a b