Fix misexplanation of haskell's bottom type

TypeTheory/NeverType.md

@@ -9,7 +9,7 @@
 ### Базовый пример
 
 Например, у нас есть функция `exit`, что завершает исполнения нашей программы, 
-то есть функция никогда не завершиться! Вот реальная сигнатура `std::process::exit` 
+то есть функция никогда не завершится! Вот реальная сигнатура `std::process::exit` 
 из стандартной библиотеке Rust[^neverust]'а:
 ```rust
 pub fn exit(code: i32) -> !
@@ -27,19 +27,25 @@ fn main() -> Result<!, ExitCode> {
 
 ## Альтернативы 
 
-В ML языках (например Haskell) так таковой never-тип не используется, сигнатура 
-той же функции `exit` в стандартной библиотеке Haskell'я выглядит так:
+В Haskell в качестве never-типа используется `Void`, определенный как тип без конструктора:
+```hs
+data Void
+```
+Язык также поддерживает создание пользовательских пустых типов.
+Стоит заметить, что в присутствии побочных эффектов нетерминированный терм не обязательно является пустым.
+Так, например, сигнатура функции `exit` в стандартной библиотеке Haskell'я выглядит так:
 ```haskell
 exitWith :: ExitCode -> IO a
 ```
 * `a` - переменная типа 
-
-Здесь используется return-type полиморфизм, что с точки зрения типов будет иметь
-похожий эффект как и never-тип.
-```haskell
-isOneOrDie :: Int -> IO String
-isOneOrDie 1 = pure "ok"
-isOneOrDie _ = die "💀"
+За счет того, что этот терм в действительности не является пустым.
+
+Однако, результат вычисления этого терма с побочными эффектами является пустым.
+То есть ни одна программа, использующая результат вычисления этого терма никогда не будет выполнена.
+Здесь, вместо `Void` используется аналогичный с точки зрения теории типов пустой тип - `forall a. a`.
+Доказать, что он пуст несложно. Для этого достаточно подставить `Void` вместо переменной типа `a`:
+```hs
+exitWith @Void :: ExitCode -> IO Void
 ```
 
 ## Ссылки