Зачем нужен Void?
Если этот тот тип который делает ничего, то для полноты мат.теории
Нурлан
Нурлан
вот замечательный сайт, где все эти превратности функционального подхода описаны
Нурлан
https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/
Anonymous
Зачем Void содержит bottom?
Anonymous
https://wiki.haskell.org/Bottom
Anonymous
Вот это.
Anonymous
Bottom is a member of any type, но зачем он войду-то?
Anonymous
Извиняюсь за глупые вопросы заранее.
Влод
Ну (моё понимание) боттом - вэлью (тэрм) любого типа, воид - тип без конструкторов или с невычеслимым конструктором что потенциально делает его типом которому не принадлежит ни один value
Влод
Вэлью по русски наверное будет значение. Но значение слишком многозначное слово
Влод
Ну житель забавно как-то звучит. Но хорошо давайте будем называть житель
Влод
Воид ненаселённый тип
Влод
А боттом как?
Влод
Житель любого типа. Или для типа тоже есть забавное словечко
Влод
Bottom is a member of any type, но зачем он войду-то?
кстати до этого были вводные слова про понимание вещей, вопрос я так и не понял
Нурлан
In the ideal world we would just say that Haskell types are sets and Haskell functions are mathematical functions between sets. There is just one little problem: A mathematical function does not execute any code — it just knows the answer. A Haskell function has to calculate the answer. It’s not a problem if the answer can be obtained in a finite number of steps — however big that number might be. But there are some calculations that involve recursion, and those might never terminate. We can’t just ban non-terminating functions from Haskell because distinguishing between terminating and non-terminating functions is undecidable — the famous halting problem. That’s why computer scientists came up with a brilliant idea, or a major hack, depending on your point of view, to extend every type by one more special value called the bottom and denoted by _|_, or Unicode ⊥. This “value” corresponds to a non-terminating computation. So a function declared as:
f :: Bool -> Bool
may return True, False, or _|_; the latter meaning that it would never terminate.
Interestingly, once you accept the bottom as part of the type system, it is convenient to treat every runtime error as a bottom, and even allow functions to return the bottom explicitly. The latter is usually done using the expression undefined, as in:
f :: Bool -> Bool
f x = undefined
This definition type checks because undefined evaluates to bottom, which is a member of any type, including Bool. You can even write:
f :: Bool -> Bool
f = undefined
(without the x) because the bottom is also a member of the type Bool->Bool.
Functions that may return bottom are called partial, as opposed to total functions, which return valid results for every possible argument.
Нурлан
Нзчт :)
Влод
вроде бы в тапл пояснялось, что тип != множество
Ilya
По-прежнему вопрос про Void. Итак, везде пишут, что это тип, у которого нет ни одного населяющего его значения.
Я нашёл такое определение Void:
newtype Void = Void Void
Хорошо. Допустим. Теперь объясните мне, почему этот тип не населяет ни одного значения
Ilya
вот же
Ilya
newtype Void = Void Void
void = Void void
Влод
"Functions that may return bottom are called partial" в такой терминологии немного неприятно, что нет разницы между потенциально незавершимыми функциями и функциями возвращающими error
Ilya
λ> :t void
void :: Void
Ilya
константа void разве не населяет тип Void?
Ilya
Или в чём я ошибаюсь?
Влод
https://hackage.haskell.org/package/base-4.9.1.0/docs/src/Data.Void.html#Void
Влод
https://hackage.haskell.org/package/void-0.7.1/docs/src/Data-Void.html#Void
ну ок здесь твой воид. теперь мне тоже интересно
Ilya
такое определение Void через newtype взято отсюда https://habrahabr.ru/post/207126/
Ilya
Ilya
вопрос значит пока в силе
melvin
а у хаскеля есть библия?
Влод
По идее вычисление конструктора незавершимо, но такое значение ты всё же можешь передавать в функции принимающие воид
Влод
было бы проще всё же определять его как тип без конструкторов
Влод
есть 2 причины почему так нужно: во всяких типах данных сделать чтобы не вернуть ничего было, например в кондуитах у producer тип входа Voi
Влод
вот это утверждение немного ломается
Ilya
А причем тут си?
Ilya
Я же определил void свой сам
Ilya
И он имеет тип Void
Нурлан
Что бы определить объект из твоего void нужно определить объект из Void а у него нет объектов.
Нурлан
Объект плохое слово
melvin
или эта?
http://book.realworldhaskell.org
melvin
или это?
http://haskellbook.com
Нурлан
а у хаскеля есть библия?
На этот вопрос нельзя отвечать. В РФ за это сажают, а то вдруг кого-нибудь оскорблю.
melvin
я всм книга книг, святое писание создателей языка, и тд
melvin
вроде как k&r для c
Нурлан
Знать бы ещё что это
melvin
Знать бы ещё что это
отака хирня
https://upload.wikimedia.org/wikipedia/commons/9/95/The_C_Programming_Language,_First_Edition_Cover_(2).svg
Ilya
Влод
@melancholiak ты же наверное тралиравать сюда пришёл. http://learnyouahaskell.com библия. в ней полный материал. ответы на все вопросы
Нурлан
newtype P = P Int, как у этого типа выглядят элементы типа?
Влод
завершай шутку
melvin
@melancholiak ты же наверное тралиравать сюда пришёл. http://learnyouahaskell.com библия. в ней полный материал. ответы на все вопросы
нет, не троллировать.
просто на офф ресурсе яп кипа книг, а прочитать хочу только одну, покачественнее
Нурлан
Влод
и зачем тогда это называть библией
Нурлан
Как P 1, P 2... Для компилятора
Когда строится элемент P Int берётся конкретный элемент из Int, а в Void таких нет
Ilya
Рекурсивный тип
Ilya
Мы же определяем поток как data Stream a = a :& Stream a
Нурлан
Почему бы тебе не использовать имена типов которые уже заняты?
Влод
ты как-то не с того начал. ты не спросил помощи, та начал докапываться мол что лучшая книга (и вообще БИБЛИЯ... это тупо звучит). ну haskellbook сейчас ок книга, но на англ, а без англ жизни особо то и нет
Нурлан
Я не помню точно чем отличается data от newtype может быть невозможностью рекурсии. Если я тебя правильно понял тут надо смотреть как компилятор читает newtype
Ilya
Ладно, давайте я поставлю вопрос ребром
Ilya
Я не помню точно чем отличается data от newtype может быть невозможностью рекурсии. Если я тебя правильно понял тут надо смотреть как компилятор читает newtype
У data ленивый конструктор, а у newtype энергичный
Ilya
Конечно, наверное в этом и зарыта собака
Ilya
Но тогда ЧТО понимается под этим??
Нурлан
Если в newtype нельзя рекурсивный тип то второй Void читается как стандартный
Ilya
λ> :t void
void :: Void