Статична і динамічна типізація

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

Тип — це колекція можливих значень. Ціле число може мати значення 0, 1, 2, 3 і так далі. Логічне може бути істиною чи брехнею. Можна придумати свій тип, наприклад, тип "ДайПять", в якому можливі значення "дай" і "5", і більше нічого. Це не рядок і не число, це новий, окремий тип.
Статично типізовані мови обмежують типи змінних: мова програмування може знати, наприклад, що x — це Integer. У цьому випадку програмісту забороняється робити
x = true
, це буде некоректний код. Компілятор відмовиться компілювати його, так що ми не зможемо навіть запустити такий код. Інший статично типізований мова може володіти іншими виражальними можливостями, і жодна з популярних типів систем не здатна висловити наш тип ДайПять (але багато можуть висловити інші, більш витончені ідеї).
Динамічно типізовані мови позначають значення типами: мова знає, що 1 це integer, 2 це integer, але він не може знати, що змінна x завжди містить ціле число.
runtime мови перевіряє ці мітки в різні моменти часу. Якщо ми спробуємо скласти два значення, то вона може перевірити, чи є вони числами, рядками або масивами. Потім вона складе ці значення, склеїть їх або видасть помилку, залежно від типу.
Статично типізовані мови
Статичні мови перевіряють типи в програмі під час компіляції, ще до запуску програми. Будь-яка програма, в якій типи порушують правила мови, вважається некоректною. Наприклад, більшість статичних мов відхилить вираз
"a" + 1
(мова Сі — це виняток з цього правила). Компілятор знає, що "a" — це рядок, а 1 — це ціле число, і що
+
працює тільки коли ліва і права частина відносяться до одного типу. Так що йому не потрібно запускати програму, щоб зрозуміти, що є проблема. Кожен вираз в статично типизированном мові належить до певного типу, який можна визначити без запуску коду.
Багато статично типізовані мови вимагають позначати тип. Функція в Java
public int add(int x, int y)
приймає два цілих числа і повертає третє ціле число. Інші статично типізовані мови можуть визначити тип автоматично. Та ж сама функція додавання в Haskell виглядає так:
add x y = x + y
. Ми не розголошуємо мові типи, але він може визначити їх сам, бо знає, що
+
працює тільки на числах, так що
x
та
y
повинні бути числами, значить функція
add
приймає два числа як аргументи.
Це не зменшує "статичність" системи типів. Система типів в Haskell знаменита своєю статичністю, строгістю і потужністю, і за всім цим фронтах Haskell випереджає Java.
Динамічно типізовані мови
Динамічно типізовані мови не вимагають вказувати тип, але і не визначають його самі. Типи змінних невідомі до того моменту, коли у них є конкретні значення при запуску. Наприклад, функція в Python
def f(x, y):
return x + y

