Skip to content

Instantly share code, notes, and snippets.

@GoldsteinE

GoldsteinE/r2.md

Created February 24, 2021 16:19
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save GoldsteinE/e9897b7def4f0889db9a19fc9d942190 to your computer and use it in GitHub Desktop.
Save GoldsteinE/e9897b7def4f0889db9a19fc9d942190 to your computer and use it in GitHub Desktop.
Download ZIP
Языки программирования, про которые вы (возможно) не знали — выпуск 2
Raw
r2.md

Языки программирования, про которые вы (возможно) не знали — выпуск 2

Язык первый, практичный — Zig

Сайт: https://ziglang.org

Zig is a general-purpose programming language and toolchain for maintaining robust, optimal, and reusable software.

— Официальный сайт Zig

Summary

Zig — это одна из попыток сделать better C. Он быстрый как C и совместим с C-библиотеками без особой боли. Это простой, небольшой язык, с мощными возможностями в compile-time, обработкой ошибок без исключений, и быстрой компиляцией. Он не безопасный (можно легко разыменовать невалидный указатель), но предотвращает некоторые из частых проблем C.

Как выглядит?

const std = @import("std");

const Header = struct {
    magic: u32,
    name: []const u8,
};

pub fn main() void {
    printInfoAboutStruct(Header);
}

fn printInfoAboutStruct(comptime T: type) void {
    const info = @typeInfo(T);
    inline for (info.Struct.fields) |field| {
        std.debug.print(
            "{s} has a field called {s} with type {s}\n",
            .{
                @typeName(T),
                field.name,
                @typeName(field.field_type),
            },
        );
    }
}

Хайлайты

  • Zig — строго, статически типизированный язык. Компилируется в нативные бинарники или в WASM. Не поддерживает какого-либо рода полиморфизма: нет ни наследования, ни интерфейсов/трейтов. Вместо этого есть compile-time рефлексия, которая позволяет получить информацию о типе во время компиляции. Так, например, работает встроенная функция print():

      switch (@typeInfo(T)) {
      .ComptimeInt, .Int, .ComptimeFloat, .Float => {
          return formatValue(value, actual_fmt, options, writer);
      },
      .Void => {
          return formatBuf("void", options, writer);
      },
      .Bool => {
          return formatBuf(if (value) "true" else "false", options, writer);
      },
      ...
  }

  • Zig порождает статические (не завязанные даже на libc) бинарники. Компилятор Zig является также компилятором C, и тоже линкует программы с libc статически.

  • Дефолтного менеджера зависимостей нет, поэтому говорить про размер экосистемы довольно сложно.

  • В Zig крайне богатые возможности для исполнения кода во время компиляции. Почти любую Zig-функцию можно запустить на этапе компиляции с помощью ключевого слова comptime. Более того, функции могут принимать типы как значения. Таким образом, вместо специального синтаксиса для дженериков, в Zig есть просто функции, которые принимают тип и возвращают тип. Так, например, выглядит объявление встроенного типа ArrayList:

    pub fn ArrayList(comptime T: type) type {
    return ArrayListAligned(T, null);
}

  • Некоторые флаги оптимизации в Zig вынесены в ключевые слова: например, слово inline перед циклом указывает компилятору, что этот цикл следует размотать (unroll).

  • В Zig есть ADT. В отличие от большинства языков с ADT, требуется вручную поддерживать отдельно enum для тега и отдельно union для значений:

    const ComplexTypeTag = enum {
  ok,
  not_ok,
};
const ComplexType = union(ComplexTypeTag) {
    ok: u8,
    not_ok: void,
};

  • Обработка ошибок осуществляется с помощью специального типа error. Функция может вернуть error union, который содержит либо ошибку, либо успех. Несмотря на то, что в Zig есть ADT, error union — это специальный тип. Все ошибки с одинаковым названием равны: error.Abc это одно и то же значение в любой части программы. Максимальное количество разных ошибок в программе — 65535.

    Для обработки error unions есть специальный оператор catch, который позволяет предоставить альтернативное значение в случае ошибки (например, res catch 0 будет равно нулю, если res содержит ошибку) или код обработки. Сокращение try expr — синтаксический сахар для expr catch |err| return err.

    Ошибки сохраняют трейсбек по мере того, как их возвращают из функций.

  • Есть defer, как в Go, и более специфичный defererr, который выполняется только в том случае, если функция вернула ошибку.

  • Асинхронность в Zig бесцветная: весь IO становится асинхронным, если выставить глобальную переменную const io_mode = .evented. Кейворды async/await существуют, но работают не так, как в большинстве других языков — async отправляет некое вычисление в бэкграунд (возвращая хендлер), а await позволяет дождаться его выполнения.

    Более того, async/await всё ещё работают, даже если сами системные вызовы синхронные. Правда, для многих асинхронных программ перевод их в blocking-режим может породить дедлоки.

    Больше про асинхронность в Zig:

  • Все функции стандартной библиотеки, которые выделяют память, принимают аллокатор в явном виде и возвращают ошибки аллокации, если они происходят. Это может быть несколько вербозно, но зато спасает от проблем при использовании в системном коде, вроде тех, что возникли при интеграции Rust в curl.

  • Zig — не безопасный язык. Указатели не могут быть нулевыми, но Zig никак не проверяет, что объект, на который указывает указатель ещё жив, или вообще был аллоцирован.

