OberonCore

Перечитывал статью "Современное ИТ: индустрия и образование. Обзор языка Ada" С. И. Рыбин.
Там есть такой абзац: "Что такое тип данных? Вы же знаете, что это такое, попробуйте сказать это одним
предложением. (молчание) - "Область занимаемой памяти?" Отлично, варианты ещё
есть? (молчание) Вот смотрите - вы знаете, что такое тип данных. Единственная
версия - область занимаемой памяти. Я вам дам вторую версию: множество значений
при совокупности операций. Оно вам нравится как - больше, меньше? - "Ну, наверное,
надо еще знать, как оно представляется в памяти..." А вот теперь я вам скажу такую
вещь, что тип данных на самом деле есть описание содержательной роли объектов
данных, которую они играют в программе. Как вы на это смотрите? Концепция строгой
типизации, она вообще зачем нужна? Например, вы пишите некую программу -
автопилот чего-то, что летает. У этого автопилота есть понятие высоты и понятие
скорости. Они есть, если говорить про область памяти, если говорить про множество
значений при совокупности операций - то это число с плавающей точкой. Правильно? А
если говорить про содержательную роль, то это высота и скорость. Если вы
описываете разные типы данных для высоты и скорости, зачем вы это делаете? А
чтобы, упаси Бог, в первом часу ночи, когда вы в бреду горячечном, не успеваете -
если вы случайно высоте скорость присвоите, что будет? Если у вас это область
памяти - всем на это наплевать. Если у вас множество значений при совокупности
операций - всем наплевать. Если у вас разные содержательные роли, то вас должен
поймать компилятор. Именно для этого нужна концепция строгой типизации. Чтобы этой
вашей ошибке не дать дойти до работающей программы, чтобы вас отругали раньше. И
чем раньше вас обругают - тем легче вам будет жить...".
После чего я попробовал написать следующий код:

Все нормально откомпилировалось. Компилятор меня не "поймал".
Может быть есть какая-нибудь обция компилятора, которая отлавливает присваивание одного типа другому?
(BlackBox 1.6 rc6)

Однако, язык не тот.

Типы Height и Speed являются эквивалентными:

Надо не просто переименовать, а обернуть в record.

И добавить алгебру типов для данной предметной области:

тип "Сила" = тип "Масса" * тип "Ускорение"

тогда

var F : Sila;
M: Massa;
a: Uskorenie;

begin
M:=2; a:=3;
F := M*a;
end.

будет работать. По правилам Ньютона

Ну и само собой,
тип "Ускорение" = тип "Длина" / тип "Время"_квадрат

Правильно! И полный контроль типов будет обеспечен.

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

Почему, у вас єсть доказательство?
То что кому то не удалось ещё не повод говорить о том что это невозможно. Это говорит о трудности, но никак не о возможности.
Сам этим вопросом не занимался. Но вопрос считаю интересным.

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

proc Om (u,i,r);
if u = null then u:=i*r
elseif i = null then i:=u/r
elseif r = null then r:=u/i
end;

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

A/B + C*E/D = 0

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

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

Ну, лично я скептически отношусь к "умному" инструментарию

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

Обычная подоборка компонент + качественный 3GL-язык, по совокупности качеств, рулят

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

type A = real;
type B = real;
type C = A*B;

var k1,k2,k3 : real;
var a1,a2,a3 : A;
var b1,b2,b3 : B;
var c1,c2,c3 : C;

и транслятор должен транслировать

a2:=k1*a1;
b2:=k2*b1;
c2:=k3*c1;
a2:=a1/k1;
c2:=k3*a2*b1+a1*b2+c1;
b3:=c3/a3+b1;

и выдавать ошибку на

c2:=k2*a2;
a2:=a1/b2;
b2:=b1+k2;

А нафига он нужен, умный такой, язык-то?

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

Достаточно убрать смешение разных слоёв из фокуса внимания (т.е. позволить программисту забыть о машинном представлении, неявных приведениях типов и т.п.; а дать ему просто надёжное типизированное число; точно так же дать простой неломаемый указатель...) - и не будет этот программист делать глупых ошибок в выражениях и т.п. Потому что эти выражения - основная его работа, смысл программы. Раньше он отвлекался на всякую дрянь инструмента, не отвлекается - и отлично. А дальше усиливать контроль - особо сильного эффекта для качества ожидать не стоит. А вот как это повлияет на компилятор и рантайм - неясно. Поробуйте для разминки хотя бы ответить на вопрос, как эти механизмы будут себя вести при разнесении связанных соотношениями типов по разным модулям, в условиях раздельной компиляции, а тем более динамической загрузки?

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

Баланс - штука тонкая.

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

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

2. Когда программист использует сложный тип, транслятор знает все о составляющих этот тип:

тип А = композиция (Б,В,Г);

Дробавление операции (*) не добавляет необходимости никакой новой информации.

3. В константах операции такого типа разрешены, а связанные с этим трудности сопоставимы.


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


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

Не компетентен.

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

Таки глобальный анализ. "Обо всех.. Собирать..."

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

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

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

Неееееее....
Раздельная компиляция в том виде, как вы говорите - это простые текстовые файлы...
И не только раздельная компиляция, но и потом еще отдельный шаг сборки линкером...
А давайте доведем среду ББ до логического конца...
Модули - это не обычные текстовые файлы, а несколько более сложные структуры, в которых содержится полная информация о типах... См диссер Франца... И СРЕДА естественно, эту информацию по каждому проекту может собирать в некий отдельный контейнер...
Каждый модуль физически отдельно, но семантически - они в одном проекте...
Дело в среде - раз уж пошли по пути усложнения от простого текста к текстовому документу... Давайте доведем до логического конца: программа - не текст, а граф с гиперссылками. Который среда бдит, обрабатывает, хранит, изменяет и прочая...

А кто мешает, заводим тип для физ. величин в СГС

и вперед! Громоздко, правда, но если хочется непременно по-ньютону

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

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

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

Про необходимость глобального анализа для Хинди-Милнера читал у Шиперского в дисере.
Сам в детали автовывода не вникал; но примерно представляю.
Так вот: тип объекта явно не описан. Он конструируется исходя из способа использования объекта. А если объект используется за пределами модуля А, то мне, чтобы скомпилировать А (сопоставить тип объекту), нужно знать все случаи использования А. И перекомпилировать, если возникает новый случай.