особенно первое

дикий трэш

не ну мне решение понятно и оно красивое довольно, да и работать в принципе достаточно удобно

просто это не для реального мира (да и то зависит от задач наверное))

Ну да

universim лучше гораздо и в нём нет этого говна?)

нету хороших прелюдий

universum нормальный

ну я с ним работал не так много, но мне нравится намного лучше бейса какое-то говно в нем наверняка есть, нужно просто найти

например когда нужны кметовские линзы, а универсум экспортит микролинзы они в принципе совместимы вроде, типы же одинаковые, просто могут быть ambiguous

/me пользуется base в 90% случаев

+ custom prelude под проект

иногда

например когда нужны кметовские линзы, а универсум экспортит микролинзы они в принципе совместимы вроде, типы же одинаковые, просто могут быть ambiguous

а если призмы нужны?

кстати как часто нужны призмы людям?

так в микролинзах есть призмы же

зато траверсалов нету

а траверсалы нужны

в смысле нету?

возможно нужны какие-то очень крутые траверсалы, я не сильно шарю в линзал, но https://hackage.haskell.org/package/microlens-0.4.8.1/docs/Lens-Micro.html#g:6

раньше не было во всяком случае

да не, траверсалы там с первой версии, как без них

хм поспать делал что в микролинзах нет призм окей

почему то*

думал*

может с какими другими минималистичными линзами я путаю..

траверсалы то всегда есть, их классами и base делать можно, вот призмы дополнительных зависимостей требуют, от профункторов

кстати вопрос к едущим на fby кто где там проживать будет?

а да, логично

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

кстати вопрос к едущим на fby кто где там проживать будет?

fbу?

fby.by

там еще 5 билетов есть

а обратно когда и на чем (те кто из питера)?

А напомните пожалуйста, или дайте ссылку почему в ФП от bottom type нельзя избавиться?

@A64m_qb0 вон что в планах на 8.4 > Improved Windows support, including support for split sections and long file paths (Tamar Christina) А ты говоришь не работают над виндой и путями

https://ghc.haskell.org/trac/ghc/wiki/Status/GHC-8.4.1

о, чего-то я путей не заметил.

А напомните пожалуйста, или дайте ссылку почему в ФП от bottom type нельзя избавиться?

Почему нельзя? См. total functional programming

А напомните пожалуйста, или дайте ссылку почему в ФП от bottom type нельзя избавиться?

почему в фр не могут быть только unlifted объекты?

@A64m_qb0 вон что в планах на 8.4 > Improved Windows support, including support for split sections and long file paths (Tamar Christina) А ты говоришь не работают над виндой и путями

что-то не видно только никаких следов добавление поддержки длинных путей. (соотв. тикеты и диффы на фабрикаторе для split sections я видел, но там не доделано еще)

Вот и я не нашёл

Может они про пути в билде гхц только?

можно ли это юзать как квантор существования? 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/

можно ли это юзать как квантор существования? exists x. https://hackage.haskell.org/package/exists-0.2/docs/Data-Exists.html

Только если констрейнт там выбрать никакой

class Vacuous a instance Vacuous a

Exists Vacuous эквивалентно квантору существования

Иначе это квантор существования + словарик

А если в качестве констрейнта выбрать SingI или Typeable, то будет сигма

Акция невиданной щедрости - при присвоении имени полю в собственном типе - геттер и сеттер в подарок!

А если в качестве констрейнта выбрать SingI или Typeable, то будет сигма

так сигма это и есть exists

Простите, не удержался, я только учусь :(

pi это forall

Сигма это пруфрелевантный exists

pi это пруфрелевантный forall

а при чем тут тогда равенство по Лейбницу?

А кто говорил про равенство по Лейбницу? (Я вообще не понял при чем тут это)

https://t.co/zmiy33Cdpt

просто в purescript через это Exists делают, GADTs

Сигма это пруфрелевантный exists

когда там уже ваша книга выйдет?) для адвансед мод

forall и pi разные, forall параметричный, id :: forall a. a -> a не может ничего с a сделать, id :: pi a. a -> a может. Во всяких Coq/Agda где forall энкодят через pi, они всунули параметричность хакнутым образом для * (а остальные кайнды не параметричны)

В DependentHaskell будет нормально, по заветам МакБрайда

два квантификатора отдельных

ERROR: S client not available

ну как бы про DT я смотрел https://www.youtube.com/watch?v=ISGENChlA4M&list=PLvPsfYrGz3wufQguebnCduYgQQ9UMeJRt

когда там уже ваша книга выйдет?) для адвансед мод

На этой или следующей неделе выйдут два драфта про парсинг

На этой или следующей неделе выйдут два драфта про парсинг

а как можно получить early access?

согласиться помимо чтения оставлять комментарии (т.е. ревьюить) и попросить инвайт у @lightgreen

@int_index можешь объяснить эту магию? https://gist.github.com/int-index/d35255377b1ee05780eb9e006959bccb

Я ничего не помню, там кто-то в Twitter упражнение запостил, я просто заставил типы сойтись

ну идею вот этих Data.Constraint.Forall

в пурсе вот это http://try.purescript.org/?gist=1304cf5bdc3af1cefa5f0a9e263d5d49&session=0548d95f-ace6-0132-6b53-a4c79b686f4a

в Haskell это для констрейнтов сделано, потому что forall слева от => использовать нельзя

А в PS я слабо понимаю что там в этом файле происходит, там ведь RankNTypes из коробки

как это вообще компилится?

На тёрмах конструктор если 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

Я понял, там type Maybe свой, а не из прелюда

Он уже включает в себя Forall

newtype Maybe' a r = Maybe' {runMaybe :: r -> (a -> r) -> r} это вообще Черч

Да, я понял, они CPS -нули всё и радуются

и какой профит оборачивать Черча в Forall?

Это похоже на упражнение о том, как программировать без ADT

Типа, смотрите, одни функции остались и ньютайпы, а у нас Maybe

согласиться помимо чтения оставлять комментарии (т.е. ревьюить) и попросить инвайт у @lightgreen

а на русском языке комментировать можно?

Да

а пожелания?

Тогда я бы покомментировал

Да, в этом смысл, фидбек в общем

(было бы что)

Почти все главы сейчас на (1), пара на (2)

И две главы про парсинг до конца недели планируется довести до начала (3), чтобы опубликовать drafts

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.