Огляд мови Idris

Agda is too mainstream!
 «Передбачення» image
 (джерело )
 
Матеріалів про мову Idris російською практично немає, спробую це виправити коротким оглядом. Також постараюся зробити текст зрозумілим для початківців, які не-функціональних і незнайомих з залежними типами програмістів, і тому тим, хто знайомий з подібними мовами, може бути простіше відмотати в кінець або відразу прочитати офіційну документацію. Писати серйозне введення в мову і теорію не беруся, але сподіваюся показати, про що це взагалі.
 
Отже, Idris — чистий функціональний мова програмування загального призначення з залежними типами.
 
 

Навіщо це?

Для короткої відповіді підійде відома цитата Дейкстри; хоча підхід і змінився з тих пір, мета залишилася та ж:
 
Глибоко помиляється той, хто думає, що виробами програмістів є програми, які вони пишуть. Програміст зобов'язаний створювати заслуговують довіри рішення і представляти їх у формі переконливих доводів, а текст написаної програми є лише супровідним матеріалом, до якого ці докази застосовні.
Якщо ж бути точнішим, то причин для створення і використання може бути декілька: автор, Edwin Brady, використовує його для дослідження прикладного програмування з залежними типами; багатьом, як і мені, подобається можливість складання точних специфікацій програм; також я сподіваюся на значне скорочення часу налагодження прикладних програм за допомогою формальної верифікації оних. І тут напрошується другий цитата:
 
Тестування програми може дуже ефективно продемонструвати наявність помилок, але безнадійно неадекватно для демонстрації їх відсутності.
 
 

Статична типізація і залежні типи

Один із способів класифікації типізації мови програмування — поділ на статичну і динамічну. При динамічної типізації, типи невідомі під час компіляції, і тому не можуть бути перевірені; це допомагає писати програми швидше, але в той же час і додає клас помилок, пов'язаних з типізацією, які виявляються під час виконання програми, що зазвичай не дуже приємно. Idris використовує статичну типізацію, так що далі мова піде тільки про неї; але щоб не лякати людей, звиклих до динамічної типізації, відразу зауважу, що використовується також і висновок типів , тобто типи можна не вказувати явно, якщо вони очевидні компілятору з контексту.
 
Типізація може огранічіваеться декількома примітивними типами — наприклад, рядки, числа, числа з плаваючою комою; тоді все, що ми можемо «сказати» про тип деякого значення (наприклад, аргументу функції, або повертається нею значення) — «рядок» , «число» , «число з плаваючою комою» . Але зазвичай це доповнюється чимось на зразок структур: прості C-подібні структури, класи, (узагальнені) алгебраїчні типи даних і пр., і заодно синонімами типів (
typedef
в C,
type
в Haskell), що вже дозволяє «сказати», наприклад, «дата» , попередньо визначивши структуру, клас або тип «дата».
 
Можна доповнити це фразою «покажчик на» , що заодно дозволяє використовувати масиви, але в високорівневих мовах частіше підтримується узагальнене програмування (шаблони в C + +, generics в Java), що вже дозволяє будувати для опису типів фрази виду «список дат », « граф доріг », « дерево подій ». Іншими словами, типи можуть бути параметризовані іншими типами.
 
І, нарешті, можна параметризовані типи значеннями, що дає можливість сказати «список, що складається з п'яти рядків» , «повідомлення, підписане Василем» ; типи функцій тоді можуть приймати вид «функція, що приймає повідомлення, підписане деяким користувачем, і повертає дані цього користувача» , замість більш поширеного «функція, що приймає повідомлення і повертає дані користувача» , що веде до набагато більш точним специфікаціям. Більш того, це дає можливість, так би мовити, перейти від підлягають до присудком, використовувати принцип «висловлювання як типи»: «5 більше 3» , «невірно, що 5 більше 3» , «7 є простим числом» , «Василь отримав 2 повідомлення» . Це і є залежні типи , які реалізовані в Idris, як, втім, і в кількох інших мовах (Agda, Coq, Epigram і т.д.), але від них Idris відрізняє прагнення бути сучасним прикладним мовою.
 
Також це, в умовах total functional programming, дозволяє користуватися відповідністю між комп'ютерними програмами та математичними доказами (відповідністю Каррі — Ховарда ): типом функції може бути, наприклад, «А менше Б, Б менше У, значить А менше В» або «повідомлення надіслано деякого користувачеві, значить даному користувачеві доступно дане повідомлення» ; доказом тоді стає тіло функції, яке просто має повернути значення заданого типу, а перевірка докази — це і є перевірка типів.
 
 

Total functional programming

Як було сказано, Idris — чистий функціональний мова . Але також підтримується опциональное вимога властивості totality функцій, під яким мається на увазі дві властивості:
 
 
     
Визначеність всюди: функція повинна бути визначена для будь-яких вхідних даних. У чистих мовах відсутність цієї властивості — чи не єдина можливість для програми «впасти» (інші — IO, зокрема вбивство процесу системою внаслідок якихось його дій, і можливі баги компілятора).
 Сувора нормалізація: при рекурсивних викликах функції, хоча б один з її аргументів повинен строго зменшуватися (структурно), або функція повинна бути продуктивна на кожній ітерації — тобто повертати якусь частину результату, і обіцянка прорахувати наступну ітерацію. У першому випадку це гарантує завершаемості функції, обходячи проблему зупинки, а в другому — можливість вважати кінцевий префікс будь-якої довжини за кінцевий час.
 
Важливо це, в першу чергу, для побудови доказів, а й коректності звичайних програм йде на користь, судячи з моїми спостереженнями. До слова, наявністю цієї властивості гарантується, що результат ледачих і жадібних обчислень даної функції буде однаковий, а обчислення в Idris за замовчуванням жадібні, але будь-який аргумент можна зробити ледачим.
 
Включати цю опцію можна для окремих функцій, для файлів, або прапором компілятора.
 
 

Приклади

Незвичний синтаксис, схоже, сильно відволікає увагу від суті описуваного, і тому описувати синтаксис Не буду; приклади коду наводяться для людей, знайомих з мовами сімейства ML, а для інших приводяться текстові описи перед цими прикладами.
 
 
Ділення
Знайома всім операція, яка є практично у всіх мовах програмування (або в їх стандартних бібліотеках) — розподіл. Але поділ на 0 заборонено, що веде до різних спірних рішень:
 
     
Повернути небудь спеціальне, начебто Infinity: тоді ми повинні визначити і правила для роботи всіх інших функцій / операцій з Infinity, що ускладнює арифметику в цілому, але, наприклад, проста властивість a / b = c → b * c = a буде загублено, і далі спроба його використання запросто призведе до результатів, відмінним від очікуваних.
 Породити виняток: це не тільки призводить до порушення нормального потоку виконання програми, заодно знову-таки створюючи грунт для багів при неспійманих винятках, а й значно ускладнює міркування (зокрема, формальне) про функції, якщо не робить його неможливим.
 Обернуть результат в Maybe , повертаючи Nothing при спробі поділу на 0: чомусь краще попередніх двох, хіба що сама функція не стимулюватиме програміста писати коректні програми, а формули можуть стати менш акуратними та / або надміру насиченими теорією категорій, попутно утруднюючи міркування про функції, що використовують таку реалізацію поділу.
 
 
У мовах з залежними типами, і в Idris зокрема, з'являється ще один варіант: заборонити ділення на 0. Іншими словами, розподіл на 0 заборонено — і ми просто робимо його неможливим; тип функції тоді описується як «функція, що приймає два числа, другий з яких не дорівнює 0, і повертає число». При бажанні, можна доповнити цю специфікацію властивістю, що говорять про зв'язок значення, що повертається з аргументами функції, тобто "… Таке, що ...", але простіше це залишити для окремих теорем, а поки повернемося до опису типу функції розподілу: до звичайних двох аргументів, нам потрібно додати третій — доказ того, що другий аргумент не дорівнює нулю.
 
Тепер розглянемо три випадки використання поділу (нагадаю, що мова йде про час компіляції):
 
 
     
Дільник відомий: доказ тривіально, оскільки еквівалентність натуральних чисел можна залагодити (іншими словами, компілятор сам бачить, дорівнює дільник нулю чи ні), і тому ми можемо, при бажанні, обернути таку функцію поділу в функцію зі звичайними двома аргументами, підставляйте один і той же простий третій аргумент.
 Дільник невідомий, але про нього відомо щось, що дозволяє переконатися в тому, що він не дорівнює нулю: наприклад, що він більше деякого невід'ємного числа. Тоді потрібно або написати доказ на місці, або скористатися функцією, що приймає те, що у нас є (доказ того, що число більше деякого невід'ємного числа), і повертає те, що нам потрібно (доказ того, що це число не дорівнює нулю). Такі функції можна називати як просто функціями, так і лемами або теоремами, але, як уже було згадано, в даному контексті це одне і те ж.
 Ми самі не впевнені в тому, що дільник нічого очікувати дорівнює нулю (після уважного розгляду ситуації в спробі довести нерівність, попередній випадок може переходити в цей): тільки в цьому випадку нам дійсно потрібно ввести перевірку перед поділом; якщо дільник дорівнює нулю, то використовувати альтернативне рішення, а в іншому випадку — скористатися отриманою інформацією і виконати поділ.
 
 
Такий підхід, звичайно, необов'язковий і в Idris, але змушує програміста переконатися в тому, що він виконує розрахунки коректно.
 
І, нарешті, приклад коду — каркас для функції розподілу:
 
 
-- (total) функция деления для натуральных чисел
-- "==" - функция проверки разрешимой эквивалентности, возвращающая Bool
-- "=" - эквивалентность высказываний, тип
total div : (n, m: Nat) -> ((m == Z) = False) -> Nat
-- деление на 0 - невозможно; просто показываем это компилятору
-- с тем же успехом, впрочем, можно и вернуть любое число
div n Z f = FalseElim $ trueNotFalse f
-- деление на положительное число
div n (S k) f = {-todo-}?div_rhs

 
Оскільки це тільки каркас, тут використана мета-змінна,
div_rhs
; людям, знайомим з Agda, вже знайомі «дірки» (holes), більш слабкою версією яких мета-змінні в Idris є, а для інших поясню: Idris дозволяє подивитися її контекст (змінні, які видно з її позиції) і мета (що має бути сконструйоване / повернуто з даної позиції), що помітно полегшує написання як доказів, так і програм. Ось так він виглядає в даному випадку:
 
 
n : Nat
  k : Nat
  f : S k == 0 = False
--------------------------------------
div_rhs : Nat

 
Також є можливість заповнювати їх напів-автоматично: маючи мету повернути
Nat
, можна скористатися командою (REPL / IDE) «refine», передавши їй, наприклад, ім'я функції
plus
, і якщо функція
plus
в змозі повернути значення необхідного типу, то вона буде підставлена замість цієї мета-змінної, а для її аргументів буде підставлено дві нових предмети. Процес це той же, який використовується і для іншої функції — повністю автоматичної заміни мета-змінних, тобто пошуком докази: у деяких випадках необхідне доказ може бути знайдено автоматично.
 
Типи (трохи підредагувати для читабельності):
 
 
λΠ> :t div
div : Nat -> (m : Nat) -> (m == 0 = False) -> Nat

 
λΠ> :t div 1 2
div 1 2 : (2 == 0 = False) -> Nat

 
λΠ> :t div 1 2 refl
div 1 2 refl : Nat

 
λΠ> :t div 1 0 refl
(ошибка, программа с подобным вызовом не пройдёт проверку типов)

 
Тепер відвернемося від реалізації функції розподілу і подивимося, що такий підхід нам дає. Почнемо з вищезгаданої коректності: функція працює саме так, як повинна. Ми можемо думати про функції так, як зазвичай думаємо про те, що нею реалізується (арифметична дія, в даному випадку: ми не можемо ділити на нуль, але в процесі розподілу ніякі концепції зразок винятків не беруть участь, а результатом є число). Можемо міркувати про функції так само, як про саму представляється нею концепції, в тому числі і формально, тобто записуючи міркування кодом. У функціях, що використовують її, міркування і висновки тепер можуть переплітатися з обчисленнями і бути перевірені, а не залишатися в голові програміста або текстових коментарях. І програма стає конструкцією з коректних міркувань і рішень, а не просто рецептом для обчислень.
 
 
Списки
Робота зі списками (або масивами) — ще одна часта завдання, що приводить приблизно до того ж набору спірних рішень і наступних помилок. Зокрема, розглянемо функцію, що повертає енний елемент списку: проблема при її реалізації полягає в тому, що ми можемо запросити елемент з позиції, якої немає в списку. Звичайні рішення — падати з «access violation» або «segmentation fault», породжувати виняток (і, можливо, потім падати з ним), використовувати Maybe.
 
У мовах з залежними типами з'являється ще пара можливих рішень. Перше — аналогічно рішенню проблеми поділу на нуль, тобто останнім аргументом функції стає доказ того, що запитувана позиція менше довжини списку.
 
Тут можна помітити, що різні числа, списки, «if-then-else» і т.п. визначаються на самій мові. Натуральні числа, реалізовані в бібліотеці, замінюються на GMP числа при компіляції в C, а такі функції, як додавання і множення — на відповідні функції GMP, що дає і швидкі розрахунки в скомпільованих програмах, і можливість міркувати про них. Тепер поглянемо на код:
 
 
data Nat = Z | S Nat
data List a = Nil | (::) a (List a)

length : List a -> Nat
length []      = 0
length (x::xs) = 1 + length xs

index : (n : Nat) -> (l : List a) -> (ok : lt n (length l) = True) -> a
index Z     (x::xs) p    = x
index (S n) (x::xs) p    = index n xs ?indexTailProof
index _     []      refl   impossible

indexTailProof = proof {
  intros;
  rewrite sym p;
  trivial;
}

 
 
indexTailProof
— доказ з використанням тактик, в стилі Coq, але можна (і мені чимось більше подобається) писати їх і в стилі Agda, тобто більш звичними функціями (кажуть, правда, що скоро тактики будуть і в Agda).
 
Друге рішення — використовувати не просто список, а список фіксованої довжини: вектор, як його називають у контексті мов з залежними типами. Приклад був згаданий вище: це те, що дозволяє сказати «список з п'яти рядків». Також нам може допомогти т.зв. кінцевий тип — тобто тип, кількість різних значень якого звичайно: можемо розглядати його як той же тип натуральних чисел, але з верхньою межею. Зручний цей тип зокрема тим, що з ним простіше сказати «число, менше n», ніж з натуральними числами, де це швидше «число, і воно менше n». Тип функції отримання енної елемента вектора тоді читається як «функція, що приймає число, менше ніж n, і список з n елементів типу a, і повертає елемент типу a».
 
У такому випадку, завданням стає надати доказ, а сконструювати число потрібного типу (тобто менша, ніж n). До слова, логіка в доказах тут відрізняється від класичної (є интуиционистской), і полягає в конструюванні доказів, тобто доказом висловлювання / типу є будь-яке значення даного типу, так що деяку схожість з попереднім підходом простежити можна, але в той же час підхід до написання програми в цілому це змінює.
 
Код:
 
 
data Fin : (n : Nat) -> Type where
    fZ : Fin (S k)
    fS : Fin k -> Fin (S k)

data Vect : Nat -> Type -> Type where
  Nil  : Vect Z a
  (::) : (x : a) -> (xs : Vect n a) -> Vect (S n) a

index : Fin n -> Vect n a -> a
index fZ     (x::xs) = x
index (fS k) (x::xs) = index k xs
-- запросить что-либо из пустого вектора невозможно, в данном случае
-- компилятор это "видит" сам
index fZ     [] impossible

 
Так ми йдемо ще далі від явних доказів, але будуємо, тим не менш, коректні програми.
 
Ну а якщо вже дісталися до векторів, то ось і функція їх об'єднання, часто приводиться в приклад для демонстрації залежних типів:
 
 
(++) : Vect m a -> Vect n a -> Vect (m + n) a
(++) []      ys = ys
(++) (x::xs) ys = x :: xs ++ ys

 
Тіло той же, що і для звичайних списків, але тип поцікавіше: зверніть увагу на
m + n
.
 
 

Приклади побільше

Вище наведені приклади окремих невеликих функцій, які Idris допомагає зробити коректними, але ось кілька більших речей навскидку:
 
 
     
Протоколи: є бібліотека Protocols , що дозволяє описувати протоколи з використанням DSL, а потім реалізовувати їх; невідповідність реалізації опису протоколу призведе до помилки.
 Фізика і гри : не тільки підтримується коректність обчислень, але й корисно доводити теореми вже після написання основних програм.
 Закони функторів, аплікативного функторів і монад можуть бути включені в код , в самі тайпкласси.
 Криптографія : очевидний приклад того, коректність чого важлива.
 Розбір і складання текстових / бінарних форматів: можливо формально доведено, що будь-які складені рядки розбираються у вихідні дані, а розібрані дані — складаються в вихідні рядка. Приблизно це я і вибрав в якості першого проекту на Idris.
 Системи прав доступу, бази даних, драйвери пристроїв — реалізацій на Idris поки не бачив, але теж речі, які хочеться бачити надійними.
 
 
Пишеться на ньому і веб-фреймворк , і бібліотека для взаємодії з DOM (до речі, на момент написання статті компілятор підтримує компіляцію в C, LLVM, Java і JavaScript), і всілякі парсери (раз , два ), і на системне програмування він націлений. Переписуються програми з Haskell на Idris досить просто.
 
Не використовується Idris поки на виробництві — принаймні, широко (чув, що в Potsdam Institute for Climate Impact Research він активно використовується, але це, можливо, не зовсім те, що зазвичай розуміється під виробництвом). Основна технічна перешкода — «необкатанность», яка повинна зважитися «обкативаніем».

Висновок

Мова це новий, і тому «сирий», але сучасний, що використовує сучасну теорію і накопичену іншими мовами практику.

Дозволивши собі трохи помріяти про майбутнє використання Idris (і мов, які з'являться після нього), можна уявити, крім загального підвищення надійності програм, технічні завдання, супроводжувані формальними специфікаціями або навіть складаються з них; зростання сервісів на зразок Proof Market ; бібліотеки фізичних, математичних, та й будь-яких інших теорій, і мов на зразок Lojban; статті та книги як списки формальних специфікацій доведених теорем; спілкування, вибудовується з автоматично перевіряються реплік і пар питання-відповідь зокрема.

Посилання та книги по темі

Офіційний сайт з документацією та посиланнями;
github wiki ;
скрінкаст з використанням idris-mode (є, до речі, і idris-vim );
Software Foundations — гарне введення в мови з залежними типами, але використовує Coq;
Type Theory and Functional Programming — опис теорії, що лежить в основі подібних мов;
TaPL, книги з Haskell і документація Agda можуть доповнити картину.


P.S.

Дякуємо тим, на кому цей огляд тестувався, за їх коментарі та ідеї.

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

0 коментарів

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