в рекордах селекторы все-таки более необычные функции, из-за собственного неймспейса рекордов, TDNR, роу-полиморфизма
А есть пейперы на теоретическое осмысление понятия рекордов?
Евгений
A64m
в хаскеле надо было как в окамле делать простые и убогие рекорды и навороченные. Но нет, такое решение почему-то затряло, как будто все остальные фичи в хаскеле не продублированы.
A64m
с рекордами и модулями комитетчики нас, хаскелистов, сильно подвели
Viacheslav
Видели бы вы рекорды в идрисе
Viacheslav
вот это топчик
Viacheslav
там даже можно поля называть одинаково в разных рекордах в одном модуле
Viacheslav
и никаких проблем с этим нет
Alexander
прямо как в haskell?
A64m
там даже можно поля называть одинаково в разных рекордах в одном модуле
в идрисе из-за перегрузки нужно применять квалификацию чуть менее чем везде. Я с таким адским адом еще ни в однм ФЯ не сталкивался, это наверное 30% моей ненависти к идрису обсепечило
Viacheslav
угу, если никаких проблем нет — это подключить пару расширений и все равно работает через одно место
Viacheslav
Alexander
GHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help
IO error: "//usr/share/ghc-vis-0.8/ghc-8.0.1/ghci" does not exist
Loaded GHCi configuration from /home/qnikst/.ghci
[1 of 1] Compiling Main ( 99877.hs, interpreted )
Ok, modules loaded: Main.
*Main> :i A
data A = A {Main.foo :: Int} -- Defined at 99877.hs:1:1
*Main> :i B
data B = B {Main.foo :: String} -- Defined at 99877.hs:2:1
Viacheslav
никаких проблем с этим не встречал
A64m
но в идрисе через это место вообще все имена работают
Alexander
я встречал
Alexander
бесит вечно когда требуются квалифицированные имена в каждой третьей строке
Alexander
если вектора и списки в одном файле есть, например
Alexander
с конструкторами та же фигня
A64m
при том что типами и так все проаннотировано, все равно не понимает ничерта, давай, давай, квалифицируй, к такому меня жизнь не готовила
Viacheslav
Viacheslav
любым из
Viacheslav
при том что типами и так все проаннотировано, все равно не понимает ничерта, давай, давай, квалифицируй, к такому меня жизнь не готовила
примеров бы, а то может не разобрались просто до конца?
A64m
foo (a :: A)
A64m
foo (b :: B)
Viacheslav
и что с этим не так?
A64m
вербозно, но так рекорды в хаскеле вообще не нужно применять, надо через RecordWildcards
Leonid 🦇
или lens
Viacheslav
ну потом просто возникает проблемы с тем, чтобы достать из рекорда что-то и проекции не работают(
Alexander
в любом случае с идрисом было хуже
A64m
примеров бы, а то может не разобрались просто до конца?
может и не разобрались, но от этого не легче
Alexander
количество боли даже при простых задачах из курса Брагилевского было слишком много
Viacheslav
в любом случае с идрисом было хуже
а я вот пописал пару месяцев на идрисе для души, потом пару месяяцев на хаскелле
A64m
Viacheslav
и могу сказать, что убогие рекорды в хаскелле по сравнению с идрисом боьше всего бесили
Viacheslav
но это ИМХО
Viacheslav
может я тоже не разобрался
Leonid 🦇
А нет предложений для расширения отключающего вообще генерацию ацессоров? а то префиксить линзы (или поля) бесит чутка
Alexander
ну мне тяжело, я не могу поработать на идрисе сравнимое с haskell время, он сдохнет раньше
A64m
меня бесит плохой вывод типов, хаскельные рекорды бесят, но и близко не как плохой вывод типов, так что я не фанат TDNR
Viacheslav
В идрисе нет вывода типов
Leonid 🦇
А нет предложений для расширения отключающего вообще генерацию ацессоров? а то префиксить линзы (или поля) бесит чутка
ну т.е. в RecordWildCards матчилось, a foo :: Bar -> Baz не было
Viacheslav
В идрисе зависимые типы и там задача вывода типа в общем случае неразрешима
A64m
В идрисе зависимые типы и там задача вывода типа в общем случае неразрешима
в общем случае она и в хаскеле неразрешима, в частных, вполне распространенных случаях она разрешима еще как и этом можно пользоваться
Vladislav
А в DependentHaskell зависимые типы и вывод типов, вот так на.
Alexander
а у нас есть TClosableTChan которые клонировать можно?
Alexander
@int_index насколько мне известно в общем случае в зависимых типах задача неразрешима
Viacheslav
мне казалось что вроде как раз разрешима, если какую-то совсем дичь не брать
Viacheslav
в System F с этим все хорошо
Alexander
общем случае = с зависимыми типами
Viacheslav
в хаскелле нет зависимых типов
Viacheslav
пока нет депендент хаскелля
Alexander
в telegram не хвататет тредов
Leonid 🦇
/me всегда выступал за сильные, независмые типы.
Vladislav
@int_index насколько мне известно в общем случае в зависимых типах задача неразрешима
Просто это не блокер для того, чтобы вывод типов был.
Антон
Правда, я не считаю это хорошей вещью
A64m
в хаскелле нет зависимых типов
для того чтоб испортить вывод типов в общем случае GADT достаточно
Vladislav
Vladislav
А дальше Эйзенберг рассказывает про то, как он печёт пироги
Антон
в плюсах норм. там главное все аргументы как explicit пометить.
Лень. Плюс в нормальных языках вообще нет такой фигни, как имплисит конструктор
Leonid 🦇
нормальных языков не бывает
Vladislav
А дальше Эйзенберг рассказывает про то, как он печёт пироги
У него описан алгоритм Bake, который дает type inference / type checking для Haskell, и выдает Pico (аналог System FC, который потом перерос в System D)
Vladislav
И вот у нас есть singletons, для которых вывод типов уже есть. А потом мы заменим их на pi-квантификатор, и что, вывод типов куда-то деться должен?
A64m
я про data Foo = Foo { bar :: Int } и bar :: Lens' Foo Int
Prelude> :set -XDuplicateRecordFields
Prelude> data Foo = Foo { foo :: Int }
Prelude> :set -XRecordWildCards
Prelude> foo Foo{..} = foo
Prelude> foo $ Foo 42
42
A64m
ну и линзы соотв. можно
Leonid 🦇
это всё меняет
Vladislav
для того чтоб испортить вывод типов в общем случае GADT достаточно
Вот именно, только никто этим не прикрывается, и в GHC для частных случаев с GADT все более менее нормально работает.
Vladislav
А в Idris сказали "у нас dep types!!1" и забили на inference.
Евгений
В идрисе зависимые типы и там задача вывода типа в общем случае неразрешима
В Хаскеле System F, для него тоже вывод типов неразрешим.
https://web.archive.org/web/20070929211126/http://www.church-project.org/reports/Wells:APAL-1999-v98-no-note.html
A64m
Вот именно, только никто этим не прикрывается, и в GHC для частных случаев с GADT все более менее нормально работает.
ну да, я об этом и говорю, могли бы за хоть какой-то вывод типов побороться
A64m
у завтипщиков просто теперь парадигма такая, вывод типов нам не интересен, мы теперь программы выводим