clojure после common lisp - насколько омерзительно и в чём именно?

Единственный аргумент который мне кажется существенным, это

Злобный матан, однако.

Т.е. расшифровывая, я прочитал три тома software foundations, на что ушло около двух лет емнип. Ну плюс хаскель/идрис.

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

И хотя вероятно _можно_ было ограничиться меньшей подготовкой (если бы были курсы в университете и т.п.), но порог вхождения во всё это всё равно не такой уж маленький. В этом смысле то что раст не взял себе зависимые типы а ограничился линейными - вполне может быть большим преимуществом. И LH по этой же причине мне кажется интересным.

Если ставить вопрос широко - то я думаю что всему этому научиться не сложнее чем объектно-ориенированному программированию.

Но здесь и сейчас люди умеют в ООП (ну.. как то), но соверешнно не умеют в приличные типы. И пока индустрия сдвинется (?) пройдёт время.

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

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

Кроме того, контракты, как я понял, это пусть довольно продвинутые, но всего лишь тесты. Т.е. ну на конкретном наборе данных у тебя отработало. А что с другим набором?

Контракты по своей сути для использования в рабочей системе. И их цель: локализовать любую ошибку при эксплуатации до модуля/функции.

А доказательтво - это гарантия, что функция соответствует спецификации. Т.е. вот для любой такой ф-ции, оно будет работать как описано и всё тут.

При верных начальных условиях и правилах вывода. Когда в реальности a * b / b не равно a, всё не так однозначно.

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

Мне она кажется более низкоуровневой. Вместо «первый элемент» приходится расшифровывать «такой элемент x с индексом ix, что для любого другого элемента y с индексом iy …».

Скорее всего корректность функции contract а потом её эквивалентность функции argmax.

∀ f,l contract f l (argmax f l) ≡ истина

Это в общем то довольно сложный код который надо запускать на разных данных чтобы найти ошибку. Т.е. это тесты.

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

Во вторую – документирование.

Их можно использовать для тестов, в том числе в стиле QuickCheck со случайными данными. Но это не основная их цель.

В этом смысле то что раст не взял себе зависимые типы а ограничился линейными - вполне может быть большим преимуществом. И LH по этой же причине мне кажется интересным.

Матан не в типах, а в доказательстве. В типах слегка напрягает излишний boilerplate, если сравнивать с refined типами, как в LH или Racket, но это реально вопрос привычки.

И просто описать зависимые типы через параметры шаблонов даже в С++ можно.

Можно написать assume, но в контракты времени выполнения условие не сконвертируется и вполне может оказаться ложным.

Не совсем по теме, но ведь и проверка каких-то контрактов может быть слишком дорогой, чтобы её выполнять каждый раз?

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

Может. В этом смысле мой argmax - это антипример (зато статически доказуемый). В реальных программах добиваются того, чтобы время выполнения контракта было пренебрежимо мало по сравнению с временем выполнения функции. Ну и компилятор помогает, выкидывая то, что при конкретном вызове очевидно. В Racket есть Contract Profiler для проверки.

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

Не совсем. Тут всё таки разница: типы в отличие от кода это что то что связывает систему в единое целое, которое потом проверяет машина. Я не знаю как эму мысль верно передать, но одно из проявлений этого свойства в том что ошибка в типе легче заметна чем ошибка в коде. Т.е. типы не сойдутся и это видно сразу. А код - пока не запустишь, никто не знает что там. Тем более слабо типизированный код.

В этом смысле зависимые типы - это типы, а контракт - это всё таки больше код.

Другое свойство (на мой взгляд) отличающее код от доказательтва: это дискретность доказательства. В том смысле что код, понимаешь, опять же, его надо написать и он может содержать и почти всегда содержит ошибки. Доказательство - совсем другая вещь, оно либо есть, либо его нет. И проверять доказательство не нужно, его проверяет машина. Проверять нужно только типы. (при этом внутри системы опять же проверяет машина, но спецификации идут отдельно от системы, как бы).

