Прекрасное:
"Telescopes Are Tries: A Dependent Type Shellac on SQLite"

Представляем телескопы (преобразователи зависимых типов в обычные) как префиксные деревья с вложенными отображениями (например, словари Python), а так как телескопы эквивалентны конъюнктивным запросам, получаем
категорию, где композиция соответствует контекстным преобразованиям.

То есть можно легко и просто эмулировать зависимые типы (да и просто сложные типы F#/Haskell) словарями Python, где ключи — значения переменных, а значения -- вложенные контексты; и никаких GADT/singletons.

Более того из "телескопных" описаний несложно генерировать SQL, а в результате получаем прозрачную работу не только с реляционными данными, но и с графами, транзитивными замыканиями и т.п.