>> 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.