История изменений

Bottom является частью системы типов в Haskell.

Вот это утрвеждение и есть «чит». Вернее не оно, а то что у боттом в хаскеле могут быть значения. Bottom пустой тип. У него нет значений, в том и смысл его. Но если тебе язык позволяет создавать экземпляр любого типа, то ты можешь просто создать что угодно. А система типов как раз не должна позволять создавать что угодно. В этом её смысл изначально.

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

Это последствие существования ленивых вычислений из-за того, что вычисление любого значения потенциально может окончиться бесконечным циклом.

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

Что такое «честная функция»?

это реализация без использования значения типа Bottom.

Bottom является частью системы типов в Haskell.

Вот это утрвеждение и есть «чит». Bottom пустой тип. У него нет значений, в том и смысл его. Но если тебе язык позволяет создавать экземпляр любого типа, то ты можешь просто создать что угодно. А система типов как раз не должна позволять создавать что угодно. В этом её смысл изначально.

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

Это последствие существования ленивых вычислений из-за того, что вычисление любого значения потенциально может окончиться бесконечным циклом.

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

Что такое «честная функция»?

это реализация без использования значения типа Bottom.

Bottom является частью системы типов в Haskell.

Вот это утрвеждение и есть «чит». Bottom пустой тип. У него нет значений, в том и смысл его. Но если тебе язык позволяет создавать экземпляр любого типа, то ты можешь просто создать что угодно. А система типов как раз не должна позволять создавать что угодно. В этом её смысл изначально.

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

Это последствие существования ленивых вычислений из-за того, что вычисление любого значения потенциально может окончиться бесконечным циклом.

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

Что такое «честная функция»?

это реализация без использования Bottom.