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?
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:
Simplify1
does one step of simplification.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
).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)
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With