може складати два цілих числа, склеювати рядка, списки і так далі, і ми не можемо зрозуміти, що саме відбувається, поки не запустимо програму. Можливо, в якийсь момент функцію f викличуть з двома рядками, і з двома числами в інший момент. В такому випадку x і y будуть містити значення різних типів в різний час. Тому говорять, що значення динамічних мовами володіють типом, але змінні і функції — немає. Значення 1 це виразно integer, але x і y можуть бути чим завгодно.
Порівняння
Більшість динамічних мов видадуть помилку, якщо типи використовуються некоректно (JavaScript — відоме виключення; він намагається повернути значення для будь-якого вираження, навіть коли воно не має сенсу). При використанні динамічно типізованих мов навіть проста помилка виду
"a" + 1
може виникнути в бойовому оточенні. Статичні мови запобігають такі помилки, але, звичайно, ступінь запобігання залежить від потужності системи типів.
Статичні і динамічні мови побудовані на фундаментально різних ідеях про коректність програм. У динамічному мовою
"a" + 1
це коректна програма: код буде запущений і з'явиться помилка в середовищі виконання. Однак, в більшості статично типізованих мов вираз
"a" + 1
— це не: вона не буде скомпільована не буде запущена. Це некоректний код, так само, як набір випадкових символів
!&%^@*&%^@*
— це некоректний код. Це додаткове поняття про коректність і некоректності не має еквівалента в динамічних мовами.
Сильна і слабка типізація
Поняття "сильний" і "слабкий" — дуже неоднозначні. Ось деякі приклади їх використання:
  • Іноді "сильний" означає "статичний".
    Тут все просто, але краще використовувати термін "статичний", тому що більшість використовують і розуміють його.
  • Іноді "сильний" означає "не робить неявне перетворення типів".
    Наприклад, JavaScript дозволяє написати
    "a" + 1
    , що можна назвати "слабкою типізацією". Але майже всі мови надають той чи інший рівень неявного перетворення, яке дозволяє автоматично переходити від цілих чисел до чисел з плаваючою комою на зразок
    1 + 1.1
    . У реальності, більшість людей використовують слово "сильний" для визначення межі між прийнятним і неприйнятним перетворенням. Немає якоїсь загальноприйнятої кордони, вони все неточні і залежать від думки конкретної людини.
  • Іноді "сильний" означає, що неможливо обійти суворі правила типізації в мові.
  • Іноді "сильний" означає безпечний для пам'яті (memory-safe).
    Сі — це приклад небезпечного для пам'яті мови. Якщо
    xs
    — це масив чотирьох чисел, то Сі з радістю виконає код
    xs[5]
    або
    xs[1000]
    , повертаючи якесь значення з пам'яті, яка знаходиться відразу за
    xs
    .
Давайте зупинимося. Ось як деякі мови відповідають цим визначенням. Як можна помітити, тільки Haskell послідовно "сильний" за всіма параметрами. Більшість мов не такі чіткі.








Мова Статичний? Неявні перетворення? Строгі правила? Безпечний для пам'яті? C Сильний Коли як Слабкий Слабкий Java Сильний Коли як Сильний Сильний Haskell Сильний Сильний Сильний Сильний Python Слабкий Коли як Слабкий Сильний JavaScript Слабкий Слабкий Слабкий Сильний
"Коли" у колонці "Неявні перетворення" означає, що поділ між сильним і слабким залежить від того, які перетворення ми вважаємо прийнятними).
Часто терміни "сильний" і "слабкий" відносяться до невизначеної комбінації різних визначень вище, і інших, не показаних тут визначень. Весь цей безлад робить слова "сильний" і "слабкий" практично безглуздими. Коли хочеться використовувати ці терміни, то краще описати, що конкретно мається на увазі. Наприклад, можна сказати, що "JavaScript повертає значення, коли складається рядок з числом, але Python повертає помилку". В такому випадку ми не будемо витрачати свої сили на спроби прийти до угоди про безліч значень слова "сильний". Або, ще гірше: прийдемо до недозволеному нерозуміння через термінології.
У більшості випадків терміни "сильний" і "слабкий" в інтернеті є неясними і погано певними думками конкретних людей. Вони використовуються, щоб назвати язик "поганим" або "гарним", і це думка обертається в технічний жаргон.
написав Кріс Сміт:
Сильна типізація: Система типів, яку я люблю і з якою мені комфортно.