Говоря коротко, код более «хлипкий» что ли. И гораздо более нудный.

Контракты по своей сути для использования в рабочей системе. И их цель: локализовать любую ошибку при эксплуатации до модуля/функции.

Зависимые типы лучше во всём кроме того что в это «слёту» не въедешь. В отличие от тестов/контрактов.

При верных начальных условиях и правилах вывода. Когда в реальности a * b / b не равно a, всё не так однозначно.

Этот аргумент меня начинает смущать. Я на него уже отвечал:
1) ну будет вместо равенства какой нибудь оператор close_to x y delta, так же индуктивно определённый, ну будем доказывтаь не равенство а достаточную близость. Бог с ним, если подход существует, значит разберёмся.

2) я этого ещё не говорил, но тебя ведь не смущает в питоне x[0.5], хотя казалось бы, никто не гарантирует что x[0.5] = x[0.5 * b / b]. И ничего, все живы.

Мне она кажется более низкоуровневой. Вместо «первый элемент» приходится расшифровывать «такой элемент x с индексом ix, что для любого другого элемента y с индексом iy …».

Кстати, к слову. А почему тебя смущает «на каждый чих» писать новые типы, а новые функции (как в твоём контракте) - не смущает?

∀ f,l contract f l (argmax f l) ≡ истина

Спасибо, что то не заметил, а ведь вроде очевидно.

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

Во вторую – документирование.

Их можно использовать для тестов, в том числе в стиле QuickCheck со случайными данными. Но это не основная их цель.

Документирование по моему у зависимых типов не хуже. За пояснение спасибо.

Матан не в типах, а в доказательстве.

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

Т.е. как пример

after : (xs ys : list a) -> (length xs < length ys) -> list a
after (x::xs) (y::ys) prf = after xs ys (congr S prf)
after [] ys _ = ys

after : (xs ys : list a) -> (length xs < length ys) -> (zs : list a ** 0 < length zs)
after (x::xs) (y::ys) prf = after xs ys (congr S prf)
after [] ys prf = (ys, prf)

А что с++? Как работать там со всем этим

#include <optional>
#include <iostream>
#include <istream>

template <class T>
auto is_not_zero(T x) { return x != 0; }

enum class GuardMode { Repeat, Optional };

template <class T, bool (*guard)(T), GuardMode Mode = GuardMode::Repeat>
struct InputMonad
{
	static auto Get(std::istream &input = std::cin)
	{
		if constexpr (Mode == GuardMode::Repeat)
		{
			T res;
			do std::cin >> res;
			while (!guard(res));
			return res;
		}

		else
		{
			T res;
			std::cin >> res;
			if (guard(res))
				return std::optional(res);
			else
				return std::optional<T>();
		}
	}
};

template <class T, GuardMode Mode = GuardMode::Repeat>
using NonZeroInput = InputMonad<T, is_not_zero<T>, Mode>;

template <class T>
auto operator/(T a, std::optional<T> b) -> std::optional<T>
{
	if (!b)
		return {};
	return a / *b;
}

template <class T, GuardMode Mode>
auto div(int a, NonZeroInput<T, Mode> b) { return a / b.Get(); }

int main()
{
	auto n = NonZeroInput<int>();
	std::cout << div(12, n) << std::endl;

	auto m = NonZeroInput<int, GuardMode::Optional>();
	auto a = div(12, m);
	std::cout << (a ? *a : -1) << std::endl;
}

сделать ты всё равно с этим ничего не сможешь

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

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

Дело в том что в LH практически зависимые типы. Т.е. Вот то как ты ими пользуешься это практически аналог моего псевдокода для after на идрис.

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

Т.е. если это что то развитое, то от доказательств ты не уйдёшь, только неудобно себе сделаешь. Кмк.

Понял, что меня здесь напрягает. Твой after имеет не два аргумента, а три. After xs ys prf. А как им пользоваться?

