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

Чуть не подавился кофе. Мы с вами может не согласны, но разве это повод меня убивать?

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

Да-да, а для «серьезных» программ на плюсах - лишь бы компилировалось. Так и пишет большинство, а потом начинается мучительное разгребание багов, которые в динамике куда как проще фиксить. Я уж молчу про жаба-ынтерпрайз - кто там пишет и как.

То есть значит такие программы все-таки есть и вы этому не противоречите? Тогда какими фактами ваше утверждение вообще можно опровергнуть? Потому что оно теперь выглядит нефальсифицируемым, а значит и совершенно безсодержательным. С тем же успехом вы могли рассказывать о розовых слониках с Альдебарана.

Почему меньше? Разве в статике не пишутся тесты на логику? В динамике пишутся те же самые тесты. Откуда берутся лишние?

тесты на логику разве будут проверять соответствие типов? Повторяю, если по логике нужно целое число 0, то можно скормить твоему коду практически любую строчку, с вероятностью 99.9% она сконвертится в 0. В тестах. А в продакшене - не сконвертится. Рано или поздно. Впрочем, если этот код поддерживать кому-то другому...

Я должен пойти в бюро статистики? Даже если не пойду это не отменит факта что всякие пхп для быдловизиток. Лисп мы же не считаем, его как кот наплакал.

Зачем? Я запущу ф-ю один единственный раз и если она возвращает строку вместо целого, то это будет видно.

как ты УВИДИШЬ, что функция вернула 0, а не «0». А может вернуть «» - это тоже с виду 0...

тесты на логику разве будут проверять соответствие типов?

Вы упорно не понимаете, о чем я говорю. Соответствие типов вообще проверять не надо. Потому что оно и так упадет чуть менее чем всегда на логических. Исключения составляют те случаи, когда мы в динамике возвращаем какой-нибудь аналог размеченного объединения, например, но в случае динамики это уже вопрос логики приложения - точно так же, как он был бы вопросом логики и в статике при замене размеченных объединений на простые. Просто потому что простые объединения намного более гибкая и выразительная штука.

Повторяю, если по логике нужно целое число 0, то можно скормить твоему коду практически любую строчку, с вероятностью 99.9% она сконвертится в 0.

Слабая типизация - говно, об этом никто не спорит. Речь идет о strong dynamic, очевидно.

как ты УВИДИШЬ, что функция вернула 0, а не «0». А может вернуть «» - это тоже с виду 0...

Я выше уже сказал, но повторю - речь о сильной типизации. С тем, что в случае слабой динамики (равно как и в какой-нибудь слабой статике типа сишки) вам летающими вокруг дилдами жопу распидорасит до уровня кварко-глююнной плазмы никто не спорит.

Я должен пойти в бюро статистики? Даже если не пойду это не отменит факта что всякие пхп для быдловизиток.

А эрланг для чего, например? или javascript+node.js?

Первое соглашусь - серьезная разработка. Второе - поделие для JS дрочеров читающих хабр по утрам

Первое соглашусь - серьезная разработка.

То есть как минимум в некоторых случаях на динамических ЯП пишут серьезные приложения и никаких колючих кактусов?

Серьезная разработка. Но синтаксический кактус ого-го. Ну я не виноват что самую старую систему actors сделали динамической.

Я должен пойти в бюро статистики? Даже если не пойду это не отменит факта что всякие пхп для быдловизиток.

Согласен, но это вовсе не потому что на пхп сложнее вылавливать ошибки типов. У динамики главный (и пожалуй единственный) недостаток - тормознутость. Там, где это не важно, никто в здравом уме статику не предпочтет. Разве что требуется сверхнадёжность и нужно связать быдлокодера по рукам и ногам.

Лисп мы же не считаем, его как кот наплакал.

Тогда и Erlang тоже выкини, чего уж там.

Ну я не виноват что самую старую систему actors сделали динамической.

Да уж, Маккарти, Кэй и Армстронг по всему видно что лохи. Наплодили быдлоязычков для визиток панимаш.

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

