Типи і функції

Це третя стаття в циклі «Теорія категорій для програмістів».

Категорія типів і функцій відіграє важливу роль у програмуванні, так що давайте поговоримо про те, що таке типи і навіщо вони нам потрібні.

Кому потрібні типи?

У спільноті є деякий незгоду про переваги статичної типізації проти динамічної і сильної типізації проти слабкою. Дозвольте мені проілюструвати вибір типізації за допомогою уявного експерименту. Уявіть собі мільйони мавп з клавіатурами, радісно жмущих випадкові клавіші, які пишуть, компілюють і запускають програми.

image



З машинним мовою, будь-яка комбінація байтів вироблена мавпами буде прийнята і запущена. Але у високорівневих мовах, високо цінується те, що компілятор здатний виявити лексичні та граматичні помилки. Багато програм будуть просто відкинуті, а мавпи залишаться без бананів, зате інші будуть мати більше шансів бути осмисленими. Перевірка типів забезпечує ще один бар'єр проти безглуздих програм. Крім того, в той час як в динамічно типізованих мовах невідповідності типів будуть виявлені тільки під час виконання, в строго типізованих статично перевіряються мовами невідповідності типів виявляються під час компіляції, що відсіває безліч некоректних програм, перш ніж у них є шанс бути запущеними.

Отже, питання в тому, чи хочемо ми, щоб мавпи були щасливі, або створювати коректні програми?

Зазвичай мета уявного експерименту з друкуючими мавпами — створення повного зібрання творів Шекспіра (прим. перекладача: або Війна і Мир Толстого). Перевірка орфографії та граматики в циклі різко збільшить шанси на успіх. Аналог перевірки типів піде ще далі: після того, як Ромео оголошений людиною, перевірка типів переконається, що на ньому не ростуть листя і що він не ловить фотони своїм потужним гравітаційним полем.

Типи потрібні для компонуемости

Теорія категорій вивчає композиції стрілок. Не будь-які дві стрілки можуть бути скомпоновані: цільовий об'єкт однієї стрілки повинен збігатися з вихідним об'єктом наступної. У програмуванні ми передаємо результати з однієї функції в іншу. Програма не буде працювати, якщо друга функція не може правильно інтерпретувати дані, отримані з допомогою першої. Обидві функції повинні підходити один до одного, щоб їх композиція запрацювала. Чим сильніше система типів мови, тим краще це подхождение можна описати і автоматично перевірити.

Єдиний серйозний аргумент, який я чую проти суворої статичної типізації: вона може відкинути деякі програми, які семантично правильні. На практиці це трапляється вкрай рідко (прим. перекладача: під уникнення срача зауважу, що тут автор не врахував, або незгодний, що є багато стилів, і звичний программсистом на скриптових мовах duck-typing теж має право на життя. З іншого боку, duck-typing можливий і в строгій системі типів через templatees, traits, type classes, interfaces, є багато технологій, так що думка автора не можна вважати строго невірним.) і, в будь-якому випадку, кожна мова містить якийсь чорний хід, щоб обійти систему типів, коли це дійсно необхідно. Навіть Haskell має unsafeCoerce. Але такі конструкції повинні використовуватися розумно. Персонаж Франца Кафки, Грегор Замза, порушує систему типів, коли він перетворюється в гігантського жука, і ми всі знаємо, як це скінчилося (прим. перекладача: погано :).

Інший аргумент, який я часто чую, в тому, що сувора типізація накладає занадто багато навантаження на програміста. Я можу співчувати цій проблемі, так як сам написав кілька оголошень ітераторів в С++, тільки от є технологія, висновок типів, яка дозволяє компілятору вивести більшість типів з контексту, в якому вони використовуються. В С++, ви можете оголосити змінну auto, і компілятор виведе тип за вас.

В Haskell, за винятком рідкісних випадків, анотації типу є опціональними. Програмісти, як правило, все одно їх використовують, тому що типи можуть багато розповісти про семантику коду, і оголошення типів допомагають розуміти помилки компіляції. Звичайна практика в Haskell — починати проект з розробки типів. Пізніше, анотації типів є основою для реалізації і стають гарантованими компілятором коментарями.

