на самом деле хочется с семантикой data U a where U : a ->. U a

но без боксинга

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

тьфу т.е. наоборот анлифтнутые, но забоксенные

угу

вообще я хочу даже не знаю чего, хинта для тайпчеккера

наверное

т.е. я хочу data Unrestricted без оверхеда

т.е. я хочу unboxed lifted type

чтобы я могу написать (# ReadWorld#, Unrestricted# a #)

т.е. поидее a тут должен быть левити-полиморфным

вечер в хату

https://www.flip.kz/catalog?prod=489763

кто нибудь знает за эту книгу?

https://medium.com/@_bravit/alejandro-serrano-mena-beginning-haskell-a-project-based-approach-2014-276d73b03353

https://www.flip.kz/catalog?prod=489763

у меня эта книга

блин не могу определиться че взять почитать на недели две

кто-нибудь читал Программист-прагматик. Путь от подмастерья к мастеру

?

TAPL бери. (На самом деле нет.)

кто-нибудь читал Программист-прагматик. Путь от подмастерья к мастеру

Да, очень хорошая книга, но при чём тут она

кто-нибудь читал Программист-прагматик. Путь от подмастерья к мастеру

полезная книга

кто-нибудь читал Программист-прагматик. Путь от подмастерья к мастеру

Читал, очень понравилось. Планирую вскоре перечитать.

Сразу же и годноты почерпнул, и мотивации.

В бумаге в СПб не нашёл, кстати.

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

не модный нынче, нетаргетированный

TAPL бери. (На самом деле нет.)

почему не брать?) я просто читаю ее, вот опять вернулся к чтению этой книги в том числе, пока есть время. вроде нормальная книга же, более-менее понятно обясняется все

не хватит на 2 недели

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

TAPL прекрасная книга, конечно. К сожалению, в ней нет некоторых важных вещей, которые тогда считались более продвинутыми, а сейчас маст хэв. Зависимые типы, в основном.

почему не брать?) я просто читаю ее, вот опять вернулся к чтению этой книги в том числе, пока есть время. вроде нормальная книга же, более-менее понятно обясняется все

Потому что я не уверен что спрашивавшему она подойдет.

@qnikst а вы в Tweag билдите через bazel много?

тест там что-то, пока средне успешно

TAPL прекрасная книга, конечно. К сожалению, в ней нет некоторых важных вещей, которые тогда считались более продвинутыми, а сейчас маст хэв. Зависимые типы, в основном.

Ну на то она и энтри-левел

там как-то вопросов больше, чем ответов

у меня в проекте стек и никс

@qnikst а вы в Tweag билдите через bazel много?

^

Ну на то она и энтри-левел

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

там есть проект где много разных языков и хитрые требования, сейчас там shake

а что посоветуете почитать про зависимые типы более-менее фундаментальное, чтобы проникнуться по-лучше идеями? я сейчас читаю type-driven development with Idris, но она сугубо про идрис и больше "практическая"

Там разве нет ничего про лямбда-куб?

в тапле есть вроде как

т.е. не сильно в курсе куда https://github.com/tweag/rules_haskell ?

это тесты как раз этого дела

я могу уточнить

Точно не Идрис, это книга по программированию (хоть и хорошая сама по себе), потому с ТАПЛ её невозможно сравнивать. Если что-то типа ТАПЛ (хотя такого и нет, к сожалению), то @bravit111 недавно обратил моё внимание на Loh, A., McBride, C., & Swierstra, W. (2010). A tutorial implementation of a dependently typed lambda calculus. Оно выглядит очень прилично. Это именно энтри-левел и с ориентацией на реализацию типа как у Пирса.

Там разве нет ничего про лямбда-куб?

Нет, конечно

Но вообще это оффтопик тут)

Активная аудитория у каналов примерно одинаковая, с первого взгляда не определить в каком ты канале, особенно когда отвечаешь на реплай. Форум хотца. Изивните за оффтоп.

Точно не Идрис, это книга по программированию (хоть и хорошая сама по себе), потому с ТАПЛ её невозможно сравнивать. Если что-то типа ТАПЛ (хотя такого и нет, к сожалению), то @bravit111 недавно обратил моё внимание на Loh, A., McBride, C., & Swierstra, W. (2010). A tutorial implementation of a dependently typed lambda calculus. Оно выглядит очень прилично. Это именно энтри-левел и с ориентацией на реализацию типа как у Пирса.

спасибо, полистал, как раз то, что нужно (We present both the mathematical specification and Haskell implementationof the abstract syntax, evaluation, and type checking. Taking the simply-typed lambda calculus as startingpoint, we move on to a minimal dependently typed lambda calculus), буду (пробовать) читать

TAPL прекрасная книга, конечно. К сожалению, в ней нет некоторых важных вещей, которые тогда считались более продвинутыми, а сейчас маст хэв. Зависимые типы, в основном.

ATTAPL же есть

ATTAPL же есть

Вы его читали? Это совсем другая книга. Это фактически сборник статей от разных авторов с разной степенью качества написанных, той методической проработки, которая была в ТАПЛ, там и близко нет. Кому-то нравится статья про зависимые типы там, но лично я так не считаю.

Вы не обижайтесь, просто когда упоминают в одном контексте ТАПЛ и АТТАПЛ я всегда поражаюсь

ну да, не берусь оценивать что там по завтипам написано, но по модулям, например, там Боб Харпер, например главу писал, что вполне прилично

Харпер хороший дядька (хоть и сильно не любит Хаскель), но если уж его вспоминать, то надо сказать и про его книгу по теории яп, по глубине сильнее Пирса

Верней, наверное, по ширине)

Кстати, если никогда не слышали Харпера вживую, обязательно пойдите на Ютуб и послушайте что-нибудь: гарантирую разрыв всевозможных шаблонов! У меня был…

Кстати, если никогда не слышали Харпера вживую, обязательно пойдите на Ютуб и послушайте что-нибудь: гарантирую разрыв всевозможных шаблонов! У меня был…

не понимаю, о чем речь

не понимаю, о чем речь

Интересный дядя

это вроде и из того что он пишет понятно

Ну не знаю, Пирса, например, скучновато слушать, а пишет прекрасно. И, скажем, Пфеннинга.

Это вообще не связанные вещи, думаю

Интересный дядя

Когда так говорят о ком-то, я обычно думаю, что этого кого-то считают психом

Не без того :) но слушать надо обязательно и оторваться невозможно

Хаскель умеет депендент фрии компиляцию?

Не без того :) но слушать надо обязательно и оторваться невозможно

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

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

под рукой — не особо, на Ютубе просто Robert Harper вот это прикольное видео с нарезкой для первого впечатления https://www.youtube.com/watch?v=RcTaweZMEzo ну а посерьёзней этот плейлист, наверное: https://www.youtube.com/watch?v=9SnefrwBIDc&list=PLGCr8P_YncjXRzdGq2SjKv5F2J8HUFeqN или любой цикл лекций из OPLSS. Последнего года тут: https://www.cs.uoregon.edu/research/summerschool/summer17/topics.php особенно четвёртая лекция угарная: он там за одну лекцию решил рассказать ВСЁ про теорию типов, что не успел в первые три. Mind blowing!

ну я просто смотрел что-то из его лекций, но не выделил особо необычности. Обращу внимание, спасибо )

ну я не даю оплачиваемой гарантии, что каждого тут зацепит :) Меня вот зацепило, да… Хотя повторю, приходится закрывать уши, когда он упоминает язык на букву Х

это да) он не стесняется при случае напомнить о несовершенствах хаскеля

это плохо что ли? Зачем уши закрывать?

Хаскель умеет депендент фрии компиляцию?

что умеет?

что умеет?

Чтобы как в го сразу статический бинарник получался

статический со всеми libffi, libgmp?

и glibc

Хаскель умеет депендент фрии компиляцию?

если вопрос действительно про статическую линковку, то умеет

огребая в случае glibc все проблемы статической линковки с glibc

проще все эти soшки рядом сложить +rpath