Теория гомоиконических типов

Lisp имеет свойство быть гомоиконным , то есть представление кода, используемого реализацией языка (списки), также доступно и идиоматически используется программами, которые хотят представлять код для своего собственного целей.

Другое крупное семейство языков функционального программирования, ML, основано на теории типов, что означает, что реализация языка требует более сложного представления кода, а также менее случайна в отношении того, что вам разрешено делать, поэтому обычно внутреннее представление недоступно для программ. Например, средства проверки доказательств для логики более высокого порядка часто реализуются в языках семейства ML, но обычно реализуют свою собственную систему теории типов, эффективно игнорируя тот факт, что компилятор ML уже имеет такую ​​систему.

Есть ли исключения из этого? Любые языки программирования, основанные на теории типов, которые предоставляют представление своего кода для программного использования?