Язык второй, исследовательский — Idris

Сайт: https://www.idris-lang.org

Idris is a programming language designed to encourage Type-Driven Development. In type-driven development, types are tools for constructing programs. We treat the type as the plan for a program, and use the compiler and type checker as our assistant, guiding us to a complete program that satisfies the type. The more expressive the type is that we give up front, the more confidence we can have that the resulting program will be correct.

— Официальный сайт Idris

Summary

Idris — один из немногих существующих языков, который предоставляет зависимые типы. Зависимые типы позволяют выразить зависимость между значением (термом) на входе у функции и типом на выходе. Например:

-- Мы определяем функцию, которая принимает значение типа `Bool` и возвращает тип
funcType : Bool -> Type
-- Пусть этим типом будет строка, если на входе было значение True
funcType True = String
-- И число, если на входе было False
funcType False = Int

-- Мы говорим, что `func` принимает два аргумента: значение типа `Bool` и значение
-- того типа, который получится, если функции `funcType` передать первый аргумент.
func : (b : Bool) -> (funcType b)
-- Как можно видеть, она возвращает разные типы значений в зависимости от своих аргументов
func True = "Hello!"
func False = 42

Это не то же самое, что comptime-функции в Zig: в отличие от comptime-функций, зависимые типы могут зависеть от значений, получаемых в рантайме (например, от пользователя). Первым аргументом функции func может быть значение, полученное с клавиатуры.

Помимо этого, у Idris есть довольно богатые возможности по формальной верификации кода.

Как выглядит?

Как Haskell, но с одинарными двоеточиями.

module BTree

public export
data BTree a = Leaf
             | Node (BTree a) a (BTree a)

export
insert : Ord a => a -> BTree a -> BTree a
insert x Leaf = Node Leaf x Leaf
insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)
                                   else (Node l v (insert x r))

export
toList : BTree a -> List a
toList Leaf = []
toList (Node l v r) = BTree.toList l ++ (v :: BTree.toList r)

export
toTree : Ord a => List a -> BTree a
toTree [] = Leaf
toTree (x :: xs) = insert x (toTree xs)

Если мы только не говорим про доказательство теорем.

helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))
helpEven j p = rewrite plusSuccRightSucc j j in p

helpOdd : (j : Nat) -> Parity (S (S (j + S j))) -> Parity (S (S (S (j + j))))
helpOdd j p = rewrite plusSuccRightSucc j j in p

parity : (n:Nat) -> Parity n
parity Z     = Even {n=Z}
parity (S Z) = Odd {n=Z}
parity (S (S k)) with (parity k)
  parity (S (S (j + j)))     | Even = helpEven j (Even {n = S j})
  parity (S (S (S (j + j)))) | Odd  = helpOdd j (Odd {n = S j})