Это самое главное в программировании для энтерпрайза. И я нахожу в этом больше плюсов, чем минусов. Но я не люблю энтерпрайз.

А каким образом можно написать код с не 100% покрытием?

В этой вселенно только так и пишут.

То есть это выходит надо написать ф-ю и ниразу ее не запустить?

Нет, выходит не так.

или как?

Так, что в некоторых функциях есть ветвления, и для их проверки просто запустить функцию недостаточно.

В этой вселенно только так и пишут.

Мы, видимо, о разных вариантах покрытия говорим. Я говорил о statement coverage, и если у вас есть по несколько тестов на ф-ю, то он на большинстве ф-й и так будет.

Так, что в некоторых функциях есть ветвления, и для их проверки просто запустить функцию недостаточно.

Конечно. И сколько у вас вложенных ветвлений бывает в среднестатистической ф-и?

если у вас есть по несколько тестов на ф-ю, то он на большинстве ф-й и так будет.

На большинстве - может быть (51% - это тоже большинство). А вот компилятор статического языка проверит 100% кода, всегда. Ну а если реально нужен динамизм - top type или opDispatch.

И сколько у вас вложенных ветвлений бывает в среднестатистической ф-и?

Если в функции есть хоть одно ветвление, просто вызова недостаточно для ее проверки. Нужно подбирать входные данные.

В том, что чек зависимых типов алгоритмически неразрешим

Это зависит. Интенсиональная Теория Типов (как и HoTT) имеет разрешимый алгоритм проверки типов, эктенсиональная теория ─ нет. Agda и Coq именно интенсиональны (если не считать postulate и axiom, соответственно, также как и некоторых эктенсиональных расширений Coq). В Epigram все значения разрешимы, поэтому проверка типов разрешима. Agda и Coq, к тому же, строго-нормализированны, так что проверка типов в любом случае разрешима (хотя в Agda есть in-module баги). В строго-нормализованном (не Тьюринг-полном) языке event loop / concurrency нужно явно выделять во внешнюю по отношению к функциональному ядру сущность (что уже можно делать в Agda с помощью postulate). С точки зрения практического применения всё это на данным момент, конечно, такая же фантастика как и динамически типизированный язык с кучей хороших внешних статических верификаторов.

т.к. эквивалентен мат. доказательству

Конструктивному доказательству же.

То есть никак несовместимо.

Через toTop касты и typecase, не в вижу в этом ничего страшного, по крайней мере, так каст из Top в статику будет безопасен ─ можно покрыть некое количество подтипов Top и поставить вменяемую заглушку на всё остальное. Вполне тотально получается.

Чистая динамика же сугубо частична по своей природе. (+), который вроде как Top ... -> Top, на самом деле не работает для всех подтипов Top и бросает исключения, то есть не является математической функций. Так что нужно либо делать тотальный (+) : Number ... -> Number и (typecase (a b c) ((Number a b c) (just (+ a b c))) (else nothing)), либо делать lift_0 : {A <: Top} -> A -> Top, lift_n : {A_0 ... A_n <: Top} -> (A_0 ... -> A_n) -> (Top ... -> Maybe Top) и, предполагая автоматическую расстановку lift_*, ─ (+ 1 2 3) => just 6, (+ 1 2 «3») => nothing. Аналогично для unlift_*. Такие lift_* и unlift_* можно выразить через typecase и toTop касты.

Вполне наблюдается.

В динамическом языке уже можно сделать compile-time проверку доступа по индексу в массиве или доказать теорему Евклида в зависимых типах? :)

Так же, как написан внутренний тайпчекер SBCL?

Он всяко не внешний (и даже никак не локализован в сырцах) и к тому же «не работает»™.

А почему без? И почему нельзя использовать уже существующий?

Ну codewalker / чекер CL явно пишется не «легко и просто». Существующий (если это про SBCL) не работает, ещё раз. См. ниже про slot-value.

