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

@int_index насколько мне известно в общем случае в зависимых типах задача неразрешима

мне казалось что вроде как раз разрешима, если какую-то совсем дичь не брать

в System F с этим все хорошо

общем случае = с зависимыми типами

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

пока нет депендент хаскелля

ну т.е. в RecordWildCards матчилось, a foo :: Bar -> Baz не было

можно не префиксить

в telegram не хвататет тредов

/me всегда выступал за сильные, независмые типы.

@int_index насколько мне известно в общем случае в зависимых типах задача неразрешима

Просто это не блокер для того, чтобы вывод типов был.

можно не префиксить

чойта, две функции с одним именем не бывает.

чойта, две функции с одним именем не бывает.

Скажи это плюсистам

чойта, две функции с одним именем не бывает.

дак с дупликейт рекорд филдс же

можно не префиксить

я про data Foo = Foo { bar :: Int } и bar :: Lens' Foo Int

Правда, я не считаю это хорошей вещью

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

для того чтоб испортить вывод типов в общем случае GADT достаточно

Скажи это плюсистам

в плюсах норм. там главное все аргументы как explicit пометить.

для того чтоб испортить вывод типов в общем случае GADT достаточно

хм, согласен

А дальше Эйзенберг рассказывает про то, как он печёт пироги

в плюсах норм. там главное все аргументы как explicit пометить.

Лень. Плюс в нормальных языках вообще нет такой фигни, как имплисит конструктор

нормальных языков не бывает

А дальше Эйзенберг рассказывает про то, как он печёт пироги

У него описан алгоритм Bake, который дает type inference / type checking для Haskell, и выдает Pico (аналог System FC, который потом перерос в System D)

я про data Foo = Foo { bar :: Int } и bar :: Lens' Foo Int

так это будет работать

нормальных языков не бывает

Это да. Но есть такие, которые к этому приближаются

И вот у нас есть singletons, для которых вывод типов уже есть. А потом мы заменим их на pi-квантификатор, и что, вывод типов куда-то деться должен?

я про 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

ну и линзы соотв. можно

ну и линзы соотв. можно

обалдеть

это всё меняет

для того чтоб испортить вывод типов в общем случае GADT достаточно

Вот именно, только никто этим не прикрывается, и в GHC для частных случаев с GADT все более менее нормально работает.

А в 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

Вот именно, только никто этим не прикрывается, и в GHC для частных случаев с GADT все более менее нормально работает.

ну да, я об этом и говорю, могли бы за хоть какой-то вывод типов побороться

у завтипщиков просто теперь парадигма такая, вывод типов нам не интересен, мы теперь программы выводим

(правда выведение программ на практике не так здорово, как выведение типов где оно есть пока работает)

В Хаскеле System F, для него тоже вывод типов неразрешим. https://web.archive.org/web/20070929211126/http://www.church-project.org/reports/Wells:APAL-1999-v98-no-note.html

ну ок, без учета first-class polymorphism, надо было точнее выразиться

Без учёта first-class polumorphism это уже Х-М и ML, немного на 30 лет назад от хаскеля

ну меньше, на 10

ну если ты в 2040 живешь, то может и на 30)

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

Если забить на вывод типов, то достаточно агды

тем более что top-level код типами аннотировать вроде как правильно

Если забить на вывод типов, то достаточно агды

осталось только прекратить там использовать весь utf и сделать простой IO

решение не было норм, да и то что там TDNR тупой это решение никак не извиняет, в языке где аннотации типов обязательные перегрузка вообще идеально должна работать, в идрисе это не так

ну меньше, на 10

Оригинальный пейпер Хиндли 69'ый год

Оригинальный пейпер Хиндли 69'ый год

Милнер же его не читал и сам изобрел в конце 70-х

оригинальный про System F где-то там же, но в общем это ни о чем не говорит

так что на мл это 69 не рапространяется

оригинальный про System F где-то там же, но в общем это ни о чем не говорит

Мы о тайп инференс говорим. До 94'ого вывод типов System F никто и не исследовал всерьёз, а на практике юзали Х-М

Coq вроде пораньше появился 94-го

так что не только Х-М

Милнер же его не читал и сам изобрел в конце 70-х

Ну даже если конец 70'ых, всё равно 25 лет получается. Тикет по rank-n-types открыт только в 2005 году: https://prime.haskell.org/ticket/60

Пейпер по OutsideIn(X) — 11'ый год

ну и линзы соотв. можно