Слабка типізація: Система типів, яка турбує мене або з якої мені не комфортно.
Поступова типізація (gradual typing)
Можна додати статичні типи динамічні мови? У деяких випадках — так. В інших це складно або неможливо. Сама очевидна проблема — це
eval
та інші схожі можливості динамічних мов. Виконання
1 + eval("2")
в Python дає 3. Але що дасть
1 + eval(read_from_the_network())
? Це залежить від того, що в мережі на момент виконання. Якщо отримаємо число, вираз коректно. Якщо рядок, то ні. Неможливо дізнатися до запуску, так що неможливо аналізувати тип статично.
Незадовільне рішення на практиці — це задати виразом
eval()
тип Any, що нагадує Object в деяких об'єктно-орієнтованих мовах програмування або інтерфейс
interface {}
в Go: це тип, якому задовольняє будь-яке значення.
Значення типу Any нічим не обмежені, так що зникає можливість системи типів допомагати нам в коді з eval. Мови, в яких є і
eval
і система типів, повинні відмовлятися від безпеки типів при кожному використанні
eval
.
У деяких мовах є опціональна або поступова типізація (gradual typing): вони динамічні за замовчуванням, але дозволяють додавати деякі статичні анотації. В Python нещодавно додали додаткові типи; TypeScript — це надбудова над JavaScript, у якому є додаткові типи; Flow виробляє статичний аналіз старого доброго коду на JavaScript.
Ці мови надають деякі переваги статичної типізації, але вони ніколи не дадуть абсолютної гарантії, як по-справжньому статичні мови. Деякі функції будуть статично типізованими, а деякі будуть динамічно типізованими. Програмісту завжди треба знати і остерігатися різниці.
Компіляція статично типізованого коду
Коли відбувається компіляція статично типізованого коду, спочатку перевіряється синтаксис, як і в будь компіляторі. Потім перевіряються типи. Це означає, що статичний мову спочатку може поскаржитися на одну синтаксичну помилку, а після її виправлення поскаржитися на 100 помилок типізації. Виправлення синтаксичної помилки не створило ці 100 помилок типізації. Компілятор просто не мав можливості виявити помилки типів, поки не був виправлений синтаксис.
Компілятори статичних мов можуть генерувати більш швидкий код, що компілятори динамічних. Наприклад, якщо компілятор знає, що функція add приймає цілі числа, то він може використовувати нативну інструкцію ADD центрального процесора. Динамічний мова буде перевіряти тип при виконанні, вибираючи один з безлічі функцій add залежно від типів (складаємо integers або floats або склеюємо рядка або, може бути, списки?) Чи потрібно вирішити, що сталася помилка і типи не відповідають один одному. Всі ці перевірки займають час. У динамічних мови використовуються різні трюки для оптимізації, наприклад JIT-компіляція (just-in-time), де код перекомпилируется при виконанні після отримання всієї необхідної про типи інформації. Однак, ніякої динамічний мова не може зрівнятися за швидкістю з акуратно написаним статичним кодом на мові начебто Rust.
Аргументи на користь статичних і динамічних типів
Прихильники статичної системи типів вказують на те, що без системи типів прості помилки можуть привести до проблем в продакшені. Це, звичайно ж, правда. Будь-хто, хто використовував динамічний мову, відчув це на собі.
Прихильники динамічних мов вказують на те, що на таких мовах, здається, легше писати код. Це, безумовно, справедливо для деяких видів коду, який ми час від часу пишемо, як, наприклад, той код
eval
. Це спірне рішення для регулярної роботи, і тут має сенс згадати невизначене слово "легко". Річ Хікі відмінно розповів про слово "легко", і його зв'язок зі словом "просто". Подивившись цей доповідь ви зрозумієте, що не легко правильно використовувати слово "легко". Остерігайтеся "легкості".
Плюси і мінуси статичних і динамічних систем типізації все ще погано вивчені, але вони безумовно залежать від мови і конкретної розв'язуваної задачі.
JavaScript намагається продовжити роботу, навіть якщо це означає безглузду конвертацію (зразок
"a" + 1
, що дає "a1"). Python у свою чергу намагається бути консервативним і часто повертає помилки, як у випадку з
"a" + 1
.
Існують різні підходи з різними рівнями безпеки, але Python і JavaScript обидва є динамічно типізованими мовами.
Сі з радістю дозволить програмісту вважати дані з будь-якого місця в пам'яті, або уявити, що значення одного типу володіє іншим типом, навіть якщо це не має ніякого сенсу і призведе до падіння програми.
Haskell ж не дозволить скласти integer і float без явного перетворення перед цим. Сі та Haskell обидва є статично типізованими, не дивлячись на такі великі відмінності.
Є безліч варіацій динамічних і статичних мов. Будь беззастережне висловлювання виду "статичні мови краще, ніж динамічні, коли справа стосується Х" — це майже гарантовано дурниця. Це може бути правдою в разі конкретних мов, але тоді краще сказати "Haskell краще, ніж Python коли справа стосується Х".
Різноманітність статичних систем типізації
Давайте поглянемо на два знаменитих прикладу статично типізованих мов: Go і Haskell. В системі типізації Go немає узагальнених типів, типів з "параметрами" від інших типів. Наприклад, можна створити свій тип для списків MyList, який може зберігати будь-які потрібні нам дані. Ми хочемо мати можливість створювати MyList цілих чисел, MyList рядків і так далі, не змінюючи вихідний код MyList. Компілятор повинен стежити за типізацією: якщо є MyList цілих чисел, і ми випадково додаємо туди рядок, то компілятор повинен відхилити програму.
Go спеціально був спроектований таким чином, щоб неможливо було ставити типи начебто MyList. Найкраще, що можливо зробити, це створити MyList "порожніх інтерфейсів": MyList може містити об'єкти, але компілятор просто не знає їх тип. Коли ми дістаємо об'єкти з MyList, нам потрібно повідомити компілятору їх тип. Якщо ми говоримо "Я дістаю рядок", але в реальності значення — це число, то буде помилка виконання, як у випадку з динамічними мовами.
Go також немає безлічі інших можливостей, які присутні в сучасних статично типізованих мовах (або навіть в деяких системах 1970-х років). У творців Go були свої причини для цих рішень, але думку людей з цього приводу іноді може звучати різко.
Тепер давайте порівняємо з Haskell, який володіє дуже потужною системою типів. Якщо задати тип MyList, то тип "списку чисел" це просто
MyList Integer
. Haskell не дасть нам випадково додати рядок в списку, і впевнитися, що ми не покладемо елемент зі списку в строкову змінну.
Haskell може виражати набагато більш складні ідеї безпосередньо типами. Наприклад,
Num a => MyList a
означає "MyList значень, які відносяться до одного типу чисел". Це може бути список integer'ів, float'ів або десяткових чисел з фіксованою точністю, але це точно ніколи не буде списком рядків, що перевіряється при компіляції.
Можна написати функцію add, яка працює з будь-якими численними типами. У цієї функції буде тип
Num a => (a -> a -> a)
. Це означає:
  • a
    може бути будь-яким числовим типом (
    Num a =>
    ).
  • Функція приймає два аргументи типу
    a
    повертає тип
    a
    (
    a -> a -> a
    ).
