История изменений
Исправление quasimoto, (текущая версия) :
Здесь у параметра x одинаковый тип или разный?
Конечно одинаковый — int.
Пусть есть тип «кольцо целых чисел». Алгебраическая структура включает в себя возможные операции (сложение, умножение). Пишу функцию (например, целочисленное деление). Это уже другой тип? Ведь количество операций изменилось...
Был конкретный тип, две конкретных замкнутых бинарных операции над ним сбоку, добавилась ещё одна конкретная (почти) замкнутая бинарная операция сбоку — исходный тип остался тот же.
Вот если упаковать этот тип, эти сложение и умножение и доказательства их свойств в структуру, то эта структура будет _моделью_ (реализацией) для _теории_ (интерфейса) «кольцо». Но модель и теория это тоже типы (зависимые, вообще говоря). От теории кольца добавлением сигнатуры операции деления и утверждений о её свойствах наследуется теория кольца с целочисленным делением, любая модель, типа нашего конкретного типа с таким делением, получается как структура агрегирующая модель кольца, модель деления и доказательства его свойств.
А www_linux_org_ru говорил про множество которое carrier структуры.
Исходная версия quasimoto, :
Здесь у параметра x одинаковый тип или разный?
Конечно одинаковый — int.
Пусть есть тип «кольцо целых чисел». Алгебраическая структура включает в себя возможные операции (сложение, умножение). Пишу функцию (например, целочисленное деление). Это уже другой тип? Ведь количество операций изменилось...
Был конкретный тип, две конкретных замкнутых бинарных операции над ним сбоку, добавилась ещё одна конкретная (почти) замкнутая бинарная операция сбоку — исходный тип остался тот же.
Вот если упаковать этот тип, эти сложение и умножение и доказательства их свойств в структуру, то эта структура будет _моделью_ (реализацией) для _теории_ (интерфейса) «кольцо». Но модель и теория это тоже типы (зависимые, вообще говоря). От теории кольца добавлением сигнатуры операции деления и утверждений о её свойствах наследуется теория кольца с целочисленным делением, любая модель, типа нашего конкретного типа с таким делением, получается как структура агрегирующая модель кольца, модель деления и доказательства его свойств.