То есть какой-нибудь нибудь вызов наподобие after (cons 1 x) x true как проверять тип будет?

Ты не можешь передать туда true, это не булев тип. Это прям такой тип length xs < length ys. соотвественно туда можно передать только это значение. Если ты его откуда то с собой имеешь, то туда его и пиши, вроде так

(prf, zs) = after xs ys proof_len_xs_lt_len_ys

lenlt : (xs ys : list a) -> Either (length xs < length ys) (length xs >= length ys)
lenlt [] y::ys = Left (length [] < length (y::ys)
lenlt xs [] =  Right (length xs >= length [])
lenlt x::xs y::ys = congr S (lenlt xs ys)

case lenlt (Cons 1 x) x of
  Left prf => Some (after (Cons 1 x) x prf)
  Right prf => None

Так lh зато без дополнительных намёков выводит доказательство для after. Или код типа

f :: { x:Double | x > -273.5 } -> Double

g x = if x > -50 then f x else x

И чтобы не компилировалось

g1 = if x > -300 then f x else x

Как хотя бы сформулировать на зависимых типах?

Так здесь он тоже внешний относительно after. То есть опечатка типа

case lenlt x (Cons 1 x) of
  Left prf => Some (after (Cons 1 x) x prf)
  Right prf => None

скомпилируется и упадёт. Или нет?

Как то так (в фигурных скобках неявный параметр, он должен выводиться из контекста).

gt_trans : {z : double} -> (x : double) -> (prf : x > y) -> {y > z} -> (x > z)

gt_dec : (x y : double) -> Either (x > y) (x <= y)

f : (x : Double) -> (prf : x > -273.5) -> Double

g x = if gt_dec x -50 == Left prf 
      then 
         f x (gt_trans x prf )
      else
         x

g1 = if x > -300 then f x else x

не скомпилируется, prf - это будет доказательство того что length x < length (Cons 1 x) потому что мы так указали в типе функции lenlt (Left - длина первого переданного списка меньше длины второго), а after ждёт что длина переданного *ему* первого меньше длинs переданного ему второго (т.е. length (Cons 1 x) < length x, так в типе after после специализации переданными значениями), т.е. типы не сойдуться

да, там я порядок параметров перепутал, должно быть так

case lenlt x (Cons 1 x) of
  Left prf => Some (after x (Cons 1 x) prf)
  Right prf => None

так lh зато без дополнительных намёков выводит доказательство для after.

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

Кстати здесь у тебя длина Cons 1 x и x при выполнении проверяется? У меня ведь статически было. Исходя из

Cons :: a -> {x:List a} -> {r:List a|length r = length x + 1}

Если вариант именно (cons 1 x и x), то доказательство можно просто предоставить как вызов функции, как то так должно сработать по идее. В этом случае компилятор не должен вызывать его в рантайме, так как доказательство не зависит от конкретных параметров.

len_x_xs : {x} -> {xs} -> length xs < length (x::xs)
-- библиотечная функция

(zs, prf) = after x (Cons 1 x) len_x_xs

Вообще это классная фича - что lh выводит много. Но всё это должно работать и в идрисе/агде/коке, причём ровно так же. И в Идрисе даже как то работало. Похоже что lh - это попытка прибить какую то часть зависимых типов гвоздями прям сверху хаскеля, и чтоб не слишком сложно было. Но по моему не слишком сложно там только в самом начале. Но надо сказать в самом начале оно и в Идрисе несложно, (хотя соглашусь что lh выглядит немного более «по свойски, по программистки, а не вот это вот всё»)

А если не библиотечная?

Пусть вообще из внешней библиотеки с сигнатурой

addElem:: a -> {x:List a | length x > 0} -> {r:List a|length r > length x}

Как это вообще записать на зависимых типах?

Я на идрисе видел нормальные (с моей точки зрения) типы.

after :: Vect a n -> Vect b m -> Vect b m

Только некуда вписать n < m

А на LH основная проблема в том, что солвер плохо работает с рекурсивными условиями.

А если не библиотечная?

Я упоминаю в том смысле что писать вроде не надо, это всё есть. А так - всё равно.

addElem:: a -> {x:List a | length x > 0} -> {r:List a|length r > length x}

addElem : a -> (x : List a) -> (r:List a ** length r > length x)
addElem a x = (Cons a x, len_x_xs)

addElem : a -> (x : List a) -> (length x > 0) -> (r:List a ** length r > length x)
addElem a x _ = (Cons a x, len_x_xs)

А если не лишнее? Мы же не знаем тела addElem. Там может быть чтение первого элемента. И получается, что любая функция с ограничениями должна возвращать пару? А тип пары точно можно описывать через **? И как в константу len_x_xs попадает информация про x и r?

По моим личным впечатлениям, вектор немного неуклюжий. Но для данного случая довольно несложно выглядит:

after :: (n < m) -> Vect a n -> Vect b m -> Vect b (m - n)

А на LH основная проблема в том, что солвер плохо работает с рекурсивными условиями.

Дело в том что система неразрешима (а если ограничить её до разрешимой, то она будет неинтересна.. т.е. что то нетривиальное не выразишь) и поэтому солвер всегда будет работать плохо.

А если не лишнее?

я поправил

В смысле, неразрешима? Там те же условия, что и в идрисе, но не отдельными аргументами, а частями уже существующих. Если же надо такой аргумент сделать при выполнении, то он делается через условие в if. В остальном полное соответствие один-к-одному. Свой злой матан для доказательств тоже есть. Я пытаюсь его осмыслить, чтобы для argmax адаптировать. Автоматика ломается на рекурсивности функций обхода списка в контракте.

Ну, не разрешима в общем случае. Иначе бы не существовало верных утверждений которые нельзя доказать. А они (в рамках зависимых типов) существуют. Соответсвенно солвер построить нельзя.

Правда с подсказками получается весьма интересно. В cpdt (книжка по коку) солвер всю рутину решает прям, если подсказки давать. Автор его назвал crush, что честно говоря отражает суть.. Попробую его к аргмаксу, когда время найду (вот сегодня можно было, но всё на ЛОР потратил :) )

