В 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 вдохновлялся теорий категорий

надо все-таки смириться, что 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, это херня которая много всего в этом языке ломает.

Вот. Херня!

А не тип

Вот. Херня!

В haskell, а не в теории типов

Да

С теорией типов у меня мир 😀

/o

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

О, вот что придумал. В теории типов не делают различия между вычислением, которое моментально возвращает "ошибку" (head []) и вычислением, которое выполняется бесконечно долго (length $ repeat 1), потому что в теории типов нет времени 🤗 Просто либо что-то возвращает, либо нет. Всё, кажется утряслось.

эм.. а разве эт неочевидно?

эм.. а разве эт неочевидно?

Теперь да:)

Как только дошло

+SafeCopy

в продолжение и дабы разбавить ужасы bottoma: а это сделано поверх distributed-process c какой-то кастомной сериализацией или вы определяете data Message = Message ByteString?

сорри я не думал, что это дополнять надо

или на более низком уровне?

на уровне distributed process

то есть там можно плагинить свою сериализацию?

ну у нас есть data Message = Message StablePrint ByteString

а оверхед на копирование?

ну типа один массив байтов в другой

или это ерунда

там writev подиее не должно быь большой проблемой при больших размерах

опа

то есть сериализатор использует writev?

в смысле сериализует сразу в сокет?

или я туплю

а, ясно

оно в lazybytestring сериализует который куски байтострок