ᛏᚺᛖ ᛚᛖᛋᛒᛁᚨᚾ ᛗᚨᚾ ᚷᛁᚱᛚ 🐝
думал*
Alexander
может с какими другими минималистичными линзами я путаю..
A64m
траверсалы то всегда есть, их классами и base делать можно, вот призмы дополнительных зависимостей требуют, от профункторов
Alexander
кстати вопрос к едущим на fby кто где там проживать будет?
Alexander
а да, логично
кана
квартиру сняли через букинг где-то на немиге
кана
fby.by
кана
там еще 5 билетов есть
Alexander
а обратно когда и на чем (те кто из питера)?
Michel
А напомните пожалуйста, или дайте ссылку почему в ФП от bottom type нельзя избавиться?
Leonid 🦇
@A64m_qb0 вон что в планах на 8.4 > Improved Windows support, including support for split sections and long file paths (Tamar Christina) А ты говоришь не работают над виндой и путями
Leonid 🦇
https://ghc.haskell.org/trac/ghc/wiki/Status/GHC-8.4.1
A64m
о, чего-то я путей не заметил.
A64m
@A64m_qb0 вон что в планах на 8.4 > Improved Windows support, including support for split sections and long file paths (Tamar Christina) А ты говоришь не работают над виндой и путями
что-то не видно только никаких следов добавление поддержки длинных путей. (соотв. тикеты и диффы на фабрикаторе для split sections я видел, но там не доделано еще)
Leonid 🦇
Вот и я не нашёл
Leonid 🦇
Может они про пути в билде гхц только?
Зигохистоморфный
можно ли это юзать как квантор существования? exists x. https://hackage.haskell.org/package/exists-0.2/docs/Data-Exists.html
Зигохистоморфный
внезапно это может exists x. как keyword http://foswiki.cs.uu.nl/foswiki/Ehc/LanguageFeatures
Зигохистоморфный
http://blog.ezyang.com/2010/10/existential-type-curry/
Vladislav
class Vacuous a instance Vacuous a
Vladislav
Exists Vacuous эквивалентно квантору существования
Vladislav
Иначе это квантор существования + словарик
Vladislav
А если в качестве констрейнта выбрать SingI или Typeable, то будет сигма
kosc
Акция невиданной щедрости - при присвоении имени полю в собственном типе - геттер и сеттер в подарок!
kosc
Простите, не удержался, я только учусь :(
Зигохистоморфный
pi это forall
Vladislav
Сигма это пруфрелевантный exists
Vladislav
pi это пруфрелевантный forall
Зигохистоморфный
а при чем тут тогда равенство по Лейбницу?
Vladislav
А кто говорил про равенство по Лейбницу? (Я вообще не понял при чем тут это)
Зигохистоморфный
https://t.co/zmiy33Cdpt
Зигохистоморфный
просто в purescript через это Exists делают, GADTs
Зигохистоморфный
Сигма это пруфрелевантный exists
когда там уже ваша книга выйдет?) для адвансед мод
Vladislav
forall и pi разные, forall параметричный, id :: forall a. a -> a не может ничего с a сделать, id :: pi a. a -> a может. Во всяких Coq/Agda где forall энкодят через pi, они всунули параметричность хакнутым образом для * (а остальные кайнды не параметричны)
Vladislav
В DependentHaskell будет нормально, по заветам МакБрайда
Vladislav
два квантификатора отдельных
Зигохистоморфный
ну как бы про DT я смотрел https://www.youtube.com/watch?v=ISGENChlA4M&list=PLvPsfYrGz3wufQguebnCduYgQQ9UMeJRt
Vladislav
когда там уже ваша книга выйдет?) для адвансед мод
На этой или следующей неделе выйдут два драфта про парсинг
Зигохистоморфный
Vladislav
согласиться помимо чтения оставлять комментарии (т.е. ревьюить) и попросить инвайт у @lightgreen
Зигохистоморфный
@int_index можешь объяснить эту магию? https://gist.github.com/int-index/d35255377b1ee05780eb9e006959bccb
Vladislav
Я ничего не помню, там кто-то в Twitter упражнение запостил, я просто заставил типы сойтись
Зигохистоморфный
ну идею вот этих Data.Constraint.Forall
Зигохистоморфный
в пурсе вот это http://try.purescript.org/?gist=1304cf5bdc3af1cefa5f0a9e263d5d49&session=0548d95f-ace6-0132-6b53-a4c79b686f4a
Vladislav
в Haskell это для констрейнтов сделано, потому что forall слева от => использовать нельзя
Vladislav
А в PS я слабо понимаю что там в этом файле происходит, там ведь RankNTypes из коробки
Vladislav
Vladislav
как это вообще компилится?
Vladislav
На тёрмах конструктор если Forall, то на типах должно быть Forall Maybe
Зигохистоморфный
как это вообще компилится?
в чем парадокс что компилится
Зигохистоморфный
ну в хаскелл похожее вроде можно newtype Forall f = Forall (forall r. f r) runForAll :: forall f r o. (f r -> o) -> Forall f -> o runForAll f (Forall l) = f l newtype Maybe' a r = Maybe' {runMaybe :: r -> (a -> r) -> r} type MMaybe a = Forall (Maybe' a) nothing :: forall a. MMaybe a nothing = Forall (Maybe' const) just :: forall a. a -> MMaybe a just x = Forall (Maybe' $ \_ j -> j x) maybe :: forall a r. r -> (a -> r) -> MMaybe a -> r maybe n j = runForAll $ \(Maybe' f) -> f n j
Vladislav
Я понял, там type Maybe свой, а не из прелюда
Vladislav
Он уже включает в себя Forall
Зигохистоморфный
newtype Maybe' a r = Maybe' {runMaybe :: r -> (a -> r) -> r} это вообще Черч
Vladislav
Да, я понял, они CPS -нули всё и радуются
Зигохистоморфный
и какой профит оборачивать Черча в Forall?
Vladislav
Это похоже на упражнение о том, как программировать без ADT
Vladislav
Типа, смотрите, одни функции остались и ньютайпы, а у нас Maybe
Vladislav
Да
Зигохистоморфный
а пожелания?
A64m
Тогда я бы покомментировал
Vladislav
Да, в этом смысл, фидбек в общем
Vladislav
(было бы что)
Vladislav
Почти все главы сейчас на (1), пара на (2)
Vladislav
И две главы про парсинг до конца недели планируется довести до начала (3), чтобы опубликовать drafts
Vladislav
1. Collect all topics/info (in the "What This Chapter Should Contain" section, but perhaps as a draft of the chapter itself) 2. Plan pedagogy - the order of introducing these topics. Think carefully about the background of the reader and when to go into more details. 3. Find best phrasing and how to use English. For now I do it together with (1) and (2), but this will get more attention when we hire an editor.
Alexander
+
Зигохистоморфный
@int_index написал @lightgreen, жду ответа
A64m
На реддите запостили ссылку на летнее письмо СПЖ в котором он призывает "ребята, давайте жить дружно", в комментариях немедленно стеко-кабало-война разгорелась, естественно
Leonid 🦇
о, надо почитать
Leonid 🦇
(reddit, письмо уже читал летом)
Leonid 🦇
мощно, 67 комментов за 15 часов
A64m
> It was quite confusing for me when I posted a support question and some people started attacking cabal developers out of the blue. What was this all about?