Система типа Haskell изоморфна непоследовательной логической системе? Если да, каковы последствия?

Ответ 1

Да, логика непоследовательна.

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

У нас все еще есть некоторые ошибки времени выполнения, такие как не исчерпывающее сопоставление шаблонов (которое я лично запретил на языке: -P), error, undefined, исключениях и т.д. Но, по крайней мере, у нас нет родственных типов. У нас также есть бесконечность (через бесконечную рекурсию), которая является необходимым злом на полном языке Тьюринга, и в любом случае это приведет к несогласованности.

Наконец, я бы сказал, что Карри-Говард полезен даже в такой непоследовательной обстановке. Например. если бы я хотел написать f :: Either a b -> a, я сразу могу заметить, что это не интуиционистская теорема, поэтому f может быть реализована только с использованием вышеперечисленных ошибок времени выполнения, поэтому, вероятно, это плохая идея, и если мне нужно a f, я должен пересмотреть свой дизайн.

Было бы также полезно иметь четко определенный "общий" фрагмент Haskell с теми же типами, но без плохих вещей, упомянутых выше? Абсолютно! Например, это позволило бы оптимизировать любое выражение типа () до значения () - после того, как все это нужно оценить. Кроме того, e :: a :~: b аналогичным образом оптимизировалось бы на что-то вроде unsafeCoerce Refl, позволяя писать "доказательства равенства между типами", для которых требовалась бы только стоимость O (1). В настоящее время, к сожалению, такие доказательства необходимо оценивать во время выполнения, что приводит к глупым накладным расходам только для обеспечения того, что доказательство является "реальным", а не, например, замаскированный undefined.

Ответ 2

Если система типа Haskell является непоследовательной системой доказательств, то мы не можем доверять ей?

Как указано в @chi, тип безопасности намного слабее, чем логическая согласованность. Цитирование Типы и языки программирования (хорошо читайте, если вас интересует такая вещь!),

Безопасность = прогресс + сохранение

[...] То, что мы хотим знать, заключается в том, что хорошо типизированные термины не застревают. Мы показываем это в два этапа, обычно называемые теоремами прогресса и сохранения.

• Прогресс: хорошо типизированный термин не застревает (либо это значение, либо он может сделать шаг в соответствии с правилами оценки).
• Сохранение: если хорошо типизированный термин принимает этап оценки, то итоговый термин также хорошо типизирован.

Эти свойства вместе говорят нам, что хорошо типизированный термин никогда не сможет достичь застрявшего состояния во время оценки.

Обратите внимание, что это определение безопасности типов не исключает возможности того, что хорошо типизированный термин будет зацикливаться навсегда или выбросить исключение. Но эти два правила гарантируют, что если вы успешно получили Int, то это действительно Int, а не Bool или Spoon или Ennui. (В Haskell это несколько усложняется ленивностью, но основная идея остается верной.) Это очень полезное свойство, и программисты учатся критиковать его в повседневной работе!

Позвольте мне отвлечься. Подобно тому, как логически-непоследовательные, но все еще сохраняющие тип системы полезны и заслуживают доверия на практике, системы на основе небезопасного, но все еще статически проверенные также полезны на практике (хотя некоторые могут отказаться от вызова их "заслуживающих доверия" ), Посмотрите на экосистему JavaScript, где "постепенно набираемые" системы, такие как TypeScript и Flow предназначены для обеспечения дополнительного уровня поддержки для работающих программистов - потому что VanillaJS - это кошмар в даже средних кодовых версиях - без смелости promises, как прогресс и сохранение. (Я слышал, что сообщества Python и PHP также постепенно (ха-ха) принимают типы.) TypeScript все еще успешно улавливает значительную долю человеческих ошибок, которые я делаю во время программирования, и поддерживает изменение кода в малом и большом, будучи "безопасным по типу" в формальном смысле.

На мой взгляд, сообщество PL имеет тенденцию уделять большое внимание проверке свойств систем (таких как безопасность типов), но часто не так, как инженеры-программисты выполняют свою работу! Инженеры, которых я знаю, заботятся о том, помогает ли инструмент им писать меньше ошибок, а не о том, было ли это доказано безопасным или последовательным. Я просто думаю, что каждая группа может многому научиться у другого! Когда умные люди в ультра-типичном сообществе соберутся вместе с умными людьми в нетипизированном сообществе для создания инструментов для инженерии, могут случиться интересные вещи.

Можно было бы представить бесконечный цикл без undefined?

Конечно. Много способов.

loop = loop
fib = 1 : 1 : zipWith (+) fib (tail fib)
repeat x = unfoldr (const (Just x))
main = forever $ print "cheese"

С формальной точки зрения все эти термины ⊥, но на практике это очень важно, какой ⊥ вы используете.

Если бы ваш вопрос действительно заключался в возможности писать циклические термины, подразумевая несогласованность? то короткий ответ - да, а именно let x = x in x :: forall a. a. Вот почему помощники помощников, такие как Agda, обычно имеют проверку завершения сеанса, которая анализирует синтаксис вашей программы и отвергает подозрительные обычаи общей рекурсии. Более длинный ответ нет, а не точно - вы можете встроить общие рекурсивные части вашей программы в монаду, а затем реализовать семантику этой пристрастности монада с каким-то внешним оценщиком. (Это именно тот подход, который Haskell делает для чистоты: поместите нечистые части в монаду IO и делегирование исполнения в систему времени исполнения.)

В заключение, да, Haskell непоследовательна как логика - каждый тип населен бесконечным семейством ⊥ с различными режимами исполнения, поэтому вы можете легко "доказать" любое предложение. Это (наряду с общей неуклюжностью зависимых типов) заключается в том, почему люди не используют Haskell в качестве доказательства теоремы. Для инженерии, однако, меньших гарантий безопасности типа, как правило, достаточно, и некоторые из них ⊥ интересны!