чёт у меня даёт функцию определить, а потом жалуется при попытке применить :(

Ну даже если конец 70'ых, всё равно 25 лет получается. Тикет по rank-n-types открыт только в 2005 году: https://prime.haskell.org/ticket/60

они раньше в хаскеле появились, ранк-2 так вообще в начале 90

Ну судя по истории тикета не оч

Ну судя по истории тикета не оч

5.04 (11 July 2002) The type system now supports full rank-N types (previously only limited rank-2 types were supported) rank-2 используется в пейпере по ST 94-го года, т.е. в версиях 0.X уже было

Rank 2 это всё-таки Х-М на дрожжах, хотя конечно это уже прогресс по сравнению с ML'ями

чёт у меня даёт функцию определить, а потом жалуется при попытке применить :(

да, только с классами работает data FooBar = FooBar { foo :: Int, bar :: Bool } data BarFoo = BarFoo { bar :: Bool, foo :: Int } class Foo a where foo :: a -> Int instance Foo FooBar where foo FooBar{..} = foo instance Foo BarFoo where foo BarFoo{..} = foo t1 = foo $ FooBar 42 True t2 = foo $ BarFoo True 24

у меня и с классами в t1, t2 жалуется

может потому что у меня один из рекордов импортируется

https://www.youtube.com/watch?v=9SOFqWYpf9Y

хм...

а что плохого в hpack?

в видео втирают, что типы это "не столь важно"

ERROR: S client not available

правильно их в кутузке везут, за такую ересь

а что плохого в hpack?

ничего. разве что отстаёт от Cabal по фичам

их за распитие везут

и йамл плох сам по себе

ну что отстает эт само собой но догонят еще ) там просто выше ругали снойманитов в том числе за него

стоит ли учить лисп?

да

Для чего?

Лиспа нет

Вообще да, просто цели интересуют

Сикп например почитать стоит имхо

Плагины для емакса сами себя не напишут.

В Лиспы валят тупо всё с S-exp, это настолько широкая категория, что ничего нельзя сказать про них толкового.

Вот да. Emacs Lisp придется изучить хочется того или нет.

Вот да. Emacs Lisp придется изучить хочется того или нет.

Я упорно сопротивляюсь )

А знаешь elisp, считай, выучил CL какой-никакой.

А в Racket говорят система макросов клёвая, но я никогда не использовал. Советую посмотреть доклад Alexis King про Hackett (с 2016), там демка впечатляет.

https://www.youtube.com/watch?v=TfehOLha-18

разве кому-то нужны плагины для Емакса? есть же текстовые редакторы

я оканчиваю ВУЗ и полвуза работаю миморубистом. я уже вышел на уровень осознания собственного говнокодерства, но еще не полностью знаю как из него выбираться. изучение lisp и сопутствующих MOOCов поможет руки и сознание выпрямить?

разве кому-то нужны плагины для Емакса? есть же текстовые редакторы

Ну вот когда напишут Proof General, agda-mode и org-mode под имя-вашего-модного-редактора-на-электроне-2018, тогда и поговорим. ?

я вообще вим юзаю

спейсмакс неасилил

А знаешь elisp, считай, выучил CL какой-никакой.

CL не такой ужас

Да, спейсмакс чет сложный после вима

я оканчиваю ВУЗ и полвуза работаю миморубистом. я уже вышел на уровень осознания собственного говнокодерства, но еще не полностью знаю как из него выбираться. изучение lisp и сопутствующих MOOCов поможет руки и сознание выпрямить?

Нет, не поможет. Но поможет понять что не так с Руби. Матцумото же вдохновлялся елиспом, даже хуже. Ну поймешь происхождение интересныех конструкций типа ?a , catch / throw и тп.

И вообще имакс чет сложный

Лиспа нет

CL и есть лисп

CL не такой ужас

Разумеется. Взять хотя бы неймспейсы.

Ладно, не буду оффтопить.

Нет, не поможет. Но поможет понять что не так с Руби. Матцумото же вдохновлялся елиспом, даже хуже. Ну поймешь происхождение интересныех конструкций типа ?a , catch / throw и тп.

думаю кэтч/троу скорееиз смолтолка вообще не знал что там елисп был в списке вдохновений

думаю кэтч/троу скорееиз смолтолка вообще не знал что там елисп был в списке вдохновений

Не, я говорю про http://www.lispworks.com/documentation/lw50/CLHS/Body/s_catch.htm Или https://ruby-doc.org/core-2.5.0/Kernel.html#method-i-throw