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

Зачем нужен Void?

newtype Void = Void Void

чтобы была ложь в типах

абсурд там

Зачем лгать в типах??

чтобы был ненаселёный тип

есть 2 причины почему так нужно: во всяких типах данных сделать чтобы не вернуть ничего было, например в кондуитах у producer тип входа Voi

Void

что говорит, что входа нет

плюс так отрицание строится

ну например чтобы not был

через a -> Void

ну я ж говорю 2 причины

ну я до сих пор не уверен есть ли норм пруверы на хаскельных типах

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

аесли пруверов нет, то не уверен имеет ли смысл лгать в типах.

есть две причины

вторая остаётся валидной

https://hackage.haskell.org/package/singletons-2.2/docs/Data-Singletons-Decide.html#t:Refuted

в синглетонах в Decision используется как ложь

Зачем нужен Void?

Если этот тот тип который делает ничего, то для полноты мат.теории

вот замечательный сайт, где все эти превратности функционального подхода описаны

https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/

Зачем Void содержит bottom?

Зачем Void содержит bottom?

Что это значит

https://wiki.haskell.org/Bottom

Вот это.

Bottom is a member of any type, но зачем он войду-то?

Извиняюсь за глупые вопросы заранее.

Ну (моё понимание) боттом - вэлью (тэрм) любого типа, воид - тип без конструкторов или с невычеслимым конструктором что потенциально делает его типом которому не принадлежит ни один 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.

Нзчт :)

вроде бы в тапл пояснялось, что тип != множество

По-прежнему вопрос про Void. Итак, везде пишут, что это тип, у которого нет ни одного населяющего его значения. Я нашёл такое определение Void: newtype Void = Void Void Хорошо. Допустим. Теперь объясните мне, почему этот тип не населяет ни одного значения

вот же

newtype Void = Void Void void = Void void

"Functions that may return bottom are called partial" в такой терминологии немного неприятно, что нет разницы между потенциально незавершимыми функциями и функциями возвращающими error

λ> :t void void :: Void

константа void разве не населяет тип Void?

Или в чём я ошибаюсь?

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 ну ок здесь твой воид. теперь мне тоже интересно

такое определение Void через newtype взято отсюда https://habrahabr.ru/post/207126/

https://hackage.haskell.org/package/void-0.7.1/docs/src/Data-Void.html#Void ну ок здесь твой воид. теперь мне тоже интересно

да, здесь так же

вопрос значит пока в силе

а у хаскеля есть библия?

По идее вычисление конструктора незавершимо, но такое значение ты всё же можешь передавать в функции принимающие воид

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

есть 2 причины почему так нужно: во всяких типах данных сделать чтобы не вернуть ничего было, например в кондуитах у producer тип входа Voi

вот это утверждение немного ломается

константа void разве не населяет тип Void?

В Haskell нет константы void в сишном понимании

А причем тут си?

а у хаскеля есть библия?

это? http://learnyouahaskell.com

Я же определил void свой сам

И он имеет тип Void

Что бы определить объект из твоего void нужно определить объект из Void а у него нет объектов.

Объект плохое слово

или эта? http://book.realworldhaskell.org

ERROR: S client not available

или это? http://haskellbook.com

а у хаскеля есть библия?

На этот вопрос нельзя отвечать. В РФ за это сажают, а то вдруг кого-нибудь оскорблю.

или это? http://haskellbook.com

Ее называют самой лучшей

На этот вопрос нельзя отвечать. В РФ за это сажают, а то вдруг кого-нибудь оскорблю.

кек

я всм книга книг, святое писание создателей языка, и тд

вроде как k&r для c

Знать бы ещё что это

Знать бы ещё что это

отака хирня https://upload.wikimedia.org/wikipedia/commons/9/95/The_C_Programming_Language,_First_Edition_Cover_(2).svg

Что бы определить объект из твоего void нужно определить объект из Void а у него нет объектов.

Пока непонятно

Ее называют самой лучшей

в ней полный материал?

@melancholiak ты же наверное тралиравать сюда пришёл. http://learnyouahaskell.com библия. в ней полный материал. ответы на все вопросы

newtype P = P Int, как у этого типа выглядят элементы типа?

завершай шутку

@melancholiak ты же наверное тралиравать сюда пришёл. http://learnyouahaskell.com библия. в ней полный материал. ответы на все вопросы

нет, не троллировать. просто на офф ресурсе яп кипа книг, а прочитать хочу только одну, покачественнее

нет, не троллировать. просто на офф ресурсе яп кипа книг, а прочитать хочу только одну, покачественнее

Ну... сложно тебе будет.

и зачем тогда это называть библией

Ну... сложно тебе будет.

чего?

newtype P = P Int, как у этого типа выглядят элементы типа?

Как P 1, P 2... Для компилятора

и зачем тогда это называть библией

что называть библией?

что называть библией?

Плз не засоряй тему

Как P 1, P 2... Для компилятора

Когда строится элемент P Int берётся конкретный элемент из Int, а в Void таких нет

Плз не засоряй тему

если ньюби пришел спрашивать что почитать - это засорение темы?

Когда строится элемент P Int берётся конкретный элемент из Int, а в Void таких нет

И что

Рекурсивный тип

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

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

ты как-то не с того начал. ты не спросил помощи, та начал докапываться мол что лучшая книга (и вообще БИБЛИЯ... это тупо звучит). ну haskellbook сейчас ок книга, но на англ, а без англ жизни особо то и нет

Я не помню точно чем отличается data от newtype может быть невозможностью рекурсии. Если я тебя правильно понял тут надо смотреть как компилятор читает newtype

Ладно, давайте я поставлю вопрос ребром

Я не помню точно чем отличается data от newtype может быть невозможностью рекурсии. Если я тебя правильно понял тут надо смотреть как компилятор читает newtype

У data ленивый конструктор, а у newtype энергичный

Конечно, наверное в этом и зарыта собака

Но тогда ЧТО понимается под этим??