И получается, что любая функция с ограничениями должна возвращать пару?

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

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

А тип пары точно можно описывать через **

Ну в Коке через *, а в идрисе кажется через **.

И как в константу len_x_xs попадает информация про x и r?

len_x_xs (кстати, я не знаю как она в библиотеке называется, чтоб не вводить в заблуждение). Может она и не нужна кстати, но отвечая на вопрос, в общем случае на примере len_x_xs, она описана так:

len_x_xs : {x} -> {xs} -> length xs < length (x::xs)

addElem : a -> (x : List a) -> (r:List a ** length x < length r)
addElem a x = (Cons a x, @len_x_xs a x)

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

Не выкидывает. Она остаётся частью типа результата.

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

Всю информацию о типах можно выкинуть на этапе компиляции.

Не выкидывает. Она остаётся частью типа результата.

Ну ситуация аналогична. В остальных языках тоже выкидывают если могут.

Кстати, я пошёл и поглядел таки, liquid haskell это похоже действительно зависимые типы, правда внутри (про ликвид хаскель не нашёл, но они на сайте lh дают ссылку на статью ниже, думаю что это основа, собственно). Но всё что применимо к зависимым типам (в смысле разрешимости там и прочих добрых свойств), должно быть применимо и к ликвид хаскель. Единственное, правда, lh может быть более ограниченным, потому что там исходный язык lh переводится в язык зависимых типов. Т.е. исходный язык может быть менее выразительным чем зависимые типы, но я не разбирался там. Правда из цитаты ниже создаётся впечатление что это именно так и есть. Вот статья http://goto.ucsd.edu/~rjhala/liquid/liquid_types.pdf

вот цитата

