Почему?

вот например ещё один вариант, назовём его "синтаксическая эквивалентность" undefined и void по буквам не совпадает, так что они не эквивалентны

А let loop = loop in loop?

void очевидно населяет тип Void. Но если она совпадает с undefined, который населяет любой тип, то ок

кстати ещё интересно: ты про теорию или про компайл-тайм, рантайм?

Хорошо, допустим. Для закрепления: Если мы определим data Void = Void Void void = Void void То void НЕ будет bottom, верно? Потому что находится в СЗНФ? А для newtype Void = Void Void void невозможно привести к СЗНФ, поэтому это bottom

Так?

Сорри, с телефона пишу, опечатки

Декомпозиция в Haskell определяет бесконечные циклы

Ты можешь с ними работать не можешь вычислить

Скажите мне в чем проблема? Я не понимаю

Хорошо, допустим. Для закрепления: Если мы определим data Void = Void Void void = Void void То void НЕ будет bottom, верно? Потому что находится в СЗНФ? А для newtype Void = Void Void void невозможно привести к СЗНФ, поэтому это bottom

в 1м случае боттом

Выражение void = Void void верное

Выражение void = Void void верное

Погоди, пожалуйста

Ща я разберусь, а потом тебе объясню

Это как определение бесконечности для целых чисел

Скажите мне в чем проблема? Я не понимаю

человек не уточняет вопрос, но думает что уже сейчас есть точный ответ

в 1м случае боттом

Почему в первом то bottom??

data же ленивый

data Void = Void Void не bottom

data Void = Void Void не bottom

Вот, это хорошо

потому что невычислимое выражение? разве что можно прикопаться к тому что боттом = невычислимое для каждого типа, а здесь для данного конкретного

потому что невычислимое выражение? разве что можно прикопаться к тому что боттом = невычислимое для каждого типа, а здесь для данного конкретного

Дай умному человеку сказать

Видел же стримы?

Там то же самое

И это никакой не боттом

нет не видел

От них можно брать take и т.д.

но и не видел определения боттома зависещего от ленивости

Если выражение не вычисляемое это не значит что его нельзя вычислять. Невычисляемый (bottom) это значит что неизвестно будет ли формула упрощена (вычеслена)

Ну как список, только без конструктора пустого списка

ну ок идею понимаю

Мы же определяем поток как data Stream a = a :& Stream a

А вычислять и упрощать да сколько влезет

легко определить бесконечный список

и ты про то же самое

Вот тебе специальная data

Мы же определяем поток как data Stream a = a :& Stream a

Но ты же этот поток не вычисляешь полностью

Но ты же этот поток не вычисляешь полностью

Да, но с ним можно делать много чего другого

Поток можно пустить на декомпозицию

Вычислить нельзя

Например напечатать первые 10 элементов или мапнуть

Печать первых 10 идёт через декомпозицию

Не через полное вычисление

тогда допустим 1) a = 1:a 2) length a 1е не боттом. 2е боттом?

По мне так да

по мне так одно и то же

А как проверить что что-то Боттом ?

В компиляторе такое есть?

нет

про компилятор забудь

тогда допустим 1) a = 1:a 2) length a 1е не боттом. 2е боттом?

У тебя в первом clause, а во втором значение

мы тут наверное про теорию

Как ты их вообще сравниваешь

Я не понял

bottom это ЗНАЧЕНИЕ

а харошо

блин да это я смачно тут народ обманул

Ты имеешь в виду, является ли a bottom?

a и length a

a не bottom

length a думаю, что да

Но блин это на самом деле разговор трех нубов

всё таки боттом?

Да

ну да, стоит как бы забыть про то что мы все некомпетентны

это только мешает

если бы здесь заявился бы авторитет то каждый бы просто сказал – ага ок я понял

и всё, а так рассуждение

я вот попробую резюмировать

1. Для любого выражения в Haskell можно сказать, что либо его верхний конструктор вычисляется за конечное время (приведение к СЗНФ, слабой заголовочной нормальной форме), либо нет. Нам не важно, что эта задача в общем случае алгоритмически неразрешима (всем известная "проблема останова"). Главное, что это так. 2. Если верен второй случай (верхний конструктор невычислим), то мы называем такое значение bottom 3. Тем не менее, даже для значений bottom можно вывести их тип. Например length (бесконечный список) — bottom типа Int 4. Мы говорим, что все bottom одного и того же типа эквивалентны и суть одно и то же значение этого типа. 5. Дополнительно мы определяем полимофный undefined, который являет собой bottom любого типа. bottom любого конкретно типа и undefined - одно и то же.

@qnikst это не бред?

Попозже прочитаю отвечу

>Мы говорим, что все bottom одного и того же типа эквивалентны плюс бесконечность и минус бесконечность

Я тут сына домой веду неудобно читать

Попозже прочитаю отвечу

хорошо, спасибо

ну или рекурсия по разным конструкторам, хотя в итоге конечно не важно какое будет значение

ну или рекурсия по разным конструкторам, хотя в итоге конечно не важно какое будет значение

Если конструкторы ленивые, то это конечно разные значения, и оба не bottom

А если энергичные, то одинаковые, bottom

я так думаю

А насчёт плюс бесконечности и минус бесконечности — ты какой тип имеешь в виду?