AZ
Чтобы нормально писать на шарпе нужно прочитать 22 книжки про ООП, свойства, интерфейсы и это все
я за всю жизнь меньше 5 книжек по шарпу прочитал, брат жив
Size: a a a
2019 December 25
AZ
Вообще все претензии Жуковского это то же бабушкино "раньше было лучше", только "в других языках было лучше".
нет, моя претензия - что люди гонятся за копейкой, тонну золота теряют
Ct
на идрисе это ошибка компиляции
И как же там компилятор понимает, что + и multiply - это немного нелогично?
AZ
И как же там компилятор понимает, что + и multiply - это немного нелогично?
нет, ты в доказательстве пишешь
multiply _ 0 = 0
multiply 0 _ = 0
multiply x y = (multiply x y - 1) + xAZ
и компиль проверит что это выполняется
ШН
нет, ты в доказательстве пишешь
multiply _ 0 = 0
multiply 0 _ = 0
multiply x y = (multiply x y - 1) + xнифига не понял, но очень интересно
Ct
и компиль проверит что это выполняется
Хм, интересно. Как он это проверяет?
AZ
Хм, интересно. Как он это проверяет?
завтипами. Вот тут пример. Правда дальше челик упоролся специально, но суть та же https://habr.com/ru/post/463957/
ШН
завтипами. Вот тут пример. Правда дальше челик упоролся специально, но суть та же https://habr.com/ru/post/463957/
м
> челик
AZ
> челик
М?
AZ
revCorrect : (xs : List a) ->
(f : b -> a -> b) ->
(init : b) ->
foldl f init (revDumb xs) = foldr (flip f) init xs
revCorrect [] f init = Refl
revCorrect (x :: xs) f init = let rec = revCorrect xs f init in
rewrite sym rec in foldlRhs f init x (revDumb xs)AZ
В итоге 5 строчек и надёжнее любых тестов
AZ
Хотя конечно любителей проверять rev 1 2 3 = 3 2 1 это не убедит
E
программист - это же, по сути, переводчик с человеческого языка на язык программирования, правильно?
С
программист - это же, по сути, переводчик с человеческого языка на язык программирования, правильно?
Иногда он переводит с человеческого мычания.
E
Иногда он переводит с человеческого мычания.
заказчика?
76
программист - это же, по сути, переводчик с человеческого языка на язык программирования, правильно?
Ну так то да, а вот инженер это кто более глубоко копает... Холивар уровня мема про датасайнс
E
Ну так то да, а вот инженер это кто более глубоко копает... Холивар уровня мема про датасайнс
понятно
76
понятно
Хотя тут все тоже не однозначно. После универа я настраивал СКУД и СВН