В GHC добавлена поддержка WebAssembly

Ну так WebAssembly - это не то же самое, что JS. Оно всё равно напрямую с браузером взаимодействовать не может, и нуждается в JS-прокладке.

JavaScript FFI

So this will take some time and may not make it into GHC 9.6.1.

Без FFI ничего интересней факториала не напишешь. А если и напишешь, то вывести результат юзеру не сможешь.

Без FFI ничего интересней факториала не напишешь. А если и напишешь, то вывести результат юзеру не сможешь.

Конечно. Но бэкенд гораздо сложнее запилить, чем FFI, так что основная часть уже сделана.

Плюс, я вроде где-то читал, что у GHC будут более частые релизы, а не раз в год как раньше. Поэтому 9.8 считай тоже не за горами.

Плюс, я вроде где-то читал, что у GHC будут более частые релизы, а не раз в год как раньше. Поэтому 9.8 считай тоже не за горами.

Сомневаюсь, что более частые релизы означают, что на FFI будет потрачено меньше времени. Скорее, это означает, что FFI будет в 9.10 или каком-нибудь 10.X.

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

Один хрен, это всё будет довольно скоро уже.

А что вообще есть на WebAssembly? Я только фигму и гуглземлю могу вспомнить.

Один хрен, это всё будет довольно скоро уже

Ага, сразу после зав.типов.

Зависимые типы в хачкелле? Спасибо, но нет!

Хотя вот от лямбд в типах я бы не отказался.

Зависимые типы в хачкелле? Спасибо, но нет!

Эйзенберг ещё в 8.2 штоле обещал. Но чота не выходит каменный цветок.

Тоже интересует.

А что вообще есть на WebAssembly? Я только фигму и гуглземлю могу вспомнить.

А теперь ещё и факториалы с фибоначчи будут.

Ну он много чо обещал :)

Тут проблема в том, что как бы очередной C++ не получился, только ленивый и с тайпклассами. ИМХО ради зав.типов лучше сразу Агду взять, благо она умеет FFI с хачкеллем.

В плане приложений? Знаю что во внутренних сервисах сейчас нередко blazor используется. Даже звали пилить CRMку.

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

blazor

Под кору заведётся?

А давайте запилим виртуальную память на серваке, чтобы у клиента ресурсов вообще не было

Чо? Концептуально WebAssembly ничем не отличается от жаба-апплетов 20-летней давности.

Есть же Liquid Haskell. Его вроде достаточно.

Достаточно для чего? Это всё таки сильно разные вещи.

Кстати, для свежих версий GHC жидкохачкеля нет :(

Достаточно для чего? Это всё таки сильно разные вещи.

Для зависимых типов и их проверки.

Кстати, для свежих версий GHC жидкохачкеля нет :(

Вот это реально грустно.

Для зависимых типов и их проверки.

Эмм… Жидкохаскелл не реализует зависимые типы. Refinement types – это всё таки немного другая тема. В данном случае, к каждому типу приделывается предикат, которому значения этого типа должны удовлетворять.

В данном случае, к каждому типу приделывается предикат, которому значения этого типа должны удовлетворять.

Предикат результата может зависеть от предиката и типа аргументов, а это уже зависимые типы.

Эммм… нет. Зависимые типы зависят от значений. Иначе в хачкелле уже давно есть зависимые типы:

type family F a where
  F Int = Bool
  F Bool = Int
  F x = ()

Видишь? Тип F зависит от другого типа!

Зависимые типы зависят от значений.

Так в Liquid так и есть:

{-@ length :: xs:[a] -> {v: Int | v = (len xs)} @-}
length :: [a] -> Int
length []     = 0
length (x:xs) = 1 + length xs

{-@ map      :: (a -> b) -> xs:[a] -> {v:[b] | (len v) = (len xs)} @-}
map _ []     = []
map f (x:xs) = (f x) : (map f xs)

Ага. Но эта штука крайне ограничена. А теперь попробуй использовать в refinement type, например, какую-нибудь монадическую функцию.

К слову, эти два механизма не то чтобы противопоставлены и не исключают друг друга. Т.е. тебе никто не мешает их интегрировать, хотя бы в теории. Например, как тут: https://www.tweag.io/blog/2021-02-05-refinement-types/

Ага. Но эта штука крайне ограничена. А теперь попробуй использовать в refinement type, например, какую-нибудь монадическую функцию.

А внутри комментариев LH разве её не получиться описать?

Не, не получится. LH ограничен примитивными типами. Там особо не развернёшься. Я даже не уверен, что оно классы и type families умеет.

Я даже не уверен, что оно классы и type families умеет.

Так работает:

{-@ type Test1 = {v:Ord | v > 0} @-}

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

Говорю же, это совершенно разные вещи.

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

Так у класса типов значения не бывает. У любого значения в Haskell только один тип.

Хотя вот от лямбд в типах я бы не отказался.

так вроде в хаскеле можно функции над типами объявлять, или мне память изменяет?

ИМХО ради зав.типов лучше сразу Агду взять, благо она умеет FFI с хачкеллем.

Кок умеет экспорт в окамл.

так вроде в хаскеле можно функции над типами объявлять, или мне память изменяет?

Можно, но там лямбд нет. Надо отдельное имя для каждой задавать.

Так у класса типов значения не бывает.

Да, потому что это constraint. Но я не об этом. Я о том, чтобы вынести значение из типов образно в значения, как например knownNat это делает с числами.

У любого значения в Haskell только один тип.

В Haskell – да. Но если мы добавляем Refinement Types, то это уже далеко не так, и каждое значение может пренадлежать какому угодно количеству этих refined types.

Ну и да, я всё ещё утверждаю, что dependent types и refinement types – разные вещи, у которых только области применения слегка пересекаются.

Коры больше нет начиная с .NET 5. У нас коммерческий проект с мордой на blazor. Так что не только для внутренних пользователей.

Ну и да, я всё ещё утверждаю, что dependent types и refinement types – разные вещи, у которых только области применения слегка пересекаются.

пару лет назад обсуждали эту тему с monk и кажется в доках по refinement types прямо написано что это некоторое подмножество зависимых типов. Надо бы проверить, правда, поскольку за давностью лет могу путать.

Можно, но там лямбд нет. Надо отдельное имя для каждой задавать.

спасибо за уточнение. помню что вроде можно было , но подробности уже уплывают.

Вот есть точное определение: https://cs.stackexchange.com/questions/21728/dependent-types-vs-refinement-types/126730#126730

Thus, refinement types are similar to dependent pair types whose second type are restricted to being a decidable predicate.

В общем, жидкие типы являются подмножеством зависимых.

спасибо за ссылку!