Останній приклад. Якщо тип функції
String -> String
, то вона приймає рядок і повертає рядок. Але якщо це
String -> IO String
, то вона також робить якийсь введення/виведення. Це може бути звернення до диска, мережі, читання з терміналу і так далі.
Якщо у функції типу ні IO, то ми знаємо, що вона не робить ніяких операцій вводу/виводу. У веб-додатку, наприклад, можна зрозуміти, змінює функція бази даних, просто глянувши на її тип. Ніякі динамічні і майже ніякі статичні мови не способи на таке. Це особливість мов з самою потужною системою типізації.
У більшості мов нам довелося б розбиратися з функцією й усіма функціями, які звідти викликаються, і так далі, у спробах знайти щось, що змінює базу даних. Це виснажливий процес, в якому легко допустити помилку. А система типів Haskell може відповісти на це питання просто і гарантовано.
Порівняйте цю потужність з Go, який не здатний висловити просту ідею MyList, не кажучи вже про "функції, яка приймає два аргументи, і вони обидва чисельні і одного типу, і яка робить введення/виведення".
Підхід Go спрощує написання інструментів для програмування Go (зокрема, реалізація компілятора може бути простою). До того ж, потрібно вивчити менше концепцій. Як ці переваги порівнянні зі значними обмеженнями — суб'єктивне питання. Однак, не можна посперечатися, що Haskell складніше вивчити, чим Go, і що система типів в Haskell набагато могутніше, і що Haskell може запобігти набагато більше типів помилок при компіляції.
Go і Haskell настільки різні мови, що їх групування в один клас "статичних мов" може вводити в оману, не дивлячись на те, що термін використовується коректно. Якщо порівнювати практичні переваги безпеки, то Go ближче до динамічних мов, ніж до Haskell'у.
З іншого боку, деякі динамічні мови безпечніше, ніж деякі статичні мови. (Python в цілому вважається набагато безпечніше, ніж Сі). Коли хочеться робити узагальнення щодо статичних або динамічних мови як групах, то не забувайте про величезній кількості відмінностей між мовами.
Конкретні приклади відмінності в можливостях систем типізації
У більш потужних системах типізації можна вказати обмеження на більш дрібних рівнях. Ось кілька прикладів, але не зациклюйтеся на них, якщо синтаксис незрозумілий.
Go можна сказати "функція add приймає два integer'а та повертає integer":
func add(int x, int y) int {
return x + y
}

