This is a good start and your calculation works out, but the standard literature wouldn't agree on your suggestion that Tom destroyed is of type t. The crucial point is that that the moved-away pronoun makes the phrase something that's missing an entity to become a sentence with a truth value, so in accordance with your lambda abstraction, which is expecting an individual argument to produce a truth value, this relative predication Tom destroyed would be of type <e,t>. In the tree, the verb destroy does not actually pick up the value of the trace to combine to <e,t>, but will remain with the object position unsatisfied.
The motivation behind this is, I imagine, that if you moved the which to a different position, you can't just squeeze out its semantic content twice and use it simulateneously as a relative pronoun and as an object to the verb phrase. It's one syntactic object that can only contribute to the meaning of the sentence once. So in the type decomposition, since the element indexed by i now serves its purpose as the specifier of the TP and can thus no longer contribute any semantic content to the completion of the VP in object position, it will be treated semantically as if it wasn't there in its original node. (Though we know that syntactically, the position will remain occupied with the trace blocking any other syntactic elements from filling the slot.)
Let's break it down step by step:
In the following (alternative see below), I will follow your suggestion that syntactically, car is an NP which first combines with the CP which Tom destroyed to another NP, to which afterwards the determiner the is applied to produce a DP:
[DP
[D [the]]
[NP
[NP [car]]
[CP [which Tom destroyed]] ]
As you correctly figured out, relative clauses act as predicate modifiers, and are thus of type <<e,t>,<e,t>>: They take an NP of type <e,t> and produce another NP <e,t>, which then combines with the determiner the to form a DP of type e:
| the car which Tom destroyed |
| | <e,t> | <<e,t>,<e,t>> |
| <<e,t>,e> | <e,t> |
| <e> |
So if the (possibly phonetically empty) relative pronoun (which) is to be an operator that is applied to the relative predication (Tom destroyed) to yield the relative clause (which Tom destroyed), it should be of type <σ,<<e,t>,<e,t>>>, where σ is the type of the relative predication:
| the car which Tom destroyed |
| | | <σ,<<e,t>,<e,t>>> | σ |
| | <e,t> | <<e,t>,<e,t>> |
| <<e,t>,e> | <e,t> |
| <e> |
The relative predication is something that's missing an individual (the "trace") to become a sentence with a truth value: {x: Tom destroyed x}. This is dreivable from the fact that destroyed is a two-place verb (type<e,<e,t>>) that so far has been fed one individual (Tom: type e), thus our σ is the type <e,t>:
| the car which Tom destroyed |
| | | | e | <e,<e,t>> |
| | | <<e,t>,<<e,t>,<e,t>>> | <e,t> |
| | <e,t> | <<e,t>,<e,t>> |
| <<e,t>,e> | <e,t> |
| <e> |
Eventually, we get that the relative pronouns must be of type <<e,t>,<<e,t>,<e,t>>>.
There should be no difference between which, who, that, and a phonetically empty ∅ -- they all have the same type-compositional behavior. I don't follow why you assume that that should be of type <t,t> or what you men by "semantically vacuous"; you'd have to elaborate more on that.
Some may prefer an analysis where the relative clause is only attached after the NP already combined with the determiner:
[DP
[DP
[D [the]]
[NP [car]] ]
[CP [which Tom destroyed]] ]
In this case, 1) for definite DPs (the car) which have type e: the relative clause must be of type <e,e> and the relative pronoun of type <<e,t>,<e,e>>; 2) for quantified DPs (a car) which have type <<e,t>,t>: the relative clause must be of type <<<e,t>,t>,<<e,t>,t>> and the relative pronoun of type <<e,t>,<<<e,t>,t>,<<e,t>,t>>:
| the car which Tom destroyed |
| <<e,t>,e> | <e,t> | <<e,t>,<e,e>> | <e,t> |
| e | <e,e> |
| e |
| a car which Tom destroyed |
| <<e,t>,<<e,t>,t>> | <e,t> | <<e,t>,<<<e,t>,t>,<<e,t>,t>>>> | <e,t> |
| <<e,t>,t> | <<<e,t>,t>,<<e,t>,t>> |
| <<e,t>,t> |
