Так ты можешь свои типы создать в любом языке. В чем проблема?
Окей, создай в ${язык-нейм} тип данных, включающий натуральные числа от 0 до 11, то есть подтип Nat, и который является кольцом по модулю 12.
Жду.
Блять можно вообще функцией ебануть, анон
int AddMod12(int a, int b) => (a + b) % 12;
А тип данных вот
public class Mod12
{
private readonly int v;
public Mod12(int value) => v = ((value % 12) + 12) % 12;
public static Mod12 operator +(Mod12 a, Mod12 b) => new(a.v + b.v);
public static Mod12 operator -(Mod12 a, Mod12 b) => new(a.v - b.v);
public static Mod12 operator (Mod12 a, Mod12 b) => new(a.v b.v);
public override string ToString() => v.ToString();
}
Вот только это всё в рантайме. Я говорю, чтобы всё было на уровне типов.
Day = Modulo Nat 12 # Модуль над множеством натуральных
a :: Day
a = 11
b :: Day
b = 1
main = a + b |> toString ~> stdout # Выведет 0
Можем придумать пример поинтересней: тип который описывает строки являющиеся валидными URL адрессами.
К примеру пусть будет функция send(URL, Binary).
Строчка send("Hello world!", "hi") отлетит с ошибкой еще на этапе компиляции.
Ну или более банальный, но важный пример RGB:
Опишем RGB как вектор:
RGB = Vector (RGBComponent, 3)
RGBComponent = Range (Nat, 0, 255)
И теперь и соответсвенно код типа
Button {
color: (400,500,100)
}
Просто не скомпилируется.
А у тебя вообще не происходит поддтипирования, ты оборачиваешь int в контейнер-класс. И я просил именно натуральные числа, а не int. Твой код обосрется, как только value будет отрицательным, а компилятор даже не пискнет на этот счет.
Всё так, но это фиксится рутинно костылями, чтобы код не обосрался.
btw тебе нужен Idris, Agda, F* или что-то такое. Но я вообще в душе не ебу что это за срань
Кстати, typescript очень близок. Там еще и типы зависимые. Для полноты картины только линейных/аффинных типов не хватает.
Если брать алгебраические типы, то как бы любой тип - это по определению множество значений. На это множество значений накладываются операции сложения и умножения. Еще иногда, очень редко встречается вычитание, например в js. Деление хз.
Что именно тебе надо-то?
>Там еще и типы зависимые.
Откуда они там? Или какая-то порезанная версия?
ADT в хаскелл это скорее про Теорию Категорий, а не про Теорию Множеств. Да и у них есть свои ограничения. К примеру ты не можешь сложить целое число с рациональным. Хотя вообще-то абсолютно любое целое число является рациональным, а значит никакой ошибки быть не может, такая операция допустима. Но GHC не пропустит.
Посмотри в сторону ZIG
Там можно через comptime запилить примерно то, что ты хочешь (но не полностью, естесна)
Там можно через comptime запилить примерно то, что ты хочешь (но не полностью, естесна)
>К примеру ты не можешь сложить целое число с рациональным.
Пик. Расскажешь почему это работает?
>скорее про Теорию Категорий, а не про Теорию Множеств.
Теоркат идет во всяких монадах и прочем говне. ADT причем тут? Это именно теория множеств. Ты легко можешь сделать множество любое, единственное ограничение, что там нельзя сделать бесконечные множетсва. Типа скажем натуральные. Но это ограничения компуктера в общем, а не ADT.
Ну и именно с рациональными.
>Типа скажем натуральные.
dat Nat = Z | S Nat
> бесконечные множетсва
Ко-типы. Хаскелл вообще крут, когда речь заходит о бесконечностях.
Вычитание для такого "натурального" числа напиши. А потом деление. Хотя возможно в этом случае и сложение уже сложно, нинаю.
Не ну обычно эти множества, которые счетные бесконечные задаются через условия. Так-то наверное ты прав, действительно можно и бесконечности задать.
В любом случае, мне интуитивно всегда казалось, что тип = множество. И так и не понел, что оп хочет.
> Вычитание для такого "натурального" числа напиши.
Вычитание не опеределено для натуральных чисел, деление не определено для целых. А вот сложение изи:
(+) :: Nat -> Nat -> Nat
S x + y = x + S y
Z + y = y
>И так и не понел, что оп хочет.
Он имел в виду определение типов через операции над множествами, как я понял.
К примеру операция деления (x / y) имеет сигнатуру x ∋ Q, y ∋ Q \ {0}.
То есть при компиляции у нас должны быть гарантии что в y никак не может попасть 0, иначе нескомпилируется, а значит есть гарантия, что division by zero exeption никогда не вылезет в рантайме.
>Вычитание не опеределено для натуральных чисел
Ну сделай не натуральными. Это же нумералы черча, я точно помню какая жопа реализовать там вычитание. Вот и хочу чтобы ты показал мастер класс.
А это точно экзепшен должен быть, а не скажем bottom?
>Binary — множество всех бинарных данных
ну вот например object, вообще общий тип
>omplex — множество комплексных чисел
эта хуйня только в математике нужна. можешь импортнуть библиотеку или сам написать классец за пару минут с реализацией операций
>List - списки (которые включает String, то текст - список символов)
можешь хранить символы в листе, но тебе нужны специализированные для строк операции, поэтому отдельная сущность
>Vector (который включает матрицы, ибо матрица - это вектор векторов), и так далее.
ну так лол ты можешь вектор векторов везде хранить, шаблонизация
кароч ты либо жирный, либо тупой даун, претендующий на интеллект, но жестко не вывозящий
понимаю что такое не спрашивают, и не в этом суть, но просто ответь - что это даст? Да, может будет удобнее, без лишних прослоек, компилируемо, но речь про функциональность - что это даст, в каких областях есть проблемы которые этим решают?
> система типов которого основана на теории множеств?
Трейты в Rust, очевидно же.
Естесно, что множества можно ограничивать.
Пусть у нас будет базовый тип (тип-юниверсум) Binary — множество всех бинарных данных, в том числе: Complex — множество комплексных чисел (которое в свою очередь включает все остальные типы чисел по цепочке), List - списки (которые включает String, то текст - список символов), Vector (который включает матрицы, ибо матрица - это вектор векторов), и так далее.
Я знаю, что Prolog во многом основан на Set Theory, но вот чтобы сама система типов была на ней основана, еще ни разу не видел.