экзотика, пока не сломается

В смысле?

старый который переэмель с лет-полиморфизмом и тот, когда включаются какие-то поверхностные проявления FC и, соотв. вывод типов не Дамас-Милнер становится

Ну тут явно больше градаций

А под капотом все равно один и тот же OutsideIn

градации не градации, а тут мощный водораздел между ML++ и недопруфнедоассистентом

А под капотом все равно один и тот же OutsideIn

параметризован только по разному

> а тут мощный водораздел Что делает его мощным? Стиль кода, или технически что-то?

система типов

Я не вижу четкой границы, каждое расширение по-отдельности как-то модифицирует систему типов.

грубо говоря, хаскель при этом аж целое семейство языков сменил, Д-М хаскель - это эмельный родственник, а модерновый - совсем нет, нет лет-полиморфизма - не 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. Очень нравится этот абзац.

чёрт, сосисочная вечеринка в сауне срывается

не буду даже шутить на эту тему, а то у меня с этим митапом какие-то сорокинские асоциации

День функциональщика

карируете там небось

как вообще к этому пришли? на последнем митапе кто-то встал и предложил мол давайте в сауну и все зааплодировали и каждый сказал что обязательно пойдёт?

@qnikst а мемори профайлер как-то можно заставить правильное время рисовать?

не видел, вроде только cpu

я про время снятия сэмплов

запускаю приложение на 1 минуту

в профайле хипа последняя строчка END_SAMPLE 3.777820

писать в eventlog, там нормальное время?

блин, eventlog это только в 8.2 :(

там cputime не знаю что с этим сделать

я понял про что ты

даж тикетов об этом нет? а какой именно cputime там?

евентлог по идее должен нормальное же время давать, но не понимаю как с графиками сэмплы соотносить тогда

CPU_TIME это часы которые меряют сколько твоя программа занимала cpu

т.е. если оно жрет проц то будет похожее время, если в idle дофига то твое время будет меньше реального

не уверен что есть баг

в данном случае почти idle, да

https://github.com/ekmett/ekmett.github.com/blob/master/presentations/Functional%20Reporting.pdf

старый который переэмель с лет-полиморфизмом и тот, когда включаются какие-то поверхностные проявления FC и, соотв. вывод типов не Дамас-Милнер становится

А разве в хаскеле по умолчанию H-M, а не 2-ранговый System F?

по умолчанию OutsideIn как HM работает

Странно, а почему не system f второго ранга?

почему странно?

Странно, а почему не system f второго ранга?

подключишь батарею из прагм и будет тебе

почему странно?

Потому что system f2 это расширение Х-М, не нарушающее его свойств же

Почему System F не включают понятно — тайп инференс рушится

а что system f2 дает над hm?

Можно ~грабить корованы~фигачить экстенсионалы

ну экстенсионалы тоже по дефолту не включены, нужно -XExistentialQuantification

подключишь батарею из прагм и будет тебе

нет, у ghc rank2 не включается в принципе, только сразу rankN

но было время..

а что тогда делает Rank2-расширение? Алиас на RankN?

да

Я не о расширении синтаксиса, а о (forall r. (forall a. X) -> r)

нет, у ghc rank2 не включается в принципе, только сразу rankN

Rank2? вроде же есть

было время это оно не так было

да

А OutsideIn гарантирует инференс, если у нас только rank2?

ну еще ExistentialQuantification есть вроде

не помню

Кстати, почему в ghc такой странный для экзистенционалов синтаксис. Почему forall????

Кстати, почему в ghc такой странный для экзистенционалов синтаксис. Почему forall????

https://en.wikibooks.org/wiki/Haskell/Existentially_quantified_types

чтобы кейворды не плодить

да вроде вполне адекватно

в расте &dyn Typeclass

ну вопрос был типа почему не exist

Кстати, почему в 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

много туда движения

ERROR: S client not available

и то, что я недавно нашел странную вещь * :: * - не баг, это новая фича - первая фаза внедрения завтипов

С хаскелем не соскучишься T_T

?

Ну большинство вещей для DT в хаскель написала Стефани Вейрих

и то, что я недавно нашел странную вещь * :: * - не баг, это новая фича - первая фаза внедрения завтипов

есть еще специальная библиотека для накостыливания недозавтипов на синглетонах

есть еще специальная библиотека для накостыливания недозавтипов на синглетонах

Ага, я вроде даже пример видел в eta lang

есть еще специальная библиотека для накостыливания недозавтипов на синглетонах

ты про singletons? Да, все эти костыли для эмуляции завтипов я видел ранее, а тут прям что-то реальное делается, только без универсумов

подступает 2k18, люди узнают про TypeInType

ну я сразу еще фаст форвард сделаю до момента, как вы узнаете, что он сломан

если попытаетесь использовать

о, а в чем сломан?

https://ghc.haskell.org/trac/ghc/ticket/12919 https://ghc.haskell.org/trac/ghc/ticket/12564

я в принципе только недавно про хаскель узнал-то

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

в первом тикете прям довольно тривиальная вещь и не работает, странно

Во втором тоже базовая.

Я говорю — он сломан, это не минорные баги.

Это core lint failures и полная неюзабельность промоутных GADT-ов (main selling point of TypeInType).

Я его включаю для кайнд-синонимов

А что-то толковое выжать на данный момент трудно.

и то, что я недавно нашел странную вещь * :: * - не баг, это новая фича - первая фаза внедрения завтипов

Всё очень плохо, если зав. типы начинают внедрять с парадокса жирарда..

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. Очень нравится этот абзац.

Не, все очень хорошо, это правильный дизайн для Haskell

По-моему произошло что-то очень странно и программисты стали воспринимать зависимые типы как ещё один способ полиморфизма >...>

Даже в Agda сначала иногда с --type-in-type доказываешь для удобства, потом делаешь нормально.

Но с type in type можно доказать что угодно

например exist n : M, even(n) -> |M| > 0 = (forall n : M, even(n)) -> |M| > 0 тут же первое утверждение верное, а второе нет.

Это мощность типа?

Нельзя

Но с type in type можно доказать что угодно

У тебя предположение, что есть proof erasure.

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. Очень нравится этот абзац.

Though this causes inconsistency in other dependently-typed languages, it does not in Haskell, essentially because equality proofs are written in a different sub-language than ordinary terms. See ​our paper [http://www.seas.upenn.edu/~sweirich/papers/fckinds.pdf] for more details.

А в Хаскеле пруфы надо редьюсить до NF

Это мощность типа?

ну там пример про множества, не про типы, логика кванторов та же, полагаю