Сувора статична типізація часто використовується як привід для нетестирования коду. Іноді ви можете почути, як Haskell-програмісти кажуть: «Якщо код збирається, він правильний.» Звичайно, немає ніякої гарантії, що програма, коректна з точки зору типів, коректна в сенсі правильного результату. В результаті такого ставлення у ряді досліджень Haskell не став сильно випереджати інші мови за якістю коду, як можна було б очікувати. Здається, що в комерційних умовах необхідність лагодити баги існує тільки до певного рівня якості, що в основному пов'язано з економікою розробки програмного забезпечення та толерантності кінцевого користувача, і дуже слабо пов'язане з мовою програмування або методологією розробки. Кращим критерієм було б виміряти, скільки проектів відстає від графіка або поставляється з сильно зниженими функціоналом.

Тепер, що стосується твердження, що модульне тестування може замінити строгу типізацію. Розглянемо загальну практику рефакторінгу в строго типізованих мовах: зміна типу аргументу функції. У сильно типізованих мовах достатньо змінити декларацію цієї функції, а потім виправити всі помилки збірки. У слабо типізованих мовах, той факт, що функція тепер очікує інші дані не може бути пов'язаний із зухвалою стороною.

Модульне тестування може зловити деякі з невідповідностей, але тестування практично завжди імовірнісний, а не детермінований процес (прим. перекладача: можливо, мався на увазі набір тестів: ви покриваєте не всі можливі входи, а якусь репрезентативну вибірку.) Тестування — погана заміна доказу коректності.

Що таке типи?

