Programming in Martin-Lof Type Theory

Morten Heine B. Sørensen and Pawel Urzyczyn «Lectures on the Curry-Howard Isomorphism»

спасибо

ёптель, несколько часов ломал голову об четырёхстраничную ошибку серванта, который не мог какие-то там типы свести

оказалось, я смотрю в документацию 0.8.1, а у меня 0.11

с сообщениями об ошибках серванту явно надо что-то делать

точнее, не серванту, а ghc

нужно чтобы он писал что возможно вы используете не ту версию?

ошибка была в том, что раньше Handler был алиасом для ExceptT, а теперь он newtype над ExceptT

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

было бы здорово видеть что-то типа couldn't match type Handler with ExceptT ... , но там было что-то очень жуткое

спасибо

мир функционалу

Так вроде же только вчера вышла библиотека, которая помимо прочих плюшек заодно и немного улучшает сообщения об ошибках серванта https://www.reddit.com/r/haskell/comments/6lvf2k/so_long_and_thanks_for_all_the/

https://github.com/haskell-wasm/wasm

Всё равно скорее всего будет жирновато

Есть же purescript

PureScript и GHC2WAsm, это две большие разницы. PureScript, это hosted язык, не имеющий своего ничего - ни GC, ни вообще рантайма. Haskell всё это имеет, а значит сможет запускаться на wasm, где языку нужно уметь и с памятью работать и с асинхронностью и проч (поэтому, кстати, жирновато будет у всех, кто будет запускаться на wasm - рантайм нужно с собой тащить, т.к. это уже не "compile to JS")

purescript компилится в js, у которого есть и gc, и рантайм, а у wasm ничего этого нет

интересный проект, но, мне кажется, преимуществ перед ghcjs у него нет

GHCJS компилится в JS, получаем один рантайм поверх другого с инородным GC и прочими прелестями. На wasm Haskell сможет работать со своим родным рантаймом - родным GC тем же. Тут как раз важно, что Haskell умеет всё сам, в отличие от Purs, и поэтому может получать профит от wasm - пропадает ненужная прослойка в виде JS VM

Имхо есть - собстно как минимум отсутствием компиляции в js

Имею опыт применения GHCJS "в продакшне". Результат лучше конечным пользователям не показывать - одна только скорость раскочегаривания рантайма сделает кого угодно грустным

Для b2b ещё сойдет - кому надо, те потерпят. Но не более

Пользы от wasm нынче мало потому, что браузерное API ещё толком не завезли туда и писать по сути можно только ускорятки числодробления, которые вызываться будут из "старого доброго" JS

Вот когда API для доступа к DOM и прочим WebGL будет доступен из wasm напрямую - заживём.

в хаскелле есть библиотека/фреймоври или еще что-нибудь в таком духе в названии которого присутствует "hero"?

лол

лол

шшшшшшшшшшшшш

.-.

ложная тревога

улетаю

вжук

Хаскелю не хватает героя

Лямбдамэн (Wadler) же! :)

purescript компилится в js, у которого есть и gc, и рантайм, а у wasm ничего этого нет

Для wasm сейчас идёт речь о том, чтобы gc делать (предлагали участвовать)

Единый GC для всех - плохая идея.

Единый GC для всех - плохая идея.

Если отключаемый — наоборот

Функциональным языкам с персистентными иммутабельными структурами данных нужен GC, хорошо работающий с объектами малого размера и малого времени жизни. Для ООП-языков наоборот - с толстыми долгоживущими объектами

Языкам с линейными типами вообще не нужен GC

Так что "one GC to collect them all", это утопия и плохая идея

Gc будет ближе к gc для функциональных языков

Очевидно, что java в вебе как-то не зашла и ещё раз пытаться наступить на те же грабли смысла нет))

Я не специалист по gc, но слушал нескольких хороших специалистов (типа William D Clinger). Моё впечатление таково, что это вполне реалистичная идея, так как на практике между языками алгоритмы сборки одни и те же используются

### Approach * Only basic but general structure: tuples (structs) and arrays. * No heavyweight object model. * Accept minimal amount of dynamic overhead (checked casts) as price for simplicity/universality. * Independent from linear memory. * Pay as you go; in particular, no effect on code not using GC. * Don't introduce dependencies on GC for other features (e.g., using resources through tables). * Avoid generics or other complex type structure _if possible_. * Extend the design iteratively, ship a minimal set of functionality fast.

Я не специалист по gc, но слушал нескольких хороших специалистов (типа William D Clinger). Моё впечатление таково, что это вполне реалистичная идея, так как на практике между языками алгоритмы сборки одни и те же используются

Общие принципы - общие :) Но, грубо говоря, настройки разные - размеры и кол-во поколений, таймаут до перехода в следующее поколение, вот это всё.

Ну так настройки, наверное, можно свои для каждого процесса задавать

Общий подход к внедрению фич в вебе — сначала сделать минимально возможную, максимально опциональную реализацию концепции, чтобы иметь в дальнейшем возможности для манёвров

"Настройки" определяют реализацию

Ну нету идеального, подходящего всем GC. Не придумали ещё. Вон в JVM их вообще несколько.

Опять же, взять Erlang - там несколько одновременно работающих GC из-за локальности данных и это отлично работает, например, Stop the World не бывает - мирков много, все одновременно никогда не останавливаются

Ну нету идеального, подходящего всем GC. Не придумали ещё. Вон в JVM их вообще несколько.

Вот механизм, благодаря которому в jvm можно использовать различные gc, сейчас и проектируют

Общий подход к внедрению фич в вебе — сначала сделать минимально возможную, максимально опциональную реализацию концепции, чтобы иметь в дальнейшем возможности для манёвров

Все внедрённые на сей день вещи в вебе ущербны в разной степени - CSS, HTML, JS

У нас вообще несовершенный мир

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

Параллельно рассказывая примеры того, что разные gc в рамках одной платформы собственно не то чтобы что-то странное

Я могу понять пользу от "GC as a Library" для произвольных LLVM backends - можно быстро накидать рантайм и как-то жить

Но языки, уже имеющие свой GC, работающий хорошо для них, не должны пересаживаться на данный свыше

Хорошо, они могут не пересаживаться

Если смогут иметь свой и быть "non managed" с точки зрения wasm, то это будет нормальный вариант.

Искоробочный же GC поможет переехать языкам/экосистемам типа Elm/PureScript/ClojureScript

ну вообще принципы то тоже весьма отличаются из-за особенностей языка т.к. можно делать много доп предположений

типа однонаправленности ссылок для иммутабельных обьектов

и сразу переход у О(н) от большего

и наличия refenential transparency, которая позволяет при Гц дублировать объекты

ну и куча другого incremental/ non incremental,

stop the world или нет

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

и серебряной пули и близко нет

Что приводит к мысли, что GC - скорее вред, чем польза.

Не понимаю, с чего вы вообще взяли, что вам предлагается серебрянная пуля)

Pay as you go; in particular, no effect on code not using GC

Это не серебро, это лопата и кирка. Минимальная имплементация означает что все гипотезы выше предстоит реализовывать самостоятельно

Не суперсет всех gc проектируют, а сабсет

Лопатой и киркой оборотня не завалить, если что :)

Просто никто никуда не спешит) Пока что это даже не фундамент, а только его чертежи

Кому интересно, можете ознакомиться тут https://github.com/WebAssembly/gc/blob/master/proposals/gc/Overview.md

Всем привет!