We present Logically Qualified Data Types, abbreviated to LiquidTypes, a system that combines Hindley-Milnertype inference with Predicate Abstraction to automatically infer dependent types precise enough to prove a variety of safety properties. Liquid types allow programmers to reap many of the benefits of dependent types, namely static verification of critical properties and the elimination of expensive run-time checks, without the heavy price of manual annotation.

Всю информацию о типах можно выкинуть на этапе компиляции.

В зависимых типах не всегда получается на практике (а в теории я не помню что там к чему). Но таки в большинстве случаев это работает.

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

Если надо, можно в явном виде тип Proof использовать:

https://github.com/ucsd-progsys/liquidhaskell/blob/develop/tests/pos/MapReduceVerified.hs

На мой взгляд более читабельно, чем https://github.com/andreykl/argmax/blob/main/argmax.v

Хотя argmax я так и не смог на нём сочинить.

Спасибо за пример большое.

Т.е. я понимаю, NonZeroInput специализируется типом того что нужно прочитать и режимом. Я так же понимаю что Get возвращает либо T либо optional<T>, как повезёт. Но ведь выбор делается на этапе компиляции. Зачем мы тогда так возимся?

Может я не так понял?

Может на after получится понятнее, если найдёшь время, конечно. Буду благодарен.

Но ведь выбор делается на этапе компиляции. Зачем мы тогда так возимся?

Там просто, как принято в C++, куча параметров. Что делать: если 0, то ли ошибку сразу, то ли ложь. Вдруг ошибку, вычисленную на этапе компиляции, мы всё равно хотим видеть в тесте.

А так это обычный

div :: Int -> {y:Int | y /= 0} -> Int

Вот менее замусоренный вариант:

template <int N>
struct lessthan {
    int x;

    lessthan(int x_){
        if(x_ < N)
            x = x_;
        else
            throw "user bad";
    }

    template <int M>
    lessthan(lessthan<M> other){
        // try to prove statically
        if constexpr(N <= M){
            x = other.x;
        } else {
            // do a runtime check if proof fails
            if(other.x < N)
                x = other.x;
            else
                throw "user bad";
        }
    }
}
lesstan<100> f(lessthan<50> x) // эквивалент f :: {x:Int | x <= 50} -> {r:Int | r <= 100}

мне кажется или