Найпростіше опис типів: вони являють собою безлічі значень. Типу Bool (пам'ятаєте, конкретні типи починаються з великої літери в Haskell) відповідає множина з двох елементів: True і False. Тип Char — множину всіх символів Unicode, наприклад 'a' або 'ą'.

Множини можуть бути кінцевими або нескінченними. Тип String, який, по суті, синонімом списку Char, — приклад нескінченної безлічі.

Коли ми оголошуємо x, як Integer:
x: Integer

ми говоримо, що це елемент множини цілих чисел. Integer в Haskell — нескінченна безліч, і може бути використане для арифметики будь-якої точності. Є і кінцеве безліч Int, яке відповідає машинного типу, як int C++.

Є деякі тонкощі, які роблять прирівнювання типів до множиною складним. Є проблеми з поліморфними функціями, які мають циклічні визначення, а також з тим, що ви не можете мати безліч всіх множин; але, як я і обіцяв, я не буду суворим математиком. Важливо те, що є категорія множин, яка називається Set, і ми з нею будемо працювати.
У Set, об'єкти — це множини, а морфизмы (стрілки) — функції.

Set — особлива категорія, тому що ми можемо зазирнути всередину її об'єктів і це допоможе багато інтуїтивно зрозуміти. Наприклад, ми знаємо, що порожня множина елементів. Ми знаємо, що існують спеціальні безлічі з одного елемента. Ми знаємо, що функції відображають елементи однієї множини в елементи іншого. Вони можуть відображати два елемента в один, але не один елемент в два. Ми знаємо, що тотожна функція відображає кожен елемент множини в себе, і так далі. Я планую поступово забувати всю цю інформацію і замість цього висловити всі ці поняття в чисто категорійної формі, тобто в термінах об'єктів і стрілок.

В ідеальному світі ми могли б просто сказати, що типу в Haskell — множини, а функції в Haskell — математичні функції між ними. Існує лише одна маленька проблема: математична функція не виконує який-небудь код — вона знає лише відповідь. Функція в Haskell повинна відповідь обчислювати. Це не проблема, якщо відповідь може бути отриманий за кінцеве число кроків, яким би великим воно не було. Але є деякі обчислення, які включають рекурсію, і ті можуть, ніколи не завершитися. Ми не можемо просто заборонити незавершающиется функції в Haskell тому, що розрізнити завершується функція, чи ні — знаменита проблема зупинки — нерозв'язна. Ось чому вчені-комп'ютерники придумали геніальну ідею, або брудний хак, в залежності від вашої точки зору, — розширити кожен тип спеціальним значенням, называнным bottom (прим. перекладача: цей термін (bottom) чується як-то по-дурному російською, якщо хто знає хороший варіант, будь ласка, пропонуйте.), яке позначається _|_ або в Unicode ⊥. Це значення відповідає незавершающемуся обчисленню. Так функція, оголошена як:
f :: Bool -> Bool

може повернути True, False, або _|_; останнє означає, що функція ніколи не завершується.

Цікаво, що, як тільки ви приймаєте bottom в систему типів, зручно розглядати кожну помилку часу виконання за bottom, і навіть дозволити функції повертати bottom явно. Останнє, як правило, здійснюється з допомогою виразу undefined:
f :: Bool -> Bool
f x = undefined

Це визначення проходить перевірку типів тому, що undefined обчислюється в bottom, яке включено в усі типи, в тому числі і Bool. Можна навіть написати:
f :: Bool -> Bool
f = undefined

(без x) тому, що bottom ще й член типу Bool -> Bool.

Функції, які можуть повертати bottom, називаються частковими, на відміну від звичайних функцій, які повертають правильні результати для всіх можливих аргументів.

З-за bottom, категорія типів Haskell і функцій, називається Hask, а не Set. З теоретичної точки зору, це джерело нескінченних ускладнень, тому на даному етапі я використовую мій ніж м'ясника і завершу ці міркування. З прагматичної точки зору, можна ігнорувати незавершающиеся функції та bottom і працювати з Hask як з повноцінним Set.

Навіщо нам математична модель?

Як програміст, ви добре знайомі з синтаксисом і граматикою мови програмування. Ці аспекти мови, як правило, формально описуються в самому початку специфікації мови. Але сенс і семантика мови набагато важче описати; це опис займає набагато більше сторінок, рідко досить формально, і майже ніколи не повно. Звідси ніколи не закінчуються дискусії серед мовних юристів, і вся кустарна промисловість книг, присвячених тлумаченню тонкощів мовних стандартів.

Є формальні засоби для опису семантики мови, але через їх складності вони в основному використовуються для спрощених, академическии, мов, а не реальних гігантів промислового програмування. Один з таких інструментів називається операційна семантика і описує механіку виконання програми. Він визначає формалізований, ідеалізований інтерпретатор. Семантика промислових мов, таких як C++, як правило, описується за допомогою неформального міркування, часто в термінах «абстрактної машини».

Проблема в тому, що про програми, що використовують операційну семантику дуже важко щось довести. Щоб показати якесь властивість програми ви, по суті, повинні «запустити її» через ідеалізований інтерпретатор.

Не важливо, що програмісти ніколи формально не доводять коректність. Ми завжди думаємо, що ми пишемо правильні програми. Ніхто не сидить за клавіатурою, кажучи: «О, я просто напишу кілька рядків коду і подивлюся, що відбувається." (прим. перекладача: ах, якби...) Ми вважаємо, що код, який ми пишемо буде виконувати певні дії, які дадуть бажані результати. Ми, як правило, дуже здивовані, якщо це не так. Це означає, що ми дійсно думаємо про програми, які ми пишемо, і ми, як правило, робимо це, запускаючи інтерпретатор в наших головах. Просто, дуже важко встежити за всіма змінними. Комп'ютери гарні для виконання програм, люди — ні! Якщо б ми були, нам би не знадобилися комп'ютери.

Але є й альтернатива. Вона називається денотаційної семантикою і заснована на математиці. У денотаційної семантики для кожної языкорой конструкції описана математичесая інтерпритація. Таким чином, якщо ви хочете довести властивість програми, ви просто говорите математичну теорему. Ви думаєте, що доказываание теорем важко, але насправді ми, люди, будували математичні методи тисячі років, так що є безліч накопичених знань, які можна використовувати. Крім того, порівняно з теоремами, які доводять професійні математики, задачі, з якими ми стикаємося в програмуванні, як правило, досить прості, якщо не тривіальні. (прим. перекладача: для доказу, автор не намагається образити програмістів.)

Розглянемо визначення функції факторіалу в Haskell, мовою легко піддається денотаційної семантики:
fact n = product [1..n]

Вираз [1..n] — це список цілих чисел від 1 до n. Функція product примножує всі елементи списку. Точно так, як визначення факторіала, взяте з підручника. Порівняйте це з C:
int fact(int n) {
int i;
int result = 1;
for (i = 2; i < = n; i++)
result *= i;
return result;
}

Чи потрібно продовжувати? (прим. перекладача: автор трохи схитрував, взявши бібліотечну функцію в Haskell. Насправді, хитрувати було не потрібно, чесне опис за визначенням не складніше):
fact 0 = 1
fact (n) = n * fact (n - 1)

Добре, я відразу визнаю, що це був дешевий прийом! Факторіал має очевидне математичне визначення. Проникливий читач може запитати: Яка математична модель для читання символу з клавіатури, або відправлення пакета по мережі? Довгий час це був би нетактовне запитання, що веде до досить заплутаних пояснень. Здавалося, денотационная семантика не підходить для значного числа важливих завдань, які необхідні для написання корисних програм, які можуть бути легко вирішувані операційної семантикою. Прорив стався з теорії категорій. Еугенио Моджі виявили, що обчислювальні ефекти можуть бути перетворені в монади. Це виявилося важливим спостереженням, яке не тільки дало денотаційної семантики нове життя і зробило чисто функціональні програми більш зручними, але й дало нову інформацію про традиційному програмуванні. Я буду говорити про монадах пізніше, коли ми розробимо більше категорійних інструментів.

Одним з важливих переваг наявності математичної моделі для програмування є можливість виконати формальний доказ коректності програмного забезпечення. Це може здатися не настільки важливим, коли ви пишете споживчий софт, але є області програмування, де ціна помилки може бути величезною, або там, де людське життя знаходиться під загрозою. Але навіть при написанні веб-додатків для системи охорони здоров'я, ви можете оцінити ту думку, що функції та алгоритми із стандартної бібліотеки мови Haskell йдуть в комплекті з доказами коректності.

Чисті і Брудні функції

Те, що ми називаємо функціями в C++ або будь-якому іншому імперативний мовою, не те ж саме, що математики називають функціями. Математична функція — просто відображення значень значення.

Ми можемо реалізувати математичну функцію на мові програмування: така функція, маючи вхідний значення буде розрахувати вихідну значення. Функція для отримання квадрата числа, ймовірно, збільшить вхідна значення сама на себе. Вона буде робити це при кожному виклику, і гарантовано зробить однаковий результат кожного разу, коли вона викликається з одним аргументом. Квадрат числа, не змінюється з фазами Місяця.

Крім того, обчислення квадрата числа не повинно мати побічного ефекту видачі смачного ништячка вашому собаці. «Функція», яка це робить, не може бути легко змодельована математичної функцей.

У мовах програмування функції, які завжди дають однаковий результат на однакових аргументах і не мають побічних ефектів, називаються чистими. У чистому функціональному мовою зразок Haskell всі функції чисті. Завдяки цьому простіше визначити денотационную семантику цих мов і моделювати їх за допомогою теорії категорій. Що стосується інших мов, то завжди можна обмежити себе чистим підмножиною, або міркувати про побічні ефекти окремо. Пізніше ми побачимо, як монади дозволяють моделювати всі види ефектів, використовуючи тільки чисті функції. В результаті ми нічого не втрачаємо, обмежуючись математичними функціями.

Приклади типів

Як тільки ви вирішите, що типи — це множини, ви можете придумати деякі вельми екзотичні приклади. Наприклад, який тип, відповідає порожньому безлічі? Ні, це не void C++, хоча цей тип називається Void в Haskell. Це тип, який не наповнений ні одним значенням. Ви можете визначити функцію, яка приймає Void, але ви ніколи не зможете її викликати. Щоб викликати її, вам доведеться забезпечити значення типу Void, а його там просто немає. Що стосується того, що ця функція може повернути — не існує ніяких обмежень. Вона може повертати будь-який тип (хоча цього ніколи не станеться, тому що вона не може бути викликана). Іншими словами, це функція, яка полиморфна за повертається типу. Хаскеллеры назвали її:
absurd :: Void -> a

(прим. перекладача: на С++ таку функцію визначити неможливо: в С++ у кожного типу є хоча б одне значення.)

(Пам'ятайте, що a — це змінна типу, яка може бути будь-яким типом.) Це ім'я не випадково. Існує більш глибока інтерпретація типів та функцій з точки зору логіки під назвою ізоморфізм Каррі-Говарда. Тип Void являє неправдивість, а функція absurd — твердження, що з хибності слід що-небудь, як у латинській фразі «ex falso sequitur quodlibet.» (прим. перекладача: з хибності слід що завгодно.)

Далі йде тип, відповідний одноэлементному безлічі. Це тип, який має тільки одне можливе значення. Це значення просто «є». Ви могли відразу його не визнати, але це void у C++. Подумайте про функції від і до цього типу. Функція void завжди може бути викликана. Якщо це чиста функція, вона завжди буде повертати один і той же результат. Ось приклад такої функції:
int f44() { return 44; }

Ви можете подумати що ця функція приймає «нічого», але, як ми тільки що бачили, функція, яка приймає «нічого» не може бути викликана, тому що немає ніякого значення, що представляє тип «нічого». Отже, що ж ця функція приймає? Концептуально, вона приймає фіктивне значення, у якого є тільки єдиний екземпляр, так що ми можемо явно його не вказувати в коді. В Haskell, однак, є символ цього значення: порожня пара дужок (). Таким чином, за забавного збігу (або не збіг?), виклик функції від void виглядає однаково і в C++ і в Haskell. Крім того, із-за любові Хаскеля до лаконічності, той же символ () використовується і для типу, конструктора і єдиного значення, відповідного одноэлементному безлічі. Ось ця функція в Haskell:
f44 :: () -> Integer
f44 () = 44

Перша лінія заявляє, що f44 перетворює тип (), оголошений «одиниця», тип Integer. Друга рядок визначає f44 з допомогою патерн-матчинга перетворює єдиний конструктор для одиниці, а саме (в число 44. Ви викликаєте цю функцію, надаючи значення ():
f44 ()

Зверніть увагу, що кожна функція від одиниці еквівалентна вибору одного елемента з цільового типу (тут, вибирається Integer 44). Насправді, ви можете думати про f44, як іншому представленні числа 44. Це приклад того, як ми можемо замінити пряме згадка елементів множини на функцію (стрілку). Функції з одиниці в якийсь тип А знаходяться у взаємно-однозначного відповідності з елементами множини A.

А як щодо функцій, які повертають void, або, в Haskell, повертають одиницю? В C++ такі функції використовуються для побічних ефектів, але ми знаємо, що такі функції не справжні, в математичному сенсі цього слова. Чиста функція, яка повертає блок нічого не робить: вона відкидає свій аргумент.

Математично функція з множини А в одноэлементное безліч відображає кожен елемент в єдиний елемент цієї множини. Для кожного А є рівно одна така функція. Ось вона для Integer:
fInt :: Integer -> ()
fInt x = ()

Ви даєте їй будь-яке ціле число, і вона повертає одиницю. Дотримуючись духу лаконічності, Haskell дозволяє використовувати символ підкреслення в якості аргументу, який відкидається. Таким чином, не потрібно придумувати для нього назву. Код вище можна переписати у вигляді:
fInt :: Integer -> ()
fInt _ = ()

Зверніть увагу, що виконання цієї функції не тільки не залежить від значення, переданого їй, але і від типу аргументу.

Функції, які можуть бути визначені однією і тією ж формулою для будь-якого типу називаються параметрично поліморфними. Ви можете реалізувати ціле сімейство таких функцій одним рівнянням, використовуючи параметр замість конкретного типу. Як назвати поліморфну функцію з будь-якого типу в одиницю? Звичайно, ми будемо називати її unit:
unit :: a -> ()
unit _ = ()

В C++ ви б реалізували її так:
template < class T>
void unit(T) {}

(прим. перекладача: щоб допомогти компілятору оптимізувати її в noop, краще так):
template < class T>
void unit(T&&) {}

Далі в «типологію типів» набір з двох елементів. В C++ він називається bool, а в Haskell, що не дивно, Bool. Різниця в тому, що в C++ bool є вбудованим типом, в той час як в Haskell він може бути визначений наступним чином:
data Bool = True | False

(Читати це визначення стоїть так: Bool може бути або True або False.) В принципі, можна було б описати цей тип і в C++:
enum bool {
true,
false
};

Але C++ перерахування насправді ціле число. Можна було б використовувати C++11 «class enum», але тоді довелося б уточнювати значення ім'ям класу: bool::true або bool::false, не кажучи вже про необхідність включати відповідний заголовок в кожному файлі, який його використовує.

Чисті функції Bool просто вибирають два значення цільового типу, одне, відповідне True і інше — False.

Функції Bool називаються предикатами. Наприклад, бібліотека Data.Char Haskell містить багато предикатів, наприклад IsAlpha або isDigit. В C++ є схожа бібліотека, яка оголошує, крім іншого, функції isalpha і isdigit, але вони повертають int, а не булевое значення. Справжні предикати визначені і називаються ctype::id(alpha, c) і ctype::is(digit, c).

Теорія категорій для програмістів: передмова
Категорія: суть композиції
Типи і функції

Джерело: Хабрахабр

0 коментарів

Тільки зареєстровані та авторизовані користувачі можуть залишати коментарі.