Реализация компилируемого Python возможна?

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

Что-то не припомню ни одного языка, где все проверки типов были бы при компиляции. Разве что Haskell, но даже там есть fromDynamic.

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

Что касается проверок при компиляции, то им почти не поддаются интервальные типы, типы значений «ненулевой указатель», «непустой список», «матрица с ненулевым определителем», …

Что-то не припомню ни одного языка, где все проверки типов были бы при компиляции.

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

Он, видимо, имел ввиду ситуации, при которых для одного и того же статического типа допустимы разные множества операций(тоже разыменование - nullptr vs valid pointer value)

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

Что-то не припомню ни одного языка, где все проверки типов были бы при компиляции. Разве что Haskell, но даже там есть fromDynamic

Да, это правда, я не знаю ни одного языка, который бы достаточно исчерпывающе проводил проверку логической корректности своего кода до выполнения. Даже Ada. которая превращает в ад процесс разработки, все равно оставляет множество лазеек.

Да, это правда, я не знаю ни одного языка, который бы достаточно исчерпывающе проводил проверку логической корректности своего кода до выполнения.

Idris ?

Да, это правда, я не знаю ни одного языка, который бы достаточно исчерпывающе проводил проверку логической корректности своего кода до выполнения.

вы сначала дайте определение «логической корректности кода». статическая типизация определяет инварианты или ограничения на то, то вы пишете, и проверяет эти инварианты во время компиляции, если это возможно. если же это невозможно, по причинам очевидным, предлагаются опциональные(или неопциональные) рантаймовые проверки этих инвариантов. «динамическую типизацию», вообще сложно назвать типизацией. поскольку никто не собирается проверять простейших инвариантов - можно ли сложить a и б, или конкатенировать b и c. и есть ли у обьекта d метод toString(). и уж сколько обломов пожато на этой ниве, когда вдруг оказывается, что a и b сложить нельзя.

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

То, что уже есть в мейнстримных языках (хотя бы шарп/свифт/rust) всё же гораздо лучше, чем в питоне. Если добавить питоновскую практику «в любой непонятной ситуации бросай исключение» при том, что checked exceptions в принципе не планируются — даже аннотации типов + тот же mypy становятся заметно менее полезными. Хотя с ними и чуть легче, чем вообще без них.

все языки со статической типизацией. а их прилично. ну скажем так..99 процентов всяких проверок на этапе компиляции

только проверки типа отличить указатель от числа, а число от буквы.

И то: в Си число от буквы не отличается, в Паскале массивы с одинаковым количеством и типами элементов — разные типы, в Си++ невозможно указать, что параметр функции должен быть конкретного типа (подойдёт любой тип с заданным преобразованием).

Проблема статической титпизации в том, что она почти всегда загоняет доступные типы в прокрустово ложе некой системы, которую удобно реализовать в машинных кодах. И потом вместо типов предметной области программист выбирает самое близкое из доступных : ограниченное длиной double приближённое значение вместо точного ограниченного предметной областью для температуры и скорости, функция для работы с прямоугольниками не может работать с квадратами, списки и массивы не могут содержать значения разного типа, и т.д.

списки и массивы не могут содержать значения разного типа

Это фича.

поскольку никто не собирается проверять простейших инвариантов - можно ли сложить a и б, или конкатенировать b и c. и есть ли у обьекта d метод toString(). и уж сколько обломов пожато на этой ниве, когда вдруг оказывается, что a и b сложить нельзя.

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

статическая типизация определяет инварианты или ограничения на то, то вы пишете

