Мультивсесвіт C# — сингулярність мови програмування

💡 Усі статті, обговорення, новини про .NET — в одному місці. Приєднуйтесь до .NET спільноти!

Своє знайомство з .NET і C# я почав приблизно у 2007 році. Я тоді навчався на 4 курсі і на той момент вже мав досвід роботи з мовами програмування C++ і Delphi. До того ж у мене був навіть комерційний продукт, написаний на Visual C++, який цілком непогано працював.

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

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

Від редакції: стаття публікується в перекладі українською мовою зі згоди та за узгодження з автором, оригінал тексту можна прочитати тут.

Передісторія

Спочатку нам доведеться повернутися в часі приблизно на 20 років. Саме у 2003 році, у надрах Microsoft Research (це дослідницький підрозділ корпорації Microsoft, практично секретна лабораторія) розпочали роботу над проєктом Singularity — високонадійною операційною системою, в якій мікроядро, драйвери пристроїв та програми написані на керованому коді.

У статті «Singularity: Rethinking the Software Stack» співробітники Microsoft Research Джеймс Ларус і Гален Хант пишуть про Singularity так:

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

Наша мова програмування Sing# є розширенням C#, що забезпечує підтримку комунікаційних примітивів ОС, а також підтримку системного програмування та факторизації коду».

Історія створення операційної системи Singularity неймовірно цікава і заслуговує на окрему статтю. Але в цьому випадку мене зацікавила фраза «наша мова програмування Sing#». Я ніколи раніше не чув про таку мову програмування і мені стало цікаво дізнатися про неї більше. Стаття у «Вікіпедії» про цю мову виявилася дуже короткою і була представлена ​​лише у двох мовних версіях — російській та німецькій. Попри малий обсяг інформації, там виявилося дещо цікаве — у картці опису мови вказувалося, що на Sing# вплинула ще одна, невідома мені досі мова — Spec#. Виходить, що у нас вже є два відгалуження від C#.

Оскільки Spec# є основою для Sing#, то шукати детальнішу інформацію я почав з неї. Команда Microsoft Research так характеризує цю мову:

«Spec# — це формальна мова для контрактів API, яка розширює C# конструкціями для ненульових типів, передумов, постумов та інваріантів об’єктів.»

Про Sing#, згідно з публікацією «An Overview of the Singularity Project», зазначено таке:

«Sing# є розширенням мови Spec#, розробленої в Microsoft Research. Sing# розширює цю мову підтримкою каналів та низькорівневих конструкцій, необхідних для системного коду.»

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

Вивчати статті та публікації можна досить довго — поки що я зміг прочитати (а скоріше навіть переглянути) лише малу частину з цих матеріалів. У процесі ознайомлення зі статтями мені стало цікаво: а чи мови з «паралельних реальностей» вплинули на C# і .NET, якими ми їх знаємо сьогодні?

Провівши невелике дослідження, я виявив, що цей вплив безумовно є. Хоча і Sing#, і Spec# не отримали подальшого розвитку, успішні ідеї справді були згодом запроваджені в C# — якісь раніше, якісь пізніше.

На сьогодні ми точно можемо зробити висновок, що низка концепцій була реалізована під час роботи над експериментальними інкарнаціями мови:

• Code Contracts;
• Non-null reference types;
• readonly / pure methods.

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

Code Contracts

Проєкт Code Contracts є відгалуженням Spec# і забезпечує спосіб визначення передумов, постумов та інваріантів об’єктів у коді:

• передумови є вимогами, які мають бути виконані при вході в метод або властивість;
• постумови описують очікування на момент завершення роботи коду методу чи властивості;
• інваріанти об’єкта описують очікуваний стан класу, що перебуває в нормальному стані.

Переваги, які пропонує використання Code Contracts:

• поліпшене тестування: перевірка контрактів на етапах як компіляції, так і виконання;
• інструменти автоматичного тестування: Code Contracts можуть використовуватися для генерації краще осмислених тестів, відфільтровуючи аргументи тесту, які не задовольняють передумов;
• статична перевірка: статичний аналізатор може визначити порушення контрактів без запуску програми. Він перевіряє неявні контракти, такі як нульові посилання та межі масиву та явні контракти;
• довідкова документація: генератор документації доповнює наявні файли документації інформацією про контракти.

Зазначу, що на сьогодні Code Contracts вже не підтримуються в .NET 5 і новіших версіях платформи, тепер замість них пропонується звернути увагу на використання nullable reference types.

Якщо ми подивимося на специфікацію Spec#, то побачимо таке визначення:

«Одним з основних елементів специфікації в Spec# є метод. Кожен метод може включати передумову, яка описує умови, за яких виклик метода дозволений, і постумову, яка визначає умови, за яких повернення метода дозволене. Отже, реалізація метода може припускати, що передумова дотримується при вході, і метод, що викликається, може припускати, що постумова дотримується при поверненні. Цю угоду між методами, що викликаються, і реалізацією, часто називають контрактом метода.»

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

Non-null reference types

У восьмій версії мови C# Microsoft запровадила поняття non-nullable references, які дозволяють розробнику гарантувати, що тип посилання не може бути нульовим. Це досягається завдяки перевіркам на етапі компіляції, що своєю чергою дозволяє створювати простіші та надійніші програми.

Концепція non-null reference types також сягає своїм корінням в Spec#, як і концепція Code Contracts. У Spec# оголошення non-null reference виглядало так:

class Student : Person {
    Transcript! t;
    public Student(string name, EnrollmentInfo! ei)
       : base(name) {
        t = new Transcript(ei); 
    }
    ...
}

Варто зазначити, що Ентоні Хоар, один з творців мови програмування ALGOL W, заявляє, що концепцію null reference запропонував саме він. І сьогодні він вважає, що це була «помилка на мільярд доларів»:

«Я називаю це своєю помилкою на мільярд доларів. Це був винахід нульового посилання у 1965 році. На той час я розробляв першу комплексну систему типів посилань в об’єктноорієнтованій мові (ALGOL W). Моя мета полягала в тому, щоб гарантувати, що будь-яке використання посилань має бути абсолютно безпечним, з автоматичною перевіркою компілятором. Але я не міг устояти перед спокусою вказати нульове посилання просто тому, що це було так легко реалізувати. Це призвело до незліченних помилок, уразливостей та системних збоїв, які, ймовірно, завдали мільярдів доларів збитків за останні 40 років.»

Думаю, що з Тоні погодяться всі розробники, кому хоч раз доводилося мати справу з null pointer exception.

«Щоб зробити використання non-null типів ще зручнішим для програмістів, які переходять на Spec# із C#, Spec# передбачає виведення non-nullity для локальних змінних. Це виведення виконується у вигляді аналізу потоку даних компілятором Spec#.» (звідси)

readonly / pure methods

У дев’ятій версії мови C# було реалізовано можливість оголошення структур лише для читання — readonly struct. Структура, оголошена з ключовим словом readonly гарантує, що жоден з її елементів не змінить стан структури. При цьому ключове слово readonly може застосовуватися як до всієї структури, так і її окремих полів, або методів.

public readonly struct Coords
{
    public Coords(double x, double y)
    {
        X = x;
        Y = y;
    }

    public double X { get; init; }
    public double Y { get; init; }

    public override string ToString() => $"({X}, {Y})";
}

Така поведінка була реалізована в Sing# через атрибут Pure: метод (функція, що належить класу) називається чистим і оголошується таким атрибутом Pure у разі, якщо він повертає значення без зміни стану. Чисті методи не повинні мати побічних ефектів:

[Pure]
public int MagicNumber() {
  return 3 + gt.StringCount(); 
}

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

Висновки

Цілком припускаю, що список прикладів впливу Spec# і Sing# на C# далеко не повний і, ознайомившись з матеріалами уважніше, ніж я, ви знайдете й інші схожі концепції мов програмування. А щоб вам було простіше займатися дослідженнями, я додаю список корисних матеріалів:

• Using the Spec# Language, Methodology, and Tools to Write Bug-Free Programs
  
• The Spec# Programming System: An Overview
  
• Singularity: Rethinking the Software Stack
  
• An Overview of the Singularity Project
  
• Language Support for Fast and Reliable Message-based Communication in Singularity OS
  
• The Spec# Programming System: Challenges and Directions