нету значения которое = bottom

Ну хорошо, не значение

bottom (отсуствие значения) населяет все lifted типы

Так как нет конструктора

или т.к. не завершается

bottom (отсуствие значения) населяет все lifted типы

А вот тут погоди

void из моего примера разве не имеет конкретный тип?

data S = S (forall a. a) внутри S тоже bottom 😏

эм.. я сказал отсутсвие значения, тут вопрос "разве не имеет конкретный тип"

а стоп, в цитатах запутался

в любом lifted типе есть _|_

т.е. может быть отсуствие значения

С этим не спорю

Хорошо, то есть если функция невычислима, то мы просто говорим, что она возвращает bottom этого типа?

Любая функция

Вроде понял

Просто мне что интересно

Можно определить два bottom разного типа, но при этом мы всё равно считаем их одинаковыми

bottom не может быть значением

bottom (отсуствие значения) населяет все lifted типы

незначение населяющее типы

ну в цитате выше боттом точно назван типом. тип без конструктора пускай будет боттом. а если есть невычислимое выражение, тип которого известен, то это уже не боттом?

ну то что пустое множество является подмножеством любого множества же никого не напрягает?

Никого

Немного напрягает, что могут быть равны элементы двух разных типов

Если это элемент - боттом

Но я уже начал привыкать

обчный intiial object =)

В теории множеств пустое множество не имеет типа, поэтому оно является подмножеством любого множества.

Получается формально bottom не имеет типа

Получается формально bottom не имеет типа

формально bottom имеет полифорфный тип (forall a. a)

формально bottom имеет полифорфный тип (forall a. a)

Ну так ещё круче

bottom (отсуствие значения) населяет все lifted типы

а что за lifted типы?

те которые содержат bottom 😏

а нет

стоп

те которые содержат bottom 😏

Вроде правильно

А не lifted это Int#

да

я чуть с boxed не попутал

unlifted это #

есть unlifted boxed, нпример ByteArray#

bottom (отсуствие значения) населяет все lifted типы

а разве не liffed типы bottom не населяет?

не населяет

let loop# = loop# in loop# не сделать вроде как

В теории множеств пустое множество не имеет типа, поэтому оно является подмножеством любого множества.

В теории множеств есть типы?

В теории множеств есть типы?

там есть принадлежность

там есть принадлежность

Переформулируй изначальное предложение со словом принадлежность вместо слова тип

обчный intiial object =)

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

Переформулируй изначальное предложение со словом принадлежность вместо слова тип

Все haskell'ные типы задаются как алгебраические множества

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

пустое множество является инициальным объектом в категории множеств, то есто это понятие из теории категорий, которую можно использовать, чтобы понимать типы

Получается формально bottom не имеет типа

Мне нравится думать о типах в Haskell как о метках на значениях. Вот изначально у нас есть просто значения, куча разных значений. А потом мы говорим, давайте теперь любое значение всегда будет содержать одну метку на себе, и только одну. Тогда типизированные (мономорфные) функции соглашаются принимать значения только с определенными метками на них, и возвращают значения других конкретных меток. Так идет вывод типов. Полиморфные функции - это как бы объединение "под одной крышей" бесконечного числа мономорфных функций, каждая из которых опять же принимает и выдает только конкретные метки. Но потом мы берем и добавляем еще одно специальное значение bottom, и говорим, что оно содержит не одну метку, а сразу все, все возможные. Соответственно, любая функция теперь может это значение вернуть. Это всё лично моё понимание, на корректность не претендую.

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

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

У боттома нет значений так что вроде звучит красиво

А наверху стоит топ

Внезапно

А наверху стоит топ

😂

верха не существует же

The top type in the type theory of mathematics, logic, and computer science, commonly abbreviated as top or by the down tack symbol (⊤), is the universal type, 

верха не существует же

Только в хаскелле

Proxy ?

Какой там

а он просто terminal, terminal соотвествует Top или нет?

Int ведь не имеет тип Proxy

Типа любое значение является значением типа top

трудно понимать, когда используют просторечие "типа" в темах про типы =_=

Извиняюсь

Мне кажется, что топ в хаскелл - это forall

Что если бы мы писали функцию id как id :: Forall a => a -> a Где Forall - это универсальный тайпкласс, для которого автоматически делается инстанс для каждого типа, и этот тайпкласс не содержит ни одного метода

Вроде норм

Что если бы мы писали функцию id как id :: Forall a => a -> a Где Forall - это универсальный тайпкласс, для которого автоматически делается инстанс для каждого типа, и этот тайпкласс не содержит ни одного метода

Чем это отличается от боттом

Всем

Ты можешь андефайнед передать в любую функцию и вернуть из любой функции

Боттом - это одно значение всех типов на свете Топ - это один тип всех значений на свете

Двойственность такая

Боттом - это одно значение всех типов на свете Топ - это один тип всех значений на свете

Ни одно значение

Ботом тип

В haskell это проще понимать как особое значение

Потому что нет подтипов и надтипов