Телеграмм чат группы haskellru страница 16281

19:38пожаловаться #1

Ad in Haskell

This style of humor honours you

19:39пожаловаться #2

[

I cant brag "hey, you, i know JavaScript" because anybody know JavaScript and many people hate js-developers.
But if i say "hey, i'm a haskell developer", they asked me "what is haskell? is it something cool and challenging?".
Yes, it is :)

19:43пожаловаться #3

sometimes people do recognize it though. So I have to resort to telling them that I also code in Agda. That always works

21:25пожаловаться #4

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

21:27пожаловаться #5

Nick Ivanych in Haskell

Тьюринг-полнота добавляется в любой язык тривиально, зачем "весь свой язык" переделывать?

21:28пожаловаться #6

adam in Haskell

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

21:28пожаловаться #7

[

тотальные языки не полные по тьюрингу

21:29пожаловаться #8

[

т.е. надо убрать тотальность

21:29пожаловаться #9

[

ха-ха

21:29пожаловаться #10

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

21:29пожаловаться #11

ну это ортогональный вопрос

21:31пожаловаться #12

кана in Haskell

как в идрисе - структурная рекурсия

никаких доказательств, просто твоя рекурсия чуть ни синтаксически ограничена

21:34пожаловаться #13

[

это таки байт поставить нормально идрис?

21:35пожаловаться #14

Maxim Koltsov in Haskell

В пропозале сказано что пофиг на тотальность

21:35пожаловаться #15

Maxim Koltsov in Haskell

Потому что хаскель это не чтобы теоремы доказывать

21:35пожаловаться #16

[

да ладно, какой-нибудь мод #total был бы прикольным

21:36пожаловаться #17

Alexander Luzgarev in Haskell

Это потому что кроме функций в язык ничего не завезли

21:36пожаловаться #18

Ilya Kos in Haskell

Ты просто хейтер

21:38пожаловаться #19

кана in Haskell

да он бы еще был бы невозможен в куче случаев

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