@haskellru - страница 906 - Telegram web archive

A64m

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

Viacheslav

В Хаскеле 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 лет назад от хаскеля

A64m

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

Viacheslav

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

Viacheslav

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

Евгений

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

Viacheslav

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

Viacheslav

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

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

A64m

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

Евгений

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

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

A64m

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

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

Viacheslav

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

A64m

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

Евгений

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

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

Viacheslav

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

Viacheslav

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

Евгений

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

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

Евгений

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

Leonid 🦇

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

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

A64m

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

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

Евгений

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

A64m

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

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'ями

A64m

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

да, только с классами работает 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

Leonid 🦇

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

Leonid 🦇

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

t1db1t

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

Alexander

хм...

Quet

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

Vladislav

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

Vladislav

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

Cheese

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

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

t1db1t

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

Cheese

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

Quet

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

Aliester

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

Anonymous

да

кана

Для чего?

Vladislav

Лиспа нет

кана

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

кана

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

Anonymous

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

Vladislav

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

Vladislav

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

Anton

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

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

Anonymous

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

Vladislav

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

Vladislav

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

Cheese

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

Aliester

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

Anonymous

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

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

Aliester

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

Aliester

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

A64m

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

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

кана

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

Anonymous

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

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

кана

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

A64m

Лиспа нет

CL и есть лисп

Anonymous

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

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

Anonymous

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