Система типов в Scala завершена по Тьюрингу. Доказательство? Пример? Преимущества?

Есть утверждения, что система типов Scala является полной по Тьюрингу. У меня следующие вопросы:

1. Есть ли формальное доказательство этого?

2. Как бы простое вычисление выглядело в системе типов Scala?

3. Приносит ли это какую-либо пользу Scala - языку? Делает ли это Scala более «мощным» в некотором роде по сравнению с языками без полной системы типов Тьюринга?

Я полагаю, это относится к языкам и системам типов в целом.