Encrypted Search and Oblivious Types

Oblivious types give encrypted search information-theoretic privacy against access pattern leakage. No ORAM, no computational hardness assumptions. Here's how.