// try to prove statically
        if constexpr(N <= M){

должно быть М < N?

Да, разумеется. Это просто пример.

То есть статические типы от целых значений вполне можно сообразить. Проблема возникает либо с вещественными типами, либо для длинных списков (он же не доказывает разворачиваемость, а реально разворачивает все вызовы до конца списка).

Этот пример гораздо проще. Вроде я понял. Спасибо большое за пример! Уже соображаю плоховато, видно спать давно пора уже , засиделся.

а вот такое сложно изобразить?

getType : Int -> Type
getType 42 = String
getType _ = Int

workingFunction : (x: Int) -> (getType x)
workingFunction 42 = "Мужик, это был смысл жизни, вселенной и всего такого!"
workingFunction x = x*2

а вот такое сложно изобразить?

template <int X> struct getType
{
   using type = int;
};

template <> struct getType<42>
{
   using type = std::string;
};

template <int X>
typename getType<X>::type workingFunction()
{
  return X*2;
}

template <>
typename getType<42>::type workingFunction<42>()
{
  return "Мужик, это был смысл жизни, вселенной и всего такого!";
}

А как выглядит вызов?

К слову, на идрисе как то так. Правда я сменил условие выбора типа на булевское, но это не так важно. И не уверен что даже так скомпиляется (из за того что булевское и x /= 42 никак не связано). И пример, конечно, вырожденный: мы в итоге таскаем с собой булевское значение которое используем чтобы вывести на экран результат.

Но это именно из-за простоты примера. Вот тут у Брэди на ~ 10:50 показан типобезопасный printf с использованием этой техники. Т.е. это действительно рабочий инструмент.

module Main

toMaybeInt : String -> Maybe Int
toMaybeInt = ?toint

getType : (isInt : Bool) -> Type
getType False = String
getType True = Int

workingFunction : (x: Int) -> getType (x /= 42)
workingFunction 42 = "Мужик, это был смысл жизни, вселенной и всего такого!"
workingFunction x = x*2

showAnswer : (isInt : Bool) -> getType isInt -> String
showAnswer True i = "Квадрат числа равен" ++ show i
showAnswer False s = s

main : IO ()
main = do mbint <- map toMaybeInt getLine
          case map (\x => (x, x /= 42)) mbint of
            Just (x, isInt) => putStr $ 
                showAnswer isInt (workingFunction x)
            Nothing => putStr "Нужно вводить целое число"

Т.е. в «искусственном случае» можно вызвать так (должно скомпиляться)

getType : (isInt : Bool) -> Type
getType False = String
getType True = Int

workingFunction : (x: Int) -> getType (x /= 42)
workingFunction 42 = "Мужик, это был смысл жизни, вселенной и всего такого!"
workingFunction x = x*2

main : IO ()
main = do putStr $ workingFunction 42
          putStr $ "Квадрат 122 равен " ++ (workingFunction 122)

А как выглядит вызов?

   std::cout << workingFunction<42>() << "," << workingFunction<33>() << std::endl;

типобезопасный printf

А если в него шаблон из пользовательского ввода грузить, то что будет?

"Квадрат 122 равен " ++ (workingFunction 122)

String ++ Int ? Так можно?

getType (x /= 42)

Если getType здесь служебный, а не определяющий, в C++ можно вообще так:

template <int X>
auto workingFunction()
{
  return X*2;
}

template <>
auto workingFunction<42>()
{
  return "Мужик, это был смысл жизни, вселенной и всего такого!";
}

Может отдельную тему создадим? А то вроде в теме про clojure и про статическую типизацию…

да, стоит, ты прав.

В лиспе независимость модулей на честном слове.

Что ты подразумеваешь под «независимостью», невозможность изменять? Я не считаю, что в лиспе это нужно по-дефолту. Во-первых, как ты сказал, это язык изначально для небольших команд, стартапов например. Зачем самим себя ограничивать? А если для больших систем подтребуется подобное ограничение и набирать в команду по объявлениям на столбах - что именно помешает внедрить необходимые механизмы хоть бы и на уровне рантайма?

В принципе, аналогичная проблема у C++ с указателями

Мне кажется, такое сравнение некорректно.

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

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

Гм. В питоне запрещено.

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

Это, как я понимаю, только в случае с непреднамеренным затиранием имени или что-то еще имеется ввиду?

Имени, значения. Содержимого любого экспортированного объекта

Для начала - import * и его аналоги в лиспе - это плохое импортирование вообще, даже в питоне так делать не принято, не известно же что вообще тебе прилетит в скоуп. И это хорошо, если ты импортируешь в начале модуля. А если в середине? ССЗБ, короче.

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

Нет, «поломал» ее ты. Другой человек честно использовал (в описанном тобой примере) библиотеку, как ее написал разработчик. А если ты переопределяешь у себя какую-то функциональность, этот другой парень, раз уж вы с ним вместе работаете, должен быть об этом в курсе. И уже завязываться на API твоей библиотеки, либо запрет подобных трюков на уровне коде стайла. Вариант, где вы оба друг о друге не знаете и ты просто используешь библиотеки из разных источников, при этом самых их патчишь как тебе вздумаете, ну что сказать, ссзб, если ты модифицируешь кишки либы, на которую завязаны другие либы. Ведь ты предварительно мог об этом узнать, правда?

А потом если кто-то захочет найти, почему (defcfun sin :double (x :double)) у него принимает целые значения, ему придётся перелопатить половину потрохов библиотеки cffi.

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

Как в Racket или python. Можно переопределить любую функцию поверх импортированной.

В CL тоже можно, но ты ведь внуть пакета залазишь. Это как раз твой пример с foo.f1 = f1.

Без явного указания модуля не работает.

import * плохая практика, да система модулей в CL не идеальная, но ее можно при желании дотюнить и все будет так же (или лучше) как в питоне.

Чем больше людей, тем больше разброс квалификации.

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

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

Изоляцию можно прикрутить, «можнасделать»(с) кароче.

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

В lisp’е затирает

[1]> (defpackage :p1 (:use :cl) (:export :f1 :f2))
#<PACKAGE P1>
[2]> (in-package :p1)
#<PACKAGE P1>
P1[3]> (defun f1 (x) (+ x 1))
F1
P1[4]> (defun f2 (x) (+ (f1 x) 1))
F2
P1[5]> (f2 3)
5
P1[6]> (defpackage :p2 (:use :cl :p1))
#<PACKAGE P2>
P1[7]> (in-package :p2)
#<PACKAGE P2>
P2[8]> (defun f1 (x) (- x 1))
F1
P2[9]> (f2 3)
3

Для начала - import * и его аналоги в лиспе - это плохое импортирование вообще

Писать

(itearate:iter (com.clearly-useful.iterate+:per c iterate:in a)
 	       (com.clearly-useful.iterate+:per d iterate:in b)
  (iterate:always (seq-equalp c d))

мягко говоря неудобно. Намного проще

(iter (per c in a)
      (per d in b)
  (always (seq-equalp c d))

но для этого приходится импортировать iterate и com.clearly-useful.iterate+.

В lisp’е затирает

Правильно, здесь же по-другому работают пакеты. Что мешает нормально проимпортировать f2?

(defpackage :p2 (:use :cl)(:import-from :p2 :f2))
(in-package :p2)
(defun f1 (x) (* x 10))
(f1 3) ;=> 30
(f2 3) ;=> 5

- все «как в питоне». Более того, если очень хочется можно вообще пакет заблочить от любых изменений, даже когда все символы импортируются через :use. :cl-package-locks и подобное. после (lock-package (find-package :p1)) будешь получать эрроры на попытки вообще что бы то ни было переопределить.

Тебе не нравится, что :use по-дефолту так работает? Ну так здесь так специально сделано, _именно_ для того, чтобы было обозначенное тобой поведение.

(itearate:iter (com.clearly-useful.iterate+:per c iterate:in a)

Так писать конечно же не надо, это понятно. Но только потому что DSL и неудобно конкретно в этом случае. А вообще именно так и надо писать и в упомянутом к ночи питоне все вот так вот и делают - import numpy as np и дальше np.hello, np.xyz по коду. Какие варианты лучше?

но для этого приходится импортировать iterate и com.clearly-useful.iterate+.

И в чем проблема? iterate это, считай, стандарт. Если не нравятся какие-то имена или ты у тебя предполагаются конфликты - можешь зашедовить или удалить / добавить синонимы там где надо. А что тут теоретически может быть лучше? макрос (iterate ... должен внутри своих скобочек создавать скоуп? Как именно?

(:import-from :p2 :f2)

*(:import-from :p1 :f2) - obvious fix.

import numpy as np

Вот именно: as np. Но в CL такой формы нет. Я пытался сделать https://github.com/Kalimehtar/advanced-readtable , но интеграция со SLIME страдала. Да и судя по количеству звёзд не особо и нужно.

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

(setf elem
  (unless (com.clearly-useful.generic-collection-interface:empty-p 
  arr)
    (com.clearly-useful.generic-collection-interface:element-at arr n)))

iterate это, считай, стандарт

Их там таких десятка полтора. Возьми hu.dwim получишь ещё полсотни слов «стандарта». И в каждом крупном проекте свой «стандарт». А если что-то случайно затрёшь, приятной отладки (хорошо, в отладчике имена с пакетом видны).

макрос (iterate … должен внутри своих скобочек создавать скоуп? Как именно?

Мой advanced-readtable предлагает push-local-package.

после (lock-package (find-package :p1)) будешь получать эрроры

Угу. Включая локальные переменные в let и локальные функции в flet и labels.