В Haskell можна сказати "функція приймає будь чисельний тип і повертає число типу":
f :: Num => a -> a -> a
add x y = x + y

У Idris можна сказати "функція приймає два integer'а та повертає ціле число, але перший аргумент повинен бути менше другого аргументу":
add : (x : Nat) -> (y : Nat) -> {auto smaller : LT x y} -> Nat
add x y = x + y

Якщо спробувати викликати функцію
add 2 1
, де перший аргумент більше другого, то компілятор відхилить програму під час компіляції. Неможливо написати програму, де перший аргумент більше другого. Рідкісний мова володіє такою можливістю. У більшості мов така перевірка відбувається при виконанні: ми б написали щось на зразок
if $ x >= y: raise SomeError()
.
В Haskell немає еквівалента такого типу як у прикладі з Idris вище, а в Go немає еквіваленту наприклад, Haskell, ні прикладу з Idris. У підсумку, Idris може запобігти безліч багів, які не зможе запобігти Haskell, а Haskell зможе запобігти безліч багів, які не помітить Go. В обох випадках необхідні додаткові можливості системи типізації, які зроблять мову більш складним.
Системи типізації деяких статичних мов
Ось приблизний список систем типізації деяких мов у порядку зростання потужності. Цей список дасть вам загальне уявлення про потужності систем, не потрібно ставитися до нього як до абсолютної правди. Зібрані в одну групу мови можуть сильно відрізнятися один від одного. В кожній системі типізації є свої заморочки, і більшість з них дуже складні.
  • C (1972), Go (2009): Ці системи зовсім не потужні, без підтримки узагальнених типів. Неможливо визначити тип MyList, який би означав "список цілих чисел", "список рядків" і т. д. Замість цього доведеться робити "список непозначених значень". Програміст повинен вручну повідомляти "це список рядків" кожен раз, коли рядок видаляється зі списку, і це може призвести до помилки під час виконання.
  • Java (1995), C# (2000): Обидві мови підтримують узагальнені типи, так що можна сказати
    MyList<String>
    і отримати список рядків, про який компілятор знає і може стежити за дотриманням правил типів. Елементи списку будуть володіти типу String, компілятор буде форсувати правила при компіляції як зазвичай, так що помилки при виконанні менш вірогідні.
  • Haskell (1990), Rust (2010), Swift (2014): Всі ці мови мають декількома просунутими можливостями, в тому числі узагальненими типами, алгебраїчними типами даних (ADTs), і класами типів або чимось схожим (типи класів, ознаки (traits) і протоколи, відповідно). Rust і Swift більш популярні, ніж Haskell, і їх просувають великі організації (Mozilla і Apple, відповідно).
  • Agda (2007), Idris (2011): Ці мови підтримують залежні типи, дозволяючи створювати типи на кшталт "функція, яка приймає два цілих числа х і y, де y більше, ніж x". Навіть обмеження "y більше, ніж x" форсується при компіляції. При виконанні y ніколи не буде менше або дорівнює x, що б не трапилося. Дуже тонкі, але важливі властивості системи можуть бути перевірені статично в цих мовах. Їх вивчає дуже мало програмістів, але ці мови викликають у них величезний ентузіазм.
Спостерігається явне рух в бік більш потужних систем типізації, особливо якщо судити по популярності мов, а не з простого факту існування мов. Відомий виняток — це Go, який пояснює, чому багато прихильників статичних мов вважають його кроком назад.
Група два (Java і C#) — це мэйнстримовые мови, зрілі і широко використовуються.
Група три знаходиться на порозі входу в мейнстрім, з великою підтримкою з боку Mozilla (Rust) і Apple (Swift).
Група чотири (Idris and Agda) далекі від мейнстріму, але це може змінитися з часом. Мови три групи були далеко від мейнстріму ще десять років тому.
Джерело: Хабрахабр

0 коментарів

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