У тебя же типы только в компасов тайм живут - на работу программы эти аннотации не влияют по сути

ещё раз тезисно, что я пытаюсь сказать

- мы говорим о статической типизации (проверке программы на этапе компиляции), но при этом gradual, то есть не по всей кодовой базе.

- под gradual typing я понимаю такое, когда программист расставляет аннотации, где ему нужно, и не делает этого там, где ему не нужно.

- у меня возникает вопрос о возможности такого алгоритма компилятора, который будет делать проверки на основе предоставленных аннотаций, не требуя от программиста расставить аннотации там, где это требуется для анализа типов.

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

Я использую clj-kondo. Хотя он и линтер, но считывает расставленные программистом типы и анализирует вызовы.

это type inference, это другое
и в данном случае это работает только с константами, тип которых очевиден при компиляции

то есть вот более практичный пример, и это уже не работает

(defn sum2 [^Long a ^Long b]
  (println a b))

(defn sum3 [a b]
  (sum2 a b))

(sum3 "3" 4)

Либо я ничего не понял, либо такого алгоритма нет.
То есть компилятор делает проверки только там где стоят аннотации, где их нет - проверки не происходят.
Есть алгоритмы автоматического вывода типов на основе использования, но это доступно только в статически-типизированных языках)

(defn sum2 [^Long a ^Long b]
  (println a b))

(defn sum3 [a b]
  (sum2 a b))

(sum3 "3" 4)

Это будет работать в clojure typed или как там его

(defn sum2 [^Long a ^Long b]
  (println a b))

(defn sum3 [a b]
  (sum2 a b))

(sum3 "3" 4)

хотя полноценный type inference тут мог бы сработать

да так не работает. но если в sum3 перед a указать или ^Long или ^String то ошибка снова будет поймана линтером в обоих случаях.

Dart?

Где надо тип - ставите тип, где не надо тип - ставите dynamic, в месте использования можете о значении предполагать что хотите, конпелятор схавает

Сееекунду. core.typed же библиотека для того же самого динамически типизированного Clojure, нет?

я тоже полагаю, что такого алгоритма нет

«То есть компилятор делает проверки только там где стоят аннотации, где их нет - проверки не происходят.»

а я говорю о том, что компилятор, чтобы сделать проверки, где стоят аннотации, попросит программиста дать больше аннотаций.

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

потому она и «не зашла» — начинаешь расставлять аннотации в одном месте, заканчиваешь расстановкой аннотаций по всему коду, включая аннотации для функций из сторонних библиотек

Ну я данном конкретном случае я бы не назвал это удовлетворением компилятора, это просто явное указание, что в данном месте проверка типов не срабатывает, но программист знает, что делает

А, ну да, в этом и суть)
То есть если у вас есть функция которая принимает стринг, то вы должны явно в вызывающем коде сказать «вот этот аргумент это стринг»

В нормальной программе unsafe cast логично ожидать только там, где данные снаружи приезжают

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