Непонял, что? Какие типизированные ф-и? Откуда они взялись и зачем их делать макросами?

Например, как сделать безопасный slot-value/typed в CL? Видимо, написать как макрос вместо с макросом let/typed с общением через контекст (defparameter *type-context* (make-hash-table :test #'eq)), только отсутствие контроля за макросами не позволит добиться желаемого. Есть какие-то другие варианты? В Racket, видимо, это можно cделать, так как hash-table связывающая типы с лексическими значениями уже встроена и работает.

изначально динамический рантайм во0первых будет на динамике шустрее

Как python, например :)

Во-первых, мы не сможем использовать в нетипизированном ЯП ф-и, написанные в типизированном

Сможем, с помощью lift или unsafeLift (динамическая функция по определению unsafe).

многие типизированные конструкции при стирании типов тупо потеряют смысл, то есть семантика ЯП кардинально изменится.

Какие? (+) перестанет числа складывать? Или речь про сильно полиморфные функции и контейнеры?

Если в функции есть хоть одно ветвление, просто вызова недостаточно для ее проверки. Нужно подбирать входные данные.

Да никто с этим и не спорил. На практике, однако, ф-и вызываются далеко не однажды и отсутствие 100% покрытия в этом смысле - это большая редкость, которая может возникать только в очень специфических случаях. В таких случаях нет проблем добавить отдельно тестов для покрытия - тем более нам эти тесты все равно будут нужны для проверки логики работы.

Соответствие типов вообще проверять не надо. Потому что оно и так упадет чуть менее чем всегда на логических.

Несоответствие типов в системе на динамически-типизированном языке может всплывать через годы (!) после написания проблемного кода. Просто потому что соответствующее сочетание данных вероятностно редко. Это может быть и не важно, но как только такой баг находится он становится уязвимостью, до тех пор пока не будет исправлен, что может быть совсем не легко - пытаться что-то локализовать в сложном, мутабельном, связном и динамическом control flow - то ещё занятие.

Это зависит.

Ну да, если нас система типов заставляет написать доказательство, то тут никаких проблем нет, т.к. проверка доказательства разрешима. Это сути не меняет, однако.

С точки зрения практического применения всё это на данным момент, конечно, такая же фантастика как и динамически типизированный язык с кучей хороших внешних статических верификаторов.

Ну тут вещи принципиально разные - в случае там агды или coq все плохо и хорошо быть не может, т.к. как ни крути а программисту все равно придется бодаться с чекером руками. Дя внешних же чекеровл никакой проблемы в области теории нет. Ее и в области практики-то нет - то есть чекер для питона не сложнее чекера для хаскеля написать. Другой вопрос в том, что оно никому не надо.

Конструктивному доказательству же.

Да любому. Вам никто не мешает для любой теории подобрать свой ЯП, чек в которой будет эквивалентен доказательству утверждений в этой теории.

Через toTop касты и typecase, не в вижу в этом ничего страшного, по крайней мере, так каст из Top в статику будет безопасен ─ можно покрыть некое количество подтипов Top и поставить вменяемую заглушку на всё остальное. Вполне тотально получается.

Нафиг вообще нужен такой каст? Я если честно не понял чем эта конструкция выразительнее подтипирования с объединениями. Статически типизированного, безо всяких кастов.

Ну codewalker / чекер CL явно пишется не «легко и просто».

Ну чекер это вообще всегда не так уж «легко и просто», если конечно не имеется в виду нечто тривиального вроде чекера для чистой System F и других элементарных вещей.

Например, как сделать безопасный slot-value/typed в CL?

не понял, а зачем его делать безопасным? Чекер не должен делать ничего безопасного. Он просто берет ваш готовый код и выставляет эррор, когда может доказать ошибку и ворнинг, когда не может доказать корректность. При чем никаких типов вы в код не добавляете, никак код не меняете, и никаких там let-typed у вас нету, очевидно.

только отсутствие контроля за макросами не позволит добиться желаемого.

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

В Racket, видимо, это можно cделать, так как hash-table связывающая типы с лексическими значениями уже встроена и работает.

Это вы про что?

Как python, например :)

