xacid: (Default)
Читаю на досуге теорию типов, а так же вдохновленный недавно прочитанным уже эссе о тотальном программировании Д. Тёрнера, думаю на досуге же вот примерно о чем. Рассуждения конечно не Бог весть какие :) Но для меня некоторые моменты таким образом становятся вполне очевидны, впрочем конечно пока образования не хватает судить насколько рассуждения эти адекватны. Идея примерно следующая:

Пока мы с помощью рекурсии определяем натуральные числа как N = 0 | 1 + N, и затем опять таки через примитивную рекурсию определяем операции сложения и умножения - всё получается замечательно: в результате сложения и умножения двух натуральных чисел мы очевидным образом получаем опять натуральное число.

Однако дальше начинаются некоторые проблемы. Разность чисел (очевидным образом обратная к сложению операция) уже является частичной функцией (на множестве натуральных чисел). А с операцией обратной к умножению - то есть с делением, всё еще хуже - в результате деления двух натуральных чисел мы можем получить уже не только не натуральное число (то есть не целое), а даже вообще не совсем до конца вычислимое число - например если разделим 10 на 3 - получим бесконечную дробь, и даже вообще не число а самую настоящую ошибку - на ноль же делить нельзя ведь.

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

Если мы желаем (а мы желаем!) чтобы функция разности чисел была тотальной, то все что нам нужно для этого сделать - ввести тип "отрицательных чисел", и построить новое надмножество "целых чисел", которое понятное дело является дизъюнктной суммой множеств "отрицательных" и "натуральных" чисел. Дальше больше - операция деления натуральных чисел в результате дает нам тип "рациональных чисел", как тип-произведение двух натуральных чисел - делимого и делителя. И еще деление нам дает сразу необходимость определять тип "ошибка" - в данном случае это будет ошибка деления на ноль. То есть деля два числа мы должны в результате получить тип-сумму из двух типов - либо рациональный результат либо ошибка. И никак иначе!

Что меня в данный момент смущает в этих выводах? Во-первых то что в большинстве используемых на практике языков программирования всего этого нет, а числа определяются вообще не очень понятными типами byte, short, int, long или float, double которые возникают непосредственно из ограничений архитектуры компьютеров. При этом самое забавное что совершая какие либо арифметические действия с например типом int я в результате получаю тоже тип int, но при этом это является грубой ошибкой, поскольку может возникнуть переполнение. Вообще, очень смешно иногда спросить кого нибудь кто считает себя хорошим программистом - "Как правильно сложить два числа int в Java или C?". Мало кто вспомнит что нужно делать это так

long add(int a, int b) { return (long)a + (long)b; }.

И таких косяков во всем этом - вагон и маленькая тележка.

И вот наводит это всё на достаточно грустные мысли - ведь если даже такие простые вещи числа и арифметика не определены и не реализованы нормальным образом в инструментах которые мы используем, то о чем можно вообще говорить дальше?

Profile

xacid: (Default)
xacid

June 2017

S M T W T F S
    123
45678910
11121314151617
18192021222324
252627282930 

Syndicate

RSS Atom

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Jul. 26th, 2017 06:36 am
Powered by Dreamwidth Studios