те которые содержат 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 это проще понимать как особое значение

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

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

Нет

Нельзя тип назвать значением

Нужно договориться

Хорошо, как тогда тип может населять другой тип? В haskell

В пределах нас 6ти человек

Bottom населяет Int

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

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

Да меня уже ничего не напрягает:)

Хорошо, пусть будет не-значение

ну bottom это не значеие

это результат for some definition of результат вычисления

Нельзя тип назвать значением

А где-то можно...

А где-то можно...

Если тип включает в себя значение он всё ещё тип. Или я не так понял?

Если тип включает в себя значение он всё ещё тип. Или я не так понял?

В dependent types языках типы и значения не различаются.

Просто насколько я себе представляю, в ванильной теории типов никаких тайпклассов нет. Есть только типы, подтипы и надтипы. Но в хс решили, что удобнее сказать, что ТИП у значения может быть только один (пока забыли про боттом), а для объединения значения разных типов будем юзать тайпклассы

В dependent types языках типы и значения не различаются.

А прям абсолютно. Ну ок

Просто насколько я себе представляю, в ванильной теории типов никаких тайпклассов нет. Есть только типы, подтипы и надтипы. Но в хс решили, что удобнее сказать, что ТИП у значения может быть только один (пока забыли про боттом), а для объединения значения разных типов будем юзать тайпклассы

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

Ну академическая

какая из?

их много: https://en.wikipedia.org/wiki/Type_theory#Systems_of_type_theory

Ну вот откуда эти все top и bottom

надо все-таки смириться, что haskell вдохновлялся теорий категорий

ERROR: S client not available

надо все-таки смириться, что haskell вдохновлялся теорий категорий

Типа ребята закругляемся. Тут теоркат

Типа ребята закругляемся. Тут теоркат

никак нет

Ну вот откуда эти все top и bottom

т.е. в простом типизированном лямбда-исчислении с подтипами с добавлением Top и Bottom?

вроде это самая простая с Top и Bottom ;)

вроде это самая простая с Top и Bottom ;)

Послушаю умного человека:) значит она

А в какой-нибудь теории типов есть тайпклассы?

Кажется здесь была ирония

А в какой-нибудь теории типов есть тайпклассы?

Забей.

А в какой-нибудь теории типов есть тайпклассы?

Это чисто прикладная вещь

Пускай пока что будут типы и порядок между ними

И вот у этих типов будет верх или низ?

И вот у этих типов будет верх или низ?

Зависит от того как определишь порядок

А в какой-нибудь теории типов есть тайпклассы?

ввести соответствующие правила и они появятся. Проблема в том, чтобы потом показать, что они ничего не ломают в теории

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

полагаю, можно посмотреть статьи какого-нибудь Wadler-а про это :)

Ладно

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

можно ввести, это ничего не сломает

Типа ребята закругляемся. Тут теоркат

Ладно этот всё таки похоже больше из области значений чем из области типов

Несмотря на то что англоязычная цитата ли Александра говорила строго об обратном

А мне всё же не даёт покоя, что (head []) и (length $ repeat 1) считаются чем-то одинаковым!!!

Недавно мне показалось, что я это понял, но всё же нет:(

Ладно этот всё таки похоже больше из области значений чем из области типов

есть отношение "a имеет тип A" (± нюансы) и есть отношение "тип A является подтипом типа B", это два разных отношения

есть отношение "a имеет тип A" (± нюансы) и есть отношение "тип A является подтипом типа B", это два разных отношения

Окей хорошо

Я рад

Но давай вставь сюда ботом

Несмотря на то что англоязычная цитата ли Александра говорила строго об обратном

В теории типов bottom это пустой подтип любого типа, но в hs я видел запись в учебнике data Int = undefined | Int#, и пусть меня первым бросит камень тот, кто назовет это чудо-юдо слева от "|" типом

Ну например любой тип является подтипом ботом

Ок?

есть следующее правило типизации: для любого типа T тип Bottom является подтипом T (Bottom :< T)

В теории типов bottom это пустой подтип любого типа, но в hs я видел запись в учебнике data Int = undefined | Int#, и пусть меня первым бросит камень тот, кто назовет это чудо-юдо слева от "|" типом

Вы запутались. undefined это не значение как value, это херня которая много всего в этом языке ломает.

Вот. Херня!