AZ
fib :: Nat -> Nat, (->) это интуиционистская импликациямежду двумя объектами может быть много стрелок, ты же знаешь
Size: a a a
2019 December 25
AZ
без эквалайзера нельзя считать их равными
λ
то есть это утверждение из Nat следует Nat
AL
Иди нахер
Напоминаю про правила. Давайте спокойней
λ
между двумя объектами может быть много стрелок, ты же знаешь
так и разные по построению пруфы обычно не эквивалентны
λ
в том же коке пруф иррелеванс вводится как аксиома, которая может конфликтовать (позволить доказать False) с другими аксиомами
AZ
fib :: Nat -> Nat, (->) это интуиционистская импликациямне кажется у тебя сигнатура просто не отражает суть фиба
G
О, я срачик пропустил
λ
мне кажется у тебя сигнатура просто не отражает суть фиба
а как ты собираешься её отображать в сигнатуре?
AL
О, я срачик пропустил
не бойся, в нем ничего нового относительно точно таких же срачей пару десятилетий назад.
AZ
Должно быть что-то вроде
fib :: Nat A -> Nat Mult (typeof fib (A - 1)) AAZ
ну короче примерно как натуральные числа через Succ
λ
> Nat A B
ето што
ето што
G
Единственный плюс, ты знаешь что типы будут правильными. Но корректность работы программы тебе никто не обещает
Типы помогают в написании корректных программ, смореть type-driven development
AZ
> Nat A B
ето што
ето што
перепутал с умножением чутка
λ
Должно быть что-то вроде
fib :: Nat A -> Nat Mult (typeof fib (A - 1)) Aты просто выносишь реализацию на уровень типов, чем это отличается от того, чтобы сделать эталонную реализацию и потом доказывать, что остальные реализации эквивалентны эталонной?
p
Отсутствие нормальных типов, возможность внесения изменений в объекты на ходу (что означает, что isinstance начинает врать),
Вот навскидку набросал.
__приватные_имена__, YOBA-функции на пару десятков именованных параметров, абсолютно неинформативные сообщения об синтаксических ошибках, тайп-хинты которые НИЧЕГО БЛЯТЬ НЕ ДЕЛАЮТ, считается нормой возвращать значения разных типов при разных входных аргументах, мутабельность является свойством типа, а не значения, иммутабельность проверяется в рантайме, все почти пишут красивый код в угоду производительности, странное убеждение, что свободные функции, засирающие неймспейс читабельнее методов, абсолютно не масштабирующиеся list comprehension/generator expressions, однострочные блять лямбды, нет pattern matching-а или даже банального switch, встроенные списки гетерогенные, для нормальных массивов приходится юзать numpy, datatypes только в 3.7 завезли, None, None everywhere, иммутабельные строки, различие copy vs deepcopy, return обязателен даже в однострочниках, уёбищный тернарный оператор, изменение импорта всех элементов модуля на импорт только выделеных элементов меняет слово в начале, импорты могут кидать эксепшены, итераторы кидают эксепшены, отрицательные индексы.Вот навскидку набросал.
1. Ну это динамика, привет.
2. Плохой стиль кодинга считается.
3. И?
4. Ты не привык просто, и все.
5. Покажи пример такой ошибки.
6. Тайп-хинты только для ИДЕ.
7. Нет, это не норма.
8. И?
9. И? Этот язык интерпретируемый, конечно блять у него на рантайме все будет завязано.
10. Нахрена тебе в питоне производительность? Числа считать другие языки бери.
11. Дело вкуса.
12. Лист компетишионсы нужны для создания списков, когда это можно уместить в одну строку. Если больше чем func(a) for a in some.bar(), то юзай обычный цикл.
13. Ну и что что однострочные.
14. Так и матчить нечего, перечислений нет.
15. Хз что это.
16. Ну и что? Язык не для числодробилок, а массивы только там нужны.
17. В расте async/await только в 1.39 завезли, Раст не нужен.
18. Ты сейчас 90% языков перечислил.
19. Производительность это не про питон.
20. Алло, это различие во всех языках.
21. Не обязателен.
22. Не используй, если не нравится🤷🏿♂.
23. Не замечал проблем с этим.
24. И?
25. И?
26. Это удобно вообще.
2. Плохой стиль кодинга считается.
3. И?
4. Ты не привык просто, и все.
5. Покажи пример такой ошибки.
6. Тайп-хинты только для ИДЕ.
7. Нет, это не норма.
8. И?
9. И? Этот язык интерпретируемый, конечно блять у него на рантайме все будет завязано.
10. Нахрена тебе в питоне производительность? Числа считать другие языки бери.
11. Дело вкуса.
12. Лист компетишионсы нужны для создания списков, когда это можно уместить в одну строку. Если больше чем func(a) for a in some.bar(), то юзай обычный цикл.
13. Ну и что что однострочные.
14. Так и матчить нечего, перечислений нет.
15. Хз что это.
16. Ну и что? Язык не для числодробилок, а массивы только там нужны.
17. В расте async/await только в 1.39 завезли, Раст не нужен.
18. Ты сейчас 90% языков перечислил.
19. Производительность это не про питон.
20. Алло, это различие во всех языках.
21. Не обязателен.
22. Не используй, если не нравится🤷🏿♂.
23. Не замечал проблем с этим.
24. И?
25. И?
26. Это удобно вообще.
λ
посмотри курс по формальной верификации на коке от Антона Трунова, он там эти штуки объясняет
p
1. Ну это динамика, привет.
2. Плохой стиль кодинга считается.
3. И?
4. Ты не привык просто, и все.
5. Покажи пример такой ошибки.
6. Тайп-хинты только для ИДЕ.
7. Нет, это не норма.
8. И?
9. И? Этот язык интерпретируемый, конечно блять у него на рантайме все будет завязано.
10. Нахрена тебе в питоне производительность? Числа считать другие языки бери.
11. Дело вкуса.
12. Лист компетишионсы нужны для создания списков, когда это можно уместить в одну строку. Если больше чем func(a) for a in some.bar(), то юзай обычный цикл.
13. Ну и что что однострочные.
14. Так и матчить нечего, перечислений нет.
15. Хз что это.
16. Ну и что? Язык не для числодробилок, а массивы только там нужны.
17. В расте async/await только в 1.39 завезли, Раст не нужен.
18. Ты сейчас 90% языков перечислил.
19. Производительность это не про питон.
20. Алло, это различие во всех языках.
21. Не обязателен.
22. Не используй, если не нравится🤷🏿♂.
23. Не замечал проблем с этим.
24. И?
25. И?
26. Это удобно вообще.
2. Плохой стиль кодинга считается.
3. И?
4. Ты не привык просто, и все.
5. Покажи пример такой ошибки.
6. Тайп-хинты только для ИДЕ.
7. Нет, это не норма.
8. И?
9. И? Этот язык интерпретируемый, конечно блять у него на рантайме все будет завязано.
10. Нахрена тебе в питоне производительность? Числа считать другие языки бери.
11. Дело вкуса.
12. Лист компетишионсы нужны для создания списков, когда это можно уместить в одну строку. Если больше чем func(a) for a in some.bar(), то юзай обычный цикл.
13. Ну и что что однострочные.
14. Так и матчить нечего, перечислений нет.
15. Хз что это.
16. Ну и что? Язык не для числодробилок, а массивы только там нужны.
17. В расте async/await только в 1.39 завезли, Раст не нужен.
18. Ты сейчас 90% языков перечислил.
19. Производительность это не про питон.
20. Алло, это различие во всех языках.
21. Не обязателен.
22. Не используй, если не нравится🤷🏿♂.
23. Не замечал проблем с этим.
24. И?
25. И?
26. Это удобно вообще.
Ты просто перечислил особенности языка, но не объяснил почему это плохо
G
1. Я тебя может удивлю, но так во всех языках. Не запустив тесты, правильность работы программы не докажешь никак.
Автоматическая верификация программ с типами. Тесты, правда, всё равно придётся писать, но меньше разительно