>> a free theorem is when you can say something that is always true about a function machine if you only know its type, but you don’t know anything about what it does on the inside.” This seemed a bit beyond him... To be fair, this is a bit beyond most who had no contact with functional programming and category theory.
Also, there is a strong intuition to free theorems that many people without an FP background will easily understand.