Во-первых, следует сравнивать компиляторы с компиляторами. Во-вторых - я так думаю и питон окажется шустрее какого-нибудь шарпа, в котором все будет завернуто в dynamic, или что там у нас в шарпе.

Сможем, с помощью lift или unsafeLift (динамическая функция по определению unsafe).

Так дело не в ф-ях а в значениях. У вас динамические ф-и боксят в dynamic, а статические - нет, по-этому вызывать статическую из динамической никак нельзя - это небезопасно. И наоборот тоже.

Какие? (+) перестанет числа складывать? Или речь про сильно полиморфные функции и контейнеры?

Например да. high-kind после стирания типов не работает никак. ad-hoc полиморфизм тоже не работает никак. Конечно, можно эмулировать имплицитами, как в скале - то есть дефакто ф-я принимает некий дополнительный параметр, если пишем статический код, то компилятор может подставлять имплицит и сам, а в динамическом делаем это явно. Это даже лучше в некотором смысле, т.к. полиморфные ф-и искаробки становятся конкретной сущностью, применение полиморфного аргумента превращается в частичное применение и т.п., но это был только общий пример «обессмысливания» программы при убирании типов - вообще же статические языки в семантике очень сильно завязаны на типы и в каждом конкретном можно кучу подобных вещей найти.

пытаться что-то локализовать в сложном, мутабельном, связном и динамическом control flow - то ещё занятие.

Ну так оно то еще занятие хоть с динамической системой типов, хоть со статической

И решение тут одно - избегать сложности, связности, мутабельного состояния... :)

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

Логические ошибки тоже. Вопрос лишь в том, каково соотношение в количестве этих ошибок.

Вот это нафлудили, отписываюсь от треда.

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

Ну да, если нас система типов заставляет написать доказательство, то тут никаких проблем нет, т.к. проверка доказательства разрешима.

Сигнатуры функций - утверждения, реализации функций - доказательства. Будет ли разрешим тайпчек или нет зависит от набора аксиом языка (и от того, не добавил ли пользователь «плохих» аксиом).

Это сути не меняет, однако.

Но типы в интенсиональной теории, получается, «правильные»?

Да любому.

Речь шла про зависимые типы, то есть про то что называется Теорией Типов (прописными буквами).

Нафиг вообще нужен такой каст?

Велосипед не мой - так почти любой dynamic устроен, через каст в него и разбор обратно по типам в typecase-like выражении.

не понял, а зачем его делать безопасным?

