Глеб
И вообще с I/O
Aleksei (astynax)
Майти, это warp, кстати. Про warp была давнишняя статья, в которой описывалось, почему оно быстро работает
Глеб
🆗
Vladislav
Vladislav
Это ко мне предъява сейчас была?
Vladislav
Пойдем выйдем поговорим
A64m
после того как @int_index топил за
data Foo where
type Foo
type Bar
type Baz
может пожертвовать им не такая и плохая идея
Vladislav
ну начнем с того, что то, что ты написал, не может работать
Vladislav
я топил за data Foo = type Bar | type Baz | type Quux
Vladislav
либо
data Foo where
type Bar :: Foo
type Baz :: Foo
type Quux :: Foo
A64m
да
Vladislav
а type Foo :: Foo работать не может
Vladislav
потому что это один неймспейс
A64m
но такого уровня повторения я бы уже не вынес
Vladislav
Так писал бы дальше
data Foo where
Bar :: Foo
Baz :: Foo
Quux :: Foo
Vladislav
ты еще не видел наверное где я топил за type [] Int вместо [Int], чтобы не было конфликта с '[Int] (который надо писать как [Int])
Vladislav
мне даже Эйзенберг сказал куда идти лечиться, но я своего мнения не поменял
A64m
это дискуссионно по крайней мере, совсем не тот уровень ужаса
Vladislav
это вообще-то одно и то же, явная квалификация неймспейса и там, и там
A64m
data type или type data было бы одно и то же, бессмысленное повторение ключевого слова n раз там где все равно нету возможности выбирать неймспейс для каждого конструктора, а только для всех разом - вот в чем проблема
Vladislav
я был за выбор неймспейса для каждого конструктора
A64m
т.е. Foo промоутится, Bar - нет, а Baz промоутится? в чем смысл этого-то?
Vladislav
да смысла вообще в двух неймспейсах нет, а если уж их два, то не понимаю, почему не дать fine-grained control
A64m
потому что ничем кроме бессмысленного повторения одного слова n раз это все равно не закончится?
Oleg
либо
data Foo where
type Bar :: Foo
type Baz :: Foo
type Quux :: Foo
я вот не пойму, это Вы тут скалу или скалу хотите в свои хашкели затащить
A64m
не надо говорить во множественном числе, второго человека который такое хочет нет
Oleg
не надо говорить во множественном числе, второго человека который такое хочет нет
ок, поправил на заглавную
Vladislav
я не знаю что там в Скале происходит, у них вместо тайпклассов имплиситы
Vladislav
дальше решил не изучать этот язык
A64m
там при объявлении "АлгТД" ключевое слово повторяется бессмысленно n раз
Oleg
там при объявлении "АлгТД" ключевое слово повторяется бессмысленно n раз
я попрошу!
три ключевых слова
Oleg
final case class
final case class
Oleg
но уже есть игрушечная скала, где не так
A64m
уже придумал как улучшить пропозал
data Foo = promoted data constructor Bar | promoted data constructor Baz | promoted data constructor Quux
Vladislav
Vladislav
но я тут последние пару дней снова в коде GHC рыскаю, так что мне кажется лучше писать pm_d_con
Vladislav
так сразу понятнее о чем речь
Oleg
уже придумал как улучшить пропозал
data Foo = promoted data constructor Bar | promoted data constructor Baz | promoted data constructor Quux
всё-таки для того, чтобы он был окончательно хорош, нужно запретить объявлять их не в GADT форме
Aleksei (astynax)
Если я имею
data Tag = A | B | C
class Foo (tag :: Tag) where
f :: Bar
я ведь не могу просто так сделать что-то вроде
map (_ f) [A, B, C]
?
Aleksei (astynax)
Или, скажем, написать такой кодек для Aeson, который позволит декодировать с учётом тега
map _ [ByteString] :: [Maybe Bar]?
Aleksei (astynax)
Потому как 'A и 'B - разные типы?
Aleksei (astynax)
Или можно суммой вида
data Taged
= TA (Proxy 'A)
| TB (Proxy 'B)
| TC (Proxy 'C)
выкрутиться?
Aleksei (astynax)
После промоута то разные "типы" же, не?
Cheese
ладно, выше уже обсудили
Cheese
вроде всё можешь
Cheese
только просто так f не напишешь, потому что из Bar не выводится t :: Tag
Cheese
можно f @tag
Vladislav
У тебя f :: forall (tag :: Tag). Foo tag => Bar, а для такого кода тебе надо f :: pi (tag :: Tag) -> Bar
Aleksei (astynax)
Вот интуитивно я как-то так и думаю
Vladislav
Ну pi-то нет без синглтонов
Aleksey
Если я имею
data Tag = A | B | C
class Foo (tag :: Tag) where
f :: Bar
я ведь не могу просто так сделать что-то вроде
map (_ f) [A, B, C]
?
в сигнатуре f тебе надо tag в каком то виде
Cheese
Это когда tag известен
можно передать снаружи как переменную, если он известен не здесь, а снаружи
Vladislav
Выкрутишься либо через
data WithFoo where
WithFoo :: Foo a => Proxy a -> WithFoo
map (_ f) [WithFoo (Proxy @A), WithFoo (Proxy @B), WithFoo (Proxy @C)]
либо через map (_ f) [toSing A, toSing B, toSing C] с синглтонами
Vladislav
могу подробнее расписать каждый из вариантов, если не очевидно
Vladislav
но смысл в том, что без нормального pi надо лифтать, либо открытым стилем (через констрейнт), либо закрытым (через синглтоны)
Aleksei (astynax)
Вот и я про прокси подумал
Vladislav
Так там главное не Proxy, а словарик Foo внутри. Proxy можно будет убрать, когда экзистенциальные переменные биндить научимся
Vladislav
https://github.com/ghc-proposals/ghc-proposals/pull/126
Vladislav
После этого пропозала я бы так написал:
data WithFoo where
WithFoo :: Foo a => WithFoo
Vladislav
В общем-то надо понимать, что это roundabout способ сделать то же самое, что
[ f @A, f @B, f @C ]
только вместо конечного Bar там весь словарь лежит. Это имеет смысл только если какие-то другие методы в словаре есть
Vladislav
а вот синглтоны это уже плюс-минус честный способ хранить там именно значение типа Tag, по которому поматчиться можно
Vladislav
Хм, а наверное toSing и помэппить можно.
Vladislav
Тогда даже
map (_ f) [A, B, C]
прокатит как изначально прошено
Cheese
кстати, если я хочу data использовать только на уровне типов, можно сказать компилятору, чтобы он принимал их спокойно без тиков?
Vladislav
недавно приняли пропозал, с которым сможешь так сказать
Vladislav
type data Foo = Bar | Baz | Quux
Vladislav
оно сразу в тайплевельный неймспейс попадёт
Vladislav
Да, что имени нет в скоупе
Cheese
отлично
Vladislav
@astynax как-то так думаю
f' :: Tag -> Bar
f' (toSing -> SomeSing (stag :: STag tag)) = case stag of
SA -> f @tag
SB -> f @tag
SC -> f @tag
матчинг можно TH-ом автоматизировать, см. sCases
Aleksei (astynax)
Хмм. Спасибо, поизучаю!
Vladislav
тогда будет что-то вроде
f' :: Tag -> Bar
f' (toSing -> SomeSing (stag :: STag tag)) = $(sCases ''Tag [| stag |] [| f @tag |])
Vladislav
девочка спросила, когда в Haskell завезут зависимые типы
плакали всей маршруткой
Aleksei (astynax)
Aleksei (astynax)
Теперь осталось решить, надо ли это мне на самом деле...