Зачем нужна статическая типизация?, или Вы всё врете!

сей разработчик не владеет

А ещё можно почтальонам одноколёсные велосипеды раздавать вместо нормальных, а потом жаловаться на нехватку кадров.

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

Так нет же. Должно быть

sort : {A : Set} {_≤_ : A → A → Set} → (∀ x y → (x ≤ y) ⊎ (y ≤ x)) → (l : List A) → Σ[ l' ∶ List A ] (Sorted _≤_ l' × Permutation l l')

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

Вот этот Σ[ l' ∶ List A ] (Sorted _≤_ l' × Permutation l l') легко запилить в виде функции-контракта, но невозможно в виде типа-класса (по крайней мере в C++).

иллюстрирую:

идея это - «а давайте-ка накатим по маленькой, господа!», это может и хорошая, но идея.

а концепция целое всепобеждающее учение.

Это вообще чудесно, требовать от языка, который не делает проверку на типы, чтобы он её делал. Один только вопрос, почему вы не переписывали его с 2.7 на жабку?

Эткуда вы такие беретесь, с Луны прилетаете? Потому что нам за это не заплатили. Потому что датасаентисты хотят панду, нампи, и тензорфло а не жабку. Потому что тебя забыли спросить

принципиально, чтобы средства ЯП позволяли выражать постусловия, предусловия и инварианты.

Динамически это проверять можно хоть на ассемблере.

call checkInvariants
call checkPreCond
...
...
...
call checkPostCond
call checkInvariants

И условия могут быть любыми.

Статически это сводится к некой системе типов. От тривиальной сишной до навороченной Agda и Typed Racket. Условия ограничены системой типов.

А я вообще чувак не модный. На скутере не езжу, смузи не заказываю. Хмуро жарю простую картошечку на сковороде, а потом иду читать непонятные для вас книжки. Мне почти 40 лет, и я могу себе позволить не заниматься борьбой с ветряными мельницами.

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

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

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

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

inf myfunction(int param){
}

class MyType{
private:
    int return_value;

public:
  MyType(int param){
      this.return_value = toReturnValue(param);
  }
  
  int getReturmValue(){ 
       return return_value;
  }

}

то есть, если мы умеем toReturnValue(param), то завернуть это в тип - вопрос чисто технический.

Если вы не понимаете аналогий, то это точно не моя проблема.

а концепция целое всепобеждающее учение.

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

Если вы не понимаете аналогий, то это точно не моя проблема.

Так я же аутист. Куда мне.

Вы показали «проблему», которая возникает в статическом ЯП.

1. Докажите, что это проблема.
2. Докажите, что в динамическом ЯП это не проблема.

А то вдруг окажется, что это не проблема вовсе. Или проблема, но как раз в динамическом ЯП. Неудобно получится.

И если его длины хватит.

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

Динамически это проверять можно хоть на ассемблере.

ну да, в принципе любой тьюринг полный ЯП можно выразить на любом другом тьюринг полном ЯП.

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

это я к тому, что ЯП - это сначала «язык», а потом уже «программирования».

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

наличие выразительных средств - это важно.

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

Напиши декларацию функции sort.

Для зависимых типов было бы так:

SortedVectorOf(a) sort(vector<int> a)

Но в C++ нет зависимых. Для

SortedVectorOfA sort(vector<int> a)

Невозможно добавить проверку на то, что передаваемый в конструктор SortedVectorOfA массив является перестановкой массива a.

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

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

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

что она нужна не во всех языках, юзкейсах и не всем пользователям

Возможность статической типизации не помешала бы во всех языках.

Даже классическое ООП с наследованием уже является нарушением строгой типизации, так как позволяет переменной одного типа присваивать значения другого типа.

Подтипа.

Невозможно добавить проверку на то, что передаваемый в конструктор SortedVectorOfA массив является перестановкой массива a.

в декларацию - невозможно. а было бы красиво и удобно, да.

От того невозможно, что сделать неохота.
У меня для каждого поля и объекта можно задать семантику любой сложности.

Вот опять приходится говорить о своей разработке, а иначе суждения будут от «диванного теоретика».

Ну да. Если с ним относится именно как с заявленным контрактом, то всё хорошо.

Но на практике всюду есть приведение типа предка к типу потомку.

Эту семантику ведь нельзя проверить на этапе компиляции.

ну вы считаете легальным присваивание int32 в int64? обычно это считают легальным, а вот при обратном присваивании вас ругнут.

int32 это подтип int64

Потом будет:

3. Докажи, что ты мне доказал.
4. Докажи, что я с тобой согласился.
5. …

Зачем, реальность всё расставила по своим местам. Да и потом, ретрограды тоже нужны. Должен же кто-то поддерживать старые монолиты на яве. Уж точно не я.

обычно это считают легальным, а вот при обратном присваивании вас ругнут.

Не ругается: https://godbolt.org/z/djGbK7ETj

Как-то без огонька ты слился.

У меня API ориентировано на run-time.

Всё дело в том, что все СУБД, форматы данных, ... имеют некую
архитектуру представления данных, которая компилятору известна.
Core API обеспечивает создание и работу с объектами в run-time.

Не скажу, что это «панацея», просто такого рода API потребно в многих задачах.

monk, супер красиво, когда некой функции передаю путь к директории в которой находится сотня (например) xlsx.
Функция анализирует все xml файлы и динамически создаёт метаданные.

А строчкой ниже вызываем функцию, загружающюю xlsx и работаем с ним.

Это был один из примеров использования API.

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

флаг -Wconversion вставьте. код такой:

#include <cstdint>
int main() 
{
    std::int64_t c = 500;
    std::int32_t b = c;
    c = c + b;
}

Например у Вас имеется объект «Треугольник», который содержит некоторые данные о нём, а в свойствах Вы можете указать его: тип, ограничения на длины сторон, ...

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

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

Как-то 1С немного поведала о своём проекте.
По 25000 классов для x86, apple и ёщё чегой-то там.

Шутка

Вот до чего людей доводит ООП!

флаг -Wconversion вставьте.

Точно. У gcc -Wall какой-то совсем не «all»…

Конечно читаю Ваши посты.
Кое-что из Вами предложенного в разработке, а многое ещё предстоит сделать.

Мы ещё не коснулись темы линковки данных.
Тема для меня весьма близка и «есть, что сказать и разработать».

Ныне технологии работы с данными «застыли в 60-х».
Не могу даже придумать объяснение, почему всё так.

Просьба продолжить диалоги в треде.
ИМХО тред весьма хорош.

---------------------------------------------------------
Шас картошки с лучком нажарю.

Почему что-то куда-то отправляется?

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

в рантайме?

настоящий контрактно-ориентированный ЯП должен давать описывать контракты декларативно и проверять их на этапе компиляции

Что именно там является одновременно и клубникой и каракатицей?

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

Но как раз таки статическая типизация в этом случае позволит не страдать при рефакторинге.

Шутка

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

Но на практике всюду есть приведение типа предка к типу потомку.

Вот это интересный кейс для обсуждения.

Что именно препятствует выстраиванию полностью верифицируемой на этапе статического анализа системы типов и что с этим делать.

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

Что именно там является одновременно и клубникой и каракатицей?

Объект живой природы, который надо как-то описать в рамках данной архитектуры.

Каким образом появление нового концепта

Вы сейчас хотите рассказать, что нужно было заранее подумать и создать достаточно расширяемую систему? Ну, удачи. ООП изначально продавалось как «напишите достаточно гибкую иерархию классов и вы получите переиспользуемые компоненты». На практике выяснилось, что каждое изменение требований приводят к изменениям архитектуры же, поэтому иерархия классов созданная для проекта А годится только для неё же и задействовать его в проекте Б не получается. Такова реальность.

Эээээээээээээээээ, расскажу свой любимый.

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

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

в твоей вселенной? в нашей с «переиспользуемыми компонентами» все ок, репозитории мейвена завалены просто всем этим переиспользуемым.

– Везде молоко, даже в умывальнике! (с)

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

Мы от вас пытаемся добиться ответа на вопрос, какие проблемы вы видите в вашем примере, которые якобы есть в ст. ЯП и якобы отсутствуют в дин. ЯП.

ООП изначально продавалось как «напишите достаточно гибкую иерархию классов и вы получите переиспользуемые компоненты».

Так вы со своим воображаемым ООП спорите, как оказывается. Иерархия абстракций создаётся под решаемую задачу и зависит от самой задачи. Универсальной иерархии не существует и не может существовать, это было бы как «теория всего».

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

Интересно, как вы задействуете иерархию типов для системы видеомониторинга в программе для рассчёта химических реакций. Есть идеи?

Вот такое вот воображаемое ООП.

ООП изначально продавалось как «напишите достаточно гибкую иерархию классов и вы получите переиспользуемые компоненты»

Это кто такое заявлял? Именно про переиспользуемость компонентов.

настоящий контрактно-ориентированный ЯП должен давать описывать контракты декларативно и проверять их на этапе компиляции

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

А на этапе компиляции мы можем получить только статическую типизацию. При достаточно мощной системе типов с её помощью можно производить некоторые достаточно сложные проверки при компиляции: монадические законы, a + b - b == a, a + (b + c) = (a + b) + c и подобные.

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

ну вот существуют фреймворки типа QT, и все ими прекрасно пользуются и не переписывают под себя.

сами такие фреймворки формируют экосистемы, и открывают вам новые возможности.

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

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

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

Всё это нужные инструменты, но не относящиеся к вопросам о статической типизации.

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

Очень рад за вас. Даже жаль, что всё это выкидывают и переписывают на Go и Js.

Документация на буквально каждую библиотеку, будь она написана хоть на Си, хоть на Питоне представляет собой:

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

Форумные аналитики: «ООП провалилось. Повторное использование кода оказалось невозможно.»