Чтобы не писать (slot-value obj 'bad-slot):

(defmacro slot-value/typed (object slot-name)
  (let ((type (when (symbolp object) (get-type object))))
    (when (and type
               (find-class type :errorp nil)
               (symbolp slot-name)
               (not (find-slot-in-class type slot-name)))
      (error "unbound slot: ~S" slot-name))
    `(slot-value ,object ,slot-name)))

во-первых, это должно быть функцией, во-вторых, get-type не работает, потому что динамика. Его можно писать как gethash из таблицы которую делает let/typed (мы делаем (let ((var val type) ...) ...)), но как следить за порядком раскрытия макросов?

Это вы про что?

А как там пример выше можно сделать? Или нельзя?

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

Prelude> default ( Int )
Prelude> :m + Data.Dynamic
Prelude Data.Dynamic> toDyn (+)
<<Int -> Int -> Int>>
Prelude Data.Dynamic> dynApply (toDyn (+)) (toDyn 1)
Just <<Int -> Int>>
Prelude Data.Dynamic> dynApply (toDyn (+)) (toDyn 1) >>= flip dynApply (toDyn 2)
Just <<Int>>
Prelude Data.Dynamic> dynApply (toDyn (+)) (toDyn 1) >>= flip dynApply (toDyn 2) >>= fromDynamic :: Maybe Int
Just 3

;)

Например да.

По ссылке есть вторая статья как раз про полиморфизм + dynamic, но я её не смотрел.

Ну так оно то еще занятие хоть с динамической системой типов, хоть со статической

Но суть в том, что это ошибка вида 1 + null. Которую трудно искать (уже по другим причинам, да). Поэтому лучше вообще не искать, то есть из

соотношение в количестве этих ошибок.

убрать все ошибки вида «тип A != тип B» (в т.ч. для параметрически полиморфных типов), «f : A -> ... реализована не для всех элементов типа A» и т.п. (насколько хватает желания «бодаться с тайпчекером»).

Есть in-browser фреймворки для тестинга(тестраннер - html страница), есть phantomjs.

Если есть посерьезнее, то зачем при этом терпеть ошибки попроще

Я на Хаскелле не писал, но даже такая система типизации, как в крестах, сильно тормозит процесс разработки. Мне в плюсах постоянно мешало то, что компилятор ругался на вещи, которыми я собирался заняться в третью очередь. Возможно, будь в плюсах понятие образа с полноценным встроенным REPL'ом, чтобы bottom-up по-человечески делать можно было, то было бы веселее.

Ну и в любом случае, даже программе на статически типизированном языке приходится сталкиваться с IO, которому по его природе нельзя доверять.

Но типы в интенсиональной теории, получается, «правильные»?

«Правильные» - сделанные удобно.

Велосипед не мой - так почти любой dynamic устроен, через каст в него и разбор обратно по типам в typecase-like выражении.

Но зачем оно надо и чем оно лучше полностью статического сабтайпинга с объединениями?

Чтобы не писать (slot-value obj 'bad-slot):

Да не должно быть у вас никакого slot-value/typed.

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

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

В-третьих, хинты если и есть, то они вообще никакии не должны влиять на семантику ЯП (внешний чекер же), так что непонятно нафига их делать какими-то макросами? Это вообще должна быть отдельная софтина, возможно никак не связанная с лиспо-рантаймом, которая занимается исключительно тем, что берет текст программы и анализирует его.

В-четвертых - CL это вообще очень говенный пример, т.к. его на мой взгляд даже и компилировать-то нельзя. А то, что называют «компиляцией» - это в нашем случае ложь, пиздеж и провокация, т.к. скомпилированный код должен сохранять семантику интерпретации, чего для общелиспа как раз и не выполняется, при чем ОЧЕНЬ СИЛЬНО не выполняется.

По ссылке есть вторая статья как раз про полиморфизм + dynamic, но я её не смотрел.

Ну с перворанговым и первопорядковым параметрическим полиморфизмом все нормально. А вот все остальное - только имплицитами (или аналог какой-то).

А как там пример выше можно сделать? Или нельзя?

Нет, такого хеша там нет (ведь типов нет). Но можно сделать, конечно. Однако, вместо глобальных хешей я предпочитаю использовать имеющиеся средства макросистемы, то есть как-то так:

http://pastebin.com/KkvhkFW1

и использоваться оно будет так:

http://pastebin.com/4j9LciaS

все ошибки в примере вылетали во время экспанда, конечно же.

Но суть в том, что это ошибка вида 1 + null. Которую трудно искать

Ну если сложно, да связно, да с мутабельным состоянием - трудно, да. А если нет - то не трудно.

(насколько хватает желания «бодаться с тайпчекером»)

Так с ним все время приходится в статике. Вне зависимости от желания.

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

ИМХО надёжность нужна ВСЕГДА, если речь идёт о приложении большем 1000 строчек. В ЯП со статической типизацией приложения в 1000+ строчек писать можно, в динамике... Я не осилил... Проблема в том, что неправильное предположение интерпретатора о типе может вылезти в ЛЮБОМ месте кода и в ЛЮБОЕ время. При строгой типизации вроде C++, ошибка с типом тоже возможна, но она будет локализована теми местами, где мы эти типы меняем (а это надо на самом деле редко в рантайме)

Это самое главное в программировании для энтерпрайза. И я нахожу в этом больше плюсов, чем минусов. Но я не люблю энтерпрайз.

я тоже люблю just for fun. Только за удовольствия не платят, а как раз наоборот...

Как людям удается создавать приложения такой сложности на JS?

Люди читают документацию, например.

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

это на самом деле хорошо, ибо практика показывает, что эти «третьестепенные» вещи успешно работают в продакшене. Вот только тестируют их таки тоже на отъэбись.

Люди читают документацию, например.

выше уже сказано, что JS надо по назначению применять, для валидации данных вебформочек. Ещё юзер может пароли генерить, прямо своим браузером, локально. Ну много чего... На 1..20 строчек.

.. JS .. по назначению .. валидации данных вебформочек .. пароли генерить .. На 1..20 строчек.

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

да, верно, так оно всё и начиналось.

да, верно, так оно всё и начиналось.

надо уметь вовремя останавливаться.

А на лоре кроме толстых школьников все спят

Зотроллел так зотроллел

Речь сейчас именно о сложных скриптах, а не простых интерфейсиках с jQuery UI.

В треде уже упоминали ClojureScript? Как раз заточен для RIA.

ИМХО надёжность нужна ВСЕГДА

Опять статикосказки начинаются. Язычки типа жабы или шарпа или даже хаскеля никакой особой надежности не дают, т.к. способны отловить только чрезвычайно узкий класс наименее значимых ошибок. Вот какая-нибудь агда тебе даст надежность, да. И то, как часто приложения пишут на агде, какбе нам очень ясно демонстрирует, насколько надежность нужна в реальности, а не в чьих-то мокрых мечтах.

При строгой типизации вроде C++

В с++ типизация слабая. То есть никаких профитов по сравнению с динамикой она не дает в принципе.

На практике, однако, ф-и вызываются далеко не однажды и отсутствие 100% покрытия в этом смысле - это большая редкость

В статьях по статической типизации динамических языков постоянно упоминаются найденные ошибки несоотвествия типов - и это в отлаженных, релизных программах. Отсуствие 100% покрытия - это вещь совершенно обычная.

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

А то, насколько часто приложения пишут на Яве/Шарпе, демонстрирует... ну ты понел.

«Правильные» - сделанные удобно.

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

Но зачем оно надо и чем оно лучше полностью статического сабтайпинга с объединениями?

Это, вроде как, его примитивная форма - сабтайпинг относительно Top, с явными кастами и разбором по типам, объединяемым в Top, в typecase. Можно обойтись и без кастов в Top, в boost::any, например, T <: any и можно свободно передавать T на место any, обратно - нужно делать any_cast в try/catch, или в switch по typeid (как раз typecase) и без исключений.

Настоящий сабтайпинг отличается тем, что имеет воздействие на рантайм (требует позднего связывания). Top, конечно, тоже имеет, но только там где он возникает.

Во-первых, внешний чекер анализирует обычный нетипизированный код.

Чтобы нормально работать такой чекер должен быть реализацией CL - он должен уметь экспанд макросов, а значит иметь определения всех стандартных макрсов, а экспандер завязан на вычислитель, значит уметь все стандартные функции и специальные формы. В том макросе я, например, использовал MOP чтобы рассматривать во время раскрытия какие слоты определены в классе, это просто проще чем внешний чекер который должен был бы идти искать и парсить defclass/destruct (но всё равно бы не смог, потому что, ещё раз, он не может быть внешним, учитывая специфику CL).

Но можно сделать, конечно.

Ну так в CL тоже можно. define-class, define-class-instance и slot-value выполняются последовательно, первые два успевают создать контекст, который будет использовать slot-value. Проблема в том, чтобы написать

(defstruct st a b) ;; standard `defstruct'

(let/typed ((x (make-st :a 1 :b 2) st)) ;; no TI, explicitly specified class `st'
  ;; using context created by expander for `let/typed':
  (slot-value/typed x 'bad-slot))
  ;; ^ ok: x : st, (find-class 'st), (not (find-slot-in-class 'bad-slot 'st)) => `error' during macroexpansion

ну и в том, что slot-value/typed - макрос, а не функция.

И то, как часто приложения пишут на агде

А Scala тут при том, что... :) Если надёжность не нужна, то непонятно, зачем typesafe так извращается (да и ещё и в такой предметной области - вебня). Дошли бы у них руки, они бы, наверное, вместо coffeescript и less css что-нибудь статически-типизированное сделали.

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

Ну да, упоминаются. Так же как и логические.

Отсуствие 100% покрытия - это вещь совершенно обычная.

Не понял перехода. Вроде выше говорилось о наличии ошибок, а тут вдруг откуда-то вылезло покрытие. Оно почти всегда 100%.

А то, насколько часто приложения пишут на Яве/Шарпе, демонстрирует... ну ты понел.

Нет, не понял. Договаривай

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

Почему не может? Вот определим, что так как оно сделано - оно не удобно. Можно обосновать что существенно иначе - нельзя.

Чтобы нормально работать такой чекер должен быть реализацией CL

Ага, в CL вообще нету исходного кода. По-этому анализировать просто нечего. И разговор об этом в контексте CL не имеет ни малейшего смысла.

Ну так в CL тоже можно.

Не, нельзя. Надо весь CL переписать, чтобы было можно.

define-class, define-class-instance и slot-value выполняются последовательно

В racket в module-level контексте оно может выполняться в любом порядке, то есть инстанцировать объект класса Foo можно до объявления Foo (главное чтобы он был объявлен в принципе). Ну и можно использовать все эти формы в любом лексическом контексте, в общелиспе - только в топ-левел. Да и как в CL сработает ассоциация с макросом данных любого вида я не совсем в курсе. Короче тьма фундаментальных проблем, которые в рамках общелиспового рантайма нерешаемы, более того - их решение противоречило бы стандарту.

ну и в том, что slot-value/typed - макрос, а не функция.

А в чем здесь проблема?

А в чем здесь проблема?

В том, что slot-value должна быть функцией (быть аргументом ФВП, например). В SBCL есть sb-c:define-source-transform с помощью которого можно «подмешать» функциям макро-подобные преобразования, так что можно сделать slot-value функцией и добавить статические проверки времени раскрытия source transformations. Но остальные проблемы неразрешимы, это верно.

В том, что slot-value должна быть функцией

Ну пусть она раскрывается в ф-ю в не-head контексте. Какие проблемы?

В SBCL есть sb-c:define-source-transform с помощью которого можно «подмешать» функциям макро-подобные преобразования, так что можно сделать slot-value функцией и добавить статические проверки времени раскрытия source transformations.

Тут главное понять, что:

1. в общелиспе нету ничег остатического, нету никакой компиляции, экспанда - есть только рантайм.

2. никаких проверок тоже нет, т.к. кода нет и проверять нечего

соответственно фраза «времени раскрытия source transformations» абсолютно бессмысленна. source не существует, а время раскрытия никогда не наступает, так что перевести ее следует как: «момент исполнения никогда не происходящего неопределенного процесса над несуществующим объектом».

Какие проблемы?

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

общелиспе нету...

Всё это есть, если посмотреть в CLHS, то определения соответствующих стадий можно найти (другое дело, что они циклически замкнуты в рамках одного рантайма). В SBCL - время раскрытия source transformations тоже есть, потому что есть макрос sb-c:define-source-transform который добавляет правило раскрытия во внутренние структуры компилятора, которое используется им на определённой стадии компиляции в машкод (ещё скажи, что машкода тоже нет), уже после maxroexpand-а, емнип.

Не понял перехода.

Если бы покрытие было 100%, этих ошибок не было бы.

А то, насколько часто приложения пишут на Яве/Шарпе, демонстрирует... ну ты понел.

Нет, не понял.

Всё ты понял.