Очень малое подмножество инвариантов (нельзя указать ни «непустой список» ни «ненулевое число» ни «отсортированный массив»). И в обмен на это крайне ограничивает возможные типы данных (нельзя в статических типах выразить ни лисповый map ни compose ни curry. Даже статические типы Typed Racket типа «список из 4 элементов с типами: целое, int32, рациональное, строка» или «функция принимающая int8 или int16 или int32 и возвращающая int16, если аргумент был int8, int32 если аргумент был int16, целое число, если аргумент был int32» в большинстве статических языков невозможны.

Это фича.

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

список из 4 элементов с типами: целое, int32, рациональное, строка

Это не список, а tuple. И это есть даже в сях, называется struct.

функция принимающая int8 или int16 или int32 и возвращающая int16, если аргумент был int8, int32 если аргумент был int16, целое число, если аргумент был int32

Перегрузка же много где есть?

«список из 4 элементов с типами: целое, int32, рациональное, строка» или «функция принимающая int8 или int16 или int32 и возвращающая int16, если аргумент был int8, int32 если аргумент был int16, целое число, если аргумент был int32» в большинстве статических языков невозможны.

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

Так в других языках слегка другие best practices. На лиспе это список потому, что так принято в лиспах. Но «список из элементов разного типа» — это не нормальный список. Юзкейс же — тупо контейнер для того, чтобы вернуть несколько значений из функции? В тот же map() такие вещи обычно не передают и оно даже не обязано быть iterable, если разобраться?

Да, это правда, я не знаю ни одного языка, который бы достаточно исчерпывающе проводил проверку логической корректности своего кода до выполнения.

Idris ?

Не знаком, но сомневаюсь, что там такое есть. Нужно ведь именно строить правила проверк инад правилами проверок до бесконечности, типа «вложений правил столько, сколько элементов в списке».

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

Самое интересно, что сколько ни пиши тестов на, скажем, a+b, все равно защиnbться от случая, когда в a и b попадет нечто несовместимое не получится. Просто потому что динамическая типизация по своей природе не накладывает никаких ограничений на то, какие значения могут попасть в a и b в ходе выполнения программы.

нельзя указать ни «непустой список» ни «ненулевое число» ни «отсортированный массив»

Омайгад, это все как раз тривиально делается: на уровень типов выносится понятие «непустой список/ненулевое число/отсортированный массив», а затем пишется функция, которая преобразует «сырой тип» в «обогащенный свойством» (хинт: функция sort может принимать «array of T» и возвращать «sorted_array of T»).

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

Любопытно, что подобие этой проблемы присутствует в стандартной библиотеке C: strchr и аналоги принимают const char*, а возвращают char*, потому что в системе типов const присобачен абы как. Но уже даже в плюсах можно написать аналогичную фунцию, которая будет сохранять константность. Кажется, даже в C11 можно.

Самое интересно, что сколько ни пиши тестов на, скажем, a+b, все равно защиnbться от случая, когда в a и b попадет нечто несовместимое не получится. Просто потому что динамическая типизация по своей природе не накладывает никаких ограничений на то, какие значения могут попасть в a и b в ходе выполнения программы

Ну такой себе аргумент. В Си тоже можно сделать какое-нибудь

a = 100+100;
a == -56 // true

Ну такой себе аргумент. В Си тоже можно сделать какое-нибудь

Что ты хотел этим показать? Никто в этом треде не говорит, что в C или даже в C++ сильная статическая типизация. Но сложить структуру с числом компилятор не позволит. И проконтролирует, что нигде в аргументах не просунут структуру вместо числа или наоборот (считаем, что все конструкторы/операторы преобразования типов explicit).

Самое интересно, что сколько ни пиши тестов на, скажем, a+b, все равно защиnbться от случая, когда в a и b попадет нечто несовместимое не получится. Просто потому что динамическая типизация по своей природе не накладывает никаких ограничений на то, какие значения могут попасть в a и b в ходе выполнения программы
Что ты хотел этим показать? Никто в этом треде не говорит, что в C или даже в C++ сильная статическая типизация. Но сложить структуру с числом компилятор не позволит. И проконтролирует, что нигде в аргументах не просунут структуру вместо числа или наоборот (считаем, что все конструкторы/операторы преобразования типов explicit)

a = Int(arg1)
b = Int(arg2)
c = a+b

Вот и защитились. Заодно, считай, и типы объявили. В стандартной либе питона такое сплошь и рядом.

Вот и защитились

Еще раз: эта проверка будет выполнена только в runtime. Нет ничего, что помешало бы тебе передать строки в arg1/arg2. Это частично решается аннотациями типов (не ручаюсь за точность названия), но это пришито сбоку и не особо удобно в использовании — как минимум надо натравливать сторонний чекер.

Еще раз: эта проверка будет выполнена только в runtime. Нет ничего, что помешало бы тебе передать строки в arg1/arg2

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

Вот и защитились. Заодно, считай, и типы объявили. В стандартной либе питона такое сплошь и рядом.

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

В любых раскладах где-то в каком-то месте нужно проводить валидацию

Если в крестах ты в объявишь прототип функции

std::string doit(Foo &foo, Bar &bar);

Теперь понятно, о чем речь?

Если в крестах ты в объявишь прототип функции
std::string doit(Foo &foo, Bar &bar);
То нигде в программе не сможешь написать int x = doit(5, 15); — компилятор не позволит. Никаких тестов, никаких преобразований. Просто на уровне типов нельзя передать 5 вместо Foo и 15 вместо Bar, а получившийся string запихнуть в int

Смогу, и напишу. Просто программа не скомпилируется. С таким же успехом можно говорить про «программа не пройдет тесты» или «программа не пройдет статический анализатор» — последние, к слову, есть и для крестов, чтобы ловить то, что штатный компилятор не ловит.

ну блин… скажите пожалста, какой физсмысл имеет ваш список «целое, int32, рациональное, строка»

Аргументы для некой функции. К этим аргументам в голову будет добавлено ещё два аргумента и вызвана функция с этими аргументами.

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

Умножение для аргументов int8 должно возвращать int16, для аргументов int16 возвращать int32, для int32 возвращать int64. На ассемблере примерно так: https://www.felixcloutier.com/x86/mul

std::string doit(Foo &foo, Bar &bar);

Зато работает такое:

mystring doit(Foo foo, Bar bar)
{
   return std::string("ok");
}
int main()
{
  int x = doit(5, 15);
}

Нет https://godbolt.org/z/EtYdr_

Ну так раз ты сам написал преобразования string -> mystring -> int, то чего ему не работать.

Зато работает такое:

Если слово explicit тебе не знакомо, то заработает.

Да https://godbolt.org/z/o7TrQ_

В IDE будут видны типы аргументов.

Так утверждение «просто на уровне типов нельзя передать 5 вместо Foo и 15 вместо Bar, а получившийся string запихнуть в int.» получается не всегда верно.

В IDE будут видны типы аргументов.

В смысле, тип числа 5? Или ожидаемый? Ожидаемый и в питоне виден (из документации).

Если ты не пишешь в конструкторе explicit, то ты про себя говоришь:«Да, я разрешаю приводится инту к Foo и Bar, а std::string может привестись к mystring».

Документацию еще прочесть нужно.

С учётом того, что конструкторов без explicit хватает и в стандартной библиотеке, о каком-то строгом контроле типов речи не идёт.

Причём неизвестно, что хуже, когда как в питоне упадёт при запуске или как в C++ преобразуется в другой тип и как-то выполнится.

Документацию еще прочесть нужно.

Я про ту, которая docstring. Её IDE читает.

С учётом того, что конструкторов без explicit хватает и в стандартной библиотеке, о каком-то строгом контроле типов речи не идёт.

Патчи никто не шлет Просто код написанный до, по моему, C++03 начнет сыпаться, так как, возможно, некоторый код надеется на неявное преобразование, а обратная совместимость в плюсах ставится выше.

Причём неизвестно, что хуже, когда как в питоне упадёт при запуске или как в C++ преобразуется в другой тип и как-то выполнится.

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

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

В std по-моему неплохо продумано, что сделать explicit, а что нет. Вообще, в плюсах подход explicit by default. Причем, в отличие от ошибок с типами в Питоне, здесь это контролируется статично, и некоторые линтеры выдают предупреждение, если не написать explicit.

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

Надо бы strong typedefs, но что-то в языке их нет, только костыли в левых библиотеках.