Как-то очень медленно. В JS-react чате ~3k людей, а в Elm < 100

Нас спасает технофашистские методы работы

Привет. Какой плагин ставить на VS Code для Хаскеля, может кто посоветовать?

haskerro > haskelly

'>' переход или сравнение?

а жс-еры въедут в elm ?

Почему нет? Въезжают и радуются. Столько костей же сломали без статической проверки типов. Тайпскрипт –– не панацея. А элм всё скажет, всё расскажет, место в коде покажет. Надо лишь попробовать.

'>' переход или сравнение?

сравнение

Как-то очень медленно. В JS-react чате ~3k людей, а в Elm < 100

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

Почему нет? Въезжают и радуются. Столько костей же сломали без статической проверки типов. Тайпскрипт –– не панацея. А элм всё скажет, всё расскажет, место в коде покажет. Надо лишь попробовать.

кстати, да. ограниченность статической системы типов даёт больше возможностей для диагностики ошибок. это как в го, только в го нужно interface {} делать, что совсем больно

Даёт больше возможностей допустить ошибки по причине невозможности достаточно хорошо закодировать домен, вы хотите сказать?

Иначе Брейнфак всё бы зарулил - там один тип только и есть, вот уж где точно "легко диагностировать ошибки" :)

malbolge

Не, malbolge, это уже спецолимпиада. Типа Perl6

Ну вообще про весь этот элм уже давно сказано: Formal methods will never have a significant impact until they can be used by people that don’t understand them. Ну, вот мы и пришли, собственно.

Элм выучить проще жс-а в разы с нуля.

Даёт больше возможностей допустить ошибки по причине невозможности достаточно хорошо закодировать домен, вы хотите сказать?

ну в хаскеле обычно получаешь ошибку что нет инстанса там то там то. хотя в большинстве случаев поможет не определение инстанса а подстановка нужно аргумента (легко запутаться когда применение через пробел записывается)

Даёт больше возможностей допустить ошибки по причине невозможности достаточно хорошо закодировать домен, вы хотите сказать?

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

haskerro > haskelly

Haskerro работает хорошо, спасибо

Haskerro работает хорошо, спасибо

пишет тип для сущности?

пишет тип для сущности?

При наведении курсора - да :)

кстати, для этого нет хоткея как в идее?

При наведении курсора - да :)

Значит ок. Просто у меня не сразу всё встало.

А как же рефлекс для фронта?)

Слушайте, а тип Void -> a населен?

Боттомом как минимум :)

я знаю про absurd, но я не очень понимаю, как может существовать функция, которая ничего не принимает

ну, если бы не было bottom

absurd :: Void -> a она не ничего не принимает, а принимает ничего

absurd a = let x = absurd a in x

только она вернёт боттом

ну это не удивительно

нужно может быть если есть, например какая-нить бесконечная функция, типа forever blabla её логично сделать тип m Void, но если вдруг по каким-то причинам надо её композить с другой, например всякими примитивами из async то там иногда нужно вызывать absurd

Слушайте, а тип Void -> a населен?

Конечно, потому что это id :)

Void можно рассматривать как forall a. a

эм...

newtype Void = Void { absurd :: forall a. a } data Void написать изоморфизм - упражнение читателю

это то понятно, вот "потому что это id" как-то неочевидно, что так

это id up to isomorphism

То есть для одного из возможных определений Void это просто unwrapping ньютайп-конструктора

Конечно, потому что это id :)

хм, разве?

не существует же функции Void -> Void

как и любой другой a -> Void

id

Void -> Void это точно id без оговорок даже

Количество функций считается как степень

0^0 = 1

как и любое x^0 = 1

поэтому функций Void -> a всегда 1 для любого a, и это absurd

а в случае Void -> Void просто absurd = id

как и любой другой a -> Void

const bottom?

Не про хаскель я говорю, нету undefined никакого

Да, речь-то не про Haskell

иначе везде +1 надо делать в алгебре, чтобы боттом учитывать

Не про хаскель я говорю, нету undefined никакого

понял, т.е. у тебя Void это пустой тип?

даже без боттома

Точнее, речь про идеализированный Haskell без боттомов (как и в любых рассуждениях такого уровня)

Void и задуман как пустой тип

@ind_index тогда поясни ещё раз, пожалуйста, почему функций Void -> Void одна штука

аргумент со степенью мне кажется формальным

точнее, лучше так вопрос поставлю

в противоречие с какими аксиомами я войду, если скажу, что функций с типом "пустой тип -> пустой тип" ноль штук, а не одна штука?

а, хм, я понял, почему

давай

я в одном своем посте представлял функцию как таблицу результатов. То есть имя тип data ABC = A | B | Cи функию isA : ABC -> Bool isA A = True isA _ = Falseможно составить таблицу (кортеж Bool ^ n, где n = |ABC|) -- A B C (True, False, False) То есть каждому i-ому значению типа ABC соответствует i-ый элемент этого кортежа. Для типа 0 -> 0 это пустой кортеж (), ведь каждому значению Void соответствует некоторое значение Void.

это () это и есть единичный тип

в противоречие с какими аксиомами я войду, если скажу, что функций с типом "пустой тип -> пустой тип" ноль штук, а не одна штука?

Это ты своим утверждением аксиому ввел

А я могу доказать ее противоречивость предоставив функцию id

я имею id :: forall a. a -> a, что мне мешает взять a = Void?

Я объясню вам сейчас интуитивно, что такое Void

функция действительно для каждого элемента Void отдает элемент Void

функция a -> Void написана быть не может, потому что она должна вернуть результат, которого не может быть (по определению Void) а если уж вам удалось в текущем контексте получить Void, то это значит, что текущий кусок кода в рантайме не выполнится никогда!

потому что нет ни одного способа ему этот Void предоставить

а оттого функция Void -> a как бы говорит "вызови меня если сможешь, я тебе дам взамен что угодно, любое a"

Да только вызвать ты ее не сможешь, а потому функция может ничего и не делать

любую функцию можно определить переобором конструкторов, например, если на вход (), то f () = ... если на вход Bool, то f True = ... f False = ... если на вход Maybe a, то f Nothing = ... f (Just a) = ... а если на вход Void, то f

что записывается как f = \case{} в Haskell и как f () вместо f = ... в Agda

Например, если я имею Either Void (), то я могу сконструировать только Right (), но никогда никакого Left ... не будет в жизни, не сконструирую никак

а потом функция, которая хочет принять Either Void (), может писать f (Left e) = absurd e

и в рантайме этого codepath и не будет никогда

потому что это абсурд, будто кто-то нам Void передал

Я не очень понимаю про что вы говорите, вы про какой-то фиксированный type theory, про инлайн логику топоса или про тьюринг-полные языки?

Про любой total functional language с inductive type definitions