data Type = Ty String | Sum (Type, Type) | Prod (Type, Type) | Fix (String, Type) | FApp (Type, String, Type) deriving Eq

instance Show Type where
	show (Ty "unit")      = "1"
	show (Ty "void")      = "0"
	show (Ty v)           = v
	show (Sum  (t1, t2))  = (show t1) ++ "+" ++ (show t2)
	show (Prod (t1, t2))  = (show t1) ++ "*" ++ (show t2)
	show (Fix  (v,  ty))  = "mu " ++ v ++ "." ++ (show ty)
	show (FApp (t, x, s)) = "[" ++ (show t) ++ "|" ++ x ++ "=" ++ (show s) ++ "]"

d ty x = flatten (csimplify (derivative ty x))

derivative (Ty v) x | x == v   = Ty "unit"
derivative (Ty v)            x = Ty "void"
derivative (Sum  (t1, t2))   x = Sum (derivative t1 x, derivative t2 x)
derivative (Prod (t1, t2))   x = Sum (Prod (derivative t1 x, t2), Prod (t1, derivative t2 x))
derivative rty@(Fix (v, ty)) x = let z = unique_name rty in Fix (z, Sum (FApp (derivative ty x, v, rty), Prod (FApp (derivative ty v, v, rty), Ty z)))
derivative (FApp (t, y, s))  x = Sum (FApp(derivative t x, y, s), Prod (FApp (derivative t y, y, s), derivative s x))

simplify (Sum  (Ty "void", x))    = simplify x
simplify (Sum  (x, Ty "void"))    = simplify x
simplify (Sum  (x, y))            = Sum (simplify x, simplify y)
simplify (Prod (Ty "void", x))    = Ty "void"
simplify (Prod (x, Ty "void"))    = Ty "void"
simplify (Prod (Ty "unit", x))    = simplify x
simplify (Prod (x, Ty "unit"))    = simplify x
simplify (Prod (x, y))            = Prod (simplify x, simplify y)
simplify (Fix  (v, ty))           | not (v `member` names ty) = ty
simplify (Fix  (v, ty))           = Fix (v, simplify ty)
simplify (FApp (t, y, s))         | not (y `member` names t) = t
simplify (FApp (t, y, s))         = FApp (simplify t, y, simplify s)
simplify x                        = x

fixed_point f x | x == (f x) = x
fixed_point f x              = fixed_point f (f x)

csimplify x = fixed_point simplify x

flatten ty = distribute Nothing ty
	where
		  distribute Nothing    t@(Ty _)           = t
		  distribute (Just lty) t@(Ty _)           = Prod (lty, t)
		  distribute mlty         (Sum  (t1, t2))  = Sum (distribute mlty t1, distribute mlty t2)
		  distribute mlty         (Prod (t1, t2))  = distribute (Just (distribute mlty t1)) t2
		  distribute Nothing      (Fix  (v,  ty))  = Fix (v, distribute Nothing ty)
		  distribute (Just lty) t@(Fix  (v,  ty))  = Prod (lty, distribute Nothing t)
		  distribute Nothing      (FApp (t, x, s)) = FApp (distribute Nothing t, x, distribute Nothing s)
		  distribute (Just lty) t@(FApp (f, x, s)) = Prod (lty, distribute Nothing t)

unique_name ty = choose fnames
	where vnames       = names ty
	      fnames       = set_difference (map (\x->[x]) "abcdefghijklmnopqrstuvwxyz") vnames
	      tname i      = "t" ++ (show i)
	      choose (n:_) = n
	      choose []    = tname (fixed_point (\i -> if (tname i `member` vnames) then i+1 else i) 0)

names (Ty x)           = [x]
names (Sum (t1, t2))   = (names t1) ++ (names t2)
names (Prod (t1, t2))  = (names t1) ++ (names t2)
names (Fix (v, ty))    = v:(names ty)
names (FApp (t, v, s)) = (v:(names t)) ++ (names s)

member x []              = False
member x (y:ys) | x == y = True
member x (_:ys)          = member x ys

set_difference xs ys = filter (\x -> not (x `member` ys)) xs

list = Fix ("X", Sum (Ty "unit", Prod (Ty "int", Ty "X")))
tree = Fix ("X", Sum (Ty "int", Prod (Ty "X", Ty "X")))