Vladislav
А под капотом все равно один и тот же OutsideIn
A64m
градации не градации, а тут мощный водораздел между ML++ и недопруфнедоассистентом
A64m
А под капотом все равно один и тот же OutsideIn
параметризован только по разному
Vladislav
> а тут мощный водораздел Что делает его мощным? Стиль кода, или технически что-то?
A64m
система типов
Vladislav
Я не вижу четкой границы, каждое расширение по-отдельности как-то модифицирует систему типов.
A64m
грубо говоря, хаскель при этом аж целое семейство языков сменил, Д-М хаскель - это эмельный родственник, а модерновый - совсем нет, нет лет-полиморфизма - не ML
кана
Add * :: *. Why do this? One alternative is to go the route of Coq and Agda and have an infinite tower of type universes. But, this adds a lot of complexity. These languages take this route because * :: * makes a language inconsistent as a logic. However, Haskell is already inconsistent as a logic (because of undefined and GHC.Exts.Any) and so we don't have to worry about a new source of inconsistency. Очень нравится этот абзац.
Leonid 🦇
чёрт, сосисочная вечеринка в сауне срывается
A64m
не буду даже шутить на эту тему, а то у меня с этим митапом какие-то сорокинские асоциации
Leonid 🦇
День функциональщика
Aliester
карируете там небось
Влод
как вообще к этому пришли? на последнем митапе кто-то встал и предложил мол давайте в сауну и все зааплодировали и каждый сказал что обязательно пойдёт?
Kirill
@qnikst а мемори профайлер как-то можно заставить правильное время рисовать?
Alexander
не видел, вроде только cpu
Kirill
я про время снятия сэмплов
Kirill
запускаю приложение на 1 минуту
Kirill
в профайле хипа последняя строчка END_SAMPLE 3.777820
Kirill
писать в eventlog, там нормальное время?
Kirill
блин, eventlog это только в 8.2 :(
Alexander
там cputime не знаю что с этим сделать
Alexander
я понял про что ты
Kirill
даж тикетов об этом нет? а какой именно cputime там?
Kirill
евентлог по идее должен нормальное же время давать, но не понимаю как с графиками сэмплы соотносить тогда
Alexander
CPU_TIME это часы которые меряют сколько твоя программа занимала cpu
Alexander
т.е. если оно жрет проц то будет похожее время, если в idle дофига то твое время будет меньше реального
Alexander
не уверен что есть баг
Kirill
в данном случае почти idle, да
Зигохистоморфный
https://github.com/ermine-language/ermine
Зигохистоморфный
https://github.com/ekmett/ekmett.github.com/blob/master/presentations/Functional%20Reporting.pdf
A64m
по умолчанию OutsideIn как HM работает
Евгений
Странно, а почему не system f второго ранга?
A64m
почему странно?
Зигохистоморфный
Странно, а почему не system f второго ранга?
подключишь батарею из прагм и будет тебе
Евгений
почему странно?
Потому что system f2 это расширение Х-М, не нарушающее его свойств же
Евгений
Почему System F не включают понятно — тайп инференс рушится
кана
а что system f2 дает над hm?
Евгений
Можно ~грабить корованы~фигачить экстенсионалы
кана
ну экстенсионалы тоже по дефолту не включены, нужно -XExistentialQuantification
A64m
подключишь батарею из прагм и будет тебе
нет, у ghc rank2 не включается в принципе, только сразу rankN
Alexander
но было время..
кана
а что тогда делает Rank2-расширение? Алиас на RankN?
A64m
да
Евгений
Я не о расширении синтаксиса, а о (forall r. (forall a. X) -> r)
Alexander
было время это оно не так было
Евгений
да
А OutsideIn гарантирует инференс, если у нас только rank2?
Зигохистоморфный
ну еще ExistentialQuantification есть вроде
A64m
не помню
Евгений
Кстати, почему в ghc такой странный для экзистенционалов синтаксис. Почему forall????
Зигохистоморфный
кана
чтобы кейворды не плодить
Anonymous
да вроде вполне адекватно
Anonymous
в расте &dyn Typeclass
кана
ну вопрос был типа почему не exist
adam
Кстати, почему в ghc такой странный для экзистенционалов синтаксис. Почему forall????
Контравариантные профункторы, конвертирующие вместо пределов, энды в их дуализм являются хорошим примером
Евгений
Что такое "дуализм" эндоморфизма? И как профункторы связаны с forall?
кана
Кстати, почему в ghc такой странный для экзистенционалов синтаксис. Почему forall????
дополнение к "чтобы кейворды не плодить" - ∃x, P(x) → C = (∀x, P(x)) → C
кана
я правда пока не могу понять это равенство совсем
кана
например exist n : M, even(n) -> |M| > 0 = (forall n : M, even(n)) -> |M| > 0 тут же первое утверждение верное, а второе нет.
кана
О, так завтипы в хаскеле это не миф и не почти невозможно будущее, есть реально движение в эту сторону, тот же TypeInType с ghc8
Alexander
много туда движения
кана
и то, что я недавно нашел странную вещь * :: * - не баг, это новая фича - первая фаза внедрения завтипов
Xeta Felius
С хаскелем не соскучишься T_T
Xeta Felius
😆
Зигохистоморфный
Ну большинство вещей для DT в хаскель написала Стефани Вейрих
A64m
и то, что я недавно нашел странную вещь * :: * - не баг, это новая фича - первая фаза внедрения завтипов
есть еще специальная библиотека для накостыливания недозавтипов на синглетонах
кана
есть еще специальная библиотека для накостыливания недозавтипов на синглетонах
ты про singletons? Да, все эти костыли для эмуляции завтипов я видел ранее, а тут прям что-то реальное делается, только без универсумов
Vladislav
подступает 2k18, люди узнают про TypeInType
Vladislav
ну я сразу еще фаст форвард сделаю до момента, как вы узнаете, что он сломан
Vladislav
если попытаетесь использовать
кана
о, а в чем сломан?
Vladislav
https://ghc.haskell.org/trac/ghc/ticket/12919 https://ghc.haskell.org/trac/ghc/ticket/12564
кана
я в принципе только недавно про хаскель узнал-то
Vladislav
в общем я больше года назад нашел два фатальных недостатка, до сих пор не могут разобраться до конца
кана
в первом тикете прям довольно тривиальная вещь и не работает, странно
Vladislav
Во втором тоже базовая.
Vladislav
Я говорю — он сломан, это не минорные баги.