Хайлайты

  • Idris умеет исполнять на уровне типов любую тотальную (т. е. ту, про которую компилятор может доказать, что она завершается (halt) функцию). Из этого очевидно, что система типов в Idris не Тьюринг-полная.

    Любую Idris-функцию можно пометить как тотальную с помощью аттрибута %total, или даже сделать это для всех функций с помощью %default total.

    Если функция в аннотации типа не тотальная (или Idris не может доказать, что она тотальная), компилятор просто оставит её неприменённой. Это можно увидеть, например, если заменить в примере из Summary Bool на String.

  • Idris — классический чисто функциональный язык вроде Haskell. Использует монады для IO.

  • Поддерживается полиморфизм через тайпклассы, которые здесь называются интерфейсами.

  • В отличие от Haskell, в Idris есть перегрузка функций.

  • Один из самых известных типов в Idris — это Vect n a. Вектор содержит в себе информацию не только о типе, лежащем внутри, но и о длине вектора, что позволяет проверять операции вроде обращения по индексу на этапе компиляции.

  • Тип натуральных чисел Nat определён как перечисление — это либо ноль (Z), либо число, следующее за другим натуральным числом n (S n). Это позволяет удобный паттерн-матчинг по натуральным числам: например, функция head, возвращающая первый элемент вектора, определена для Vect (S _) a, но не для Vect Z a.

  • Вместо любого значения (или типа, типы — тоже значения) в Idris можно подставить ?дырку (hole). При проверке типов, компилятор выведет на экран типы всех дырок в программе. Это удобно, когда в какой-то момент непонятно, значение какого типа ожидается.

  • Idris 2 (актуальная версия) использует рантайм Scheme.

  • В Idris 2 есть линейные типы, которые позволяют гарантировать, что значение используется ровно один раз. Это полезно для проверки корректности использования ресурсов: например, взятый лок можно использовать ровно один раз, отпустив его (и получив свободный лок). Аналогично, свободный лок можно ровно один раз взять, получив взятый лок.

  • Idris предоставляет инструментарий для доказательства теорем про исходный код программы.

  • Про Idris есть книга Type-Driven Development with Idris, которая умеет объяснять Idris куда лучше, чем я. К этой книге есть дополнение, исправляющее её для совместимости с Idris 2. Кроме того, в открытом доступе существует туториал по Idris 2.

Язык третий, эзотерический — /// (slashes)

Страница на Esolangs: https://esolangs.org/wiki////

Summary

/// — это язык, полностью основанный на поиске и замене строк в тексте. Он Тьюринг-полный, потому что на нём можно выразить интерпретатор языка Bitwice Cyclic Tag. Поддерживает вывод, но не ввод.

Как выглядит

/]
[///#/ bottles of beer on the wall,
//$/ bottles of beer
Take one down, pass it around
//%/ bottles of beer on the wall.

/99#99$98%98#98$97%97#97$96%96#96$95%95#95$94%94#94$93%93]
[#93$92%92#92$91%91#91$90%90#90$89%89#89$88%88#88$87%87#87]
[$86%86#86$85%85#85$84%84#84$83%83#83$82%82#82$81%81#81$80]
[%80#80$79%79#79$78%78#78$77%77#77$76%76#76$75%75#75$74%74]
[#74$73%73#73$72%72#72$71%71#71$70%70#70$69%69#69$68%68#68]
[$67%67#67$66%66#66$65%65#65$64%64#64$63%63#63$62%62#62$61]
[%61#61$60%60#60$59%59#59$58%58#58$57%57#57$56%56#56$55%55]
[#55$54%54#54$53%53#53$52%52#52$51%51#51$50%50#50$49%49#49]
[$48%48#48$47%47#47$46%46#46$45%45#45$44%44#44$43%43#43$42]
[%42#42$41%41#41$40%40#40$39%39#39$38%38#38$37%37#37$36%36]
[#36$35%35#35$34%34#34$33%33#33$32%32#32$31%31#31$30%30#30]
[$29%29#29$28%28#28$27%27#27$26%26#26$25%25#25$24%24#24$23]
[%23#23$22%22#22$21%21#21$20%20#20$19%19#19$18%18#18$17%17]
[#17$16%16#16$15%15#15$14%14#14$13%13#13$12%12#12$11%11#11]
[$10%10#10$9%9#9$8%8#8$7%7#7$6%6#6$5%5#5$4%4#4$3%3#3$2%2#2]
[$1 bottle of beer on the wall.
 
1 bottle of beer on the wall,
1 bottle of beer
Take one down, pass it around
No more bottles of beer on the wall.

Хайлайты

  • Программа на /// выполняется, пока она не пуста. Действие определяется по первому символу программы:

    Символ Действие
    / Парсит команду в формате /PATTERN/REPLACEMENT/ и заменяет PATTERN на REPLACEMENT
    \ Удаляет два первых символа из программы и выводит второй
    другой Удаляет первый символ из программы и выводит его

  • Замена выполняется, пока в строке остаются вхождения PATTERN. К примеру, программа

    /ab/qa/abb

    будет выполняться так:

    /ab/qa/abb   # Парсим /ab/qa/, выполняем первую замену
/ab/qa/qab   # Замена в самом выражении не происходит
/ab/qa/qqa   # Сделали вторую замену
qqa          # Больше вхождений нет, завершили замену
qa           # Вывели q, удалили символ
a            # Аналогично
             # Вывели a. Программа теперь пуста и выполнение завершается

  • PATTERN — это просто фиксированная строка, не регулярное выражение

  • Очевидно, любая программа на ///, которая не содержит символов / и \ — квайн.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment