Rewriting Calculus with(out) Types