#prog #article

Putting the I back in IDE: Towards a Github Explorer

Статья о том, как происходит процесс разработки и ревью кода в Jane street — значительно более интегрированный процесс, чем с комбинацией git и GitHub/Gitlab. Серьёзно, я хочу, чтобы у меня так на работе было.

Imagine a system for editing and reviewing code where:

* Every branch of every repo gets its own sandboxed directory. Your revision history in each branch, including uncommitted stuff, is persisted, as are build artifacts. When you switch contexts, each project is just as you left it.
* Within your editor, you can pull up a global view of all your branches, your outstanding pull requests, and the pull requests you’re assigned to review. It’s one keystroke to view the summary for a pull, and one more to start editing any of its files right there under your cursor.
* Code review happens entirely within the editor. You’re fed a series of diffs: one keystroke to approve, one keystroke to start editing. Dive in, make your changes, leave comments for the author, push, and move on.

We’ve actually developed this workflow at Jane Street, and it’s been used daily by hundreds of engineers for about two years now.

<...>

The trouble is that it’s pretty coupled to our somewhat uncommon toolchain: <...>

The goal of this post, then, is just to show off what the result looks like – to show you what kind of workflow is possible – in the hope that it inspires similar tools in other ecosystems. The truth is that after writing code at work this way for a while, you start to wish that you had something similar at home.

#prog #video

How Jane Street Does Code Review

И небольшой доклад с точки зрения пользователя этой системы. Вместе с ценными ответами на вопросы аудитории.

А на телефоне табличку что-то перекорёжило 😒

Кстати, накидал её в asciiflow.com

#prog #моё

Давайте немного поговорим о вариантности и о том, как она связана с мутабельностью и алиасингом.

Сначала немного напомню о вариантности. Если Sub является подтипом Sup (что записывается как Sub <: Sup), то:

Обобщённый тип Co<T> называется ковариантным по T, если из Sub <: Sup вытекает Co<Sub> <: Co<Sup>;
Обобщённый тип Contr<T> называется контравариантным по T, если из Sub <: Sup вытекает Contr<Sub> :> Contr<Sup> (или, что то же самое, Contr<Sup> <: Contr<Sub>);
Обобщённый тип Inv<T> называется инвариантным по T, если из Sub <: Sup не вытекает ни Inv<Sub> <: Inv<Sup>, ни Inv<Sup> <: Inv<Sub>.

Или, иными словами: ковариантность сохраняет отношение субтипизации, контравариантность обращает отношение субтипизации, а инвариантность вообще его не предохраняет. Уточнение ти́пового параметра важно, поскольку обобщённый тип с несколькими параметрами может иметь разную вариантность по разным параметрам.

Какое это имеет отношение к обычным программистам? Ну, обычные программисты, как правило, пишут на мейнстримных языках программирования, и эти языки обычно объектно-ориентированные. В этих языках часто есть наследование, и наследование можно до некоторой степени моделировать через отношение субтипизации (что не вполне верно, но больше говорит об убогости ЯП, чем о реальной связанности этих концепций).

Пусть у нас есть функция из T в R, сигнатуры T -> R. Тип функции можно представить как применение конструктора типа -> к типам T и R (собственно, в Haskell синтаксис (->) T R валиден), и потому тип функции можно воспринимать, как обобщённый тип с двумя параметрами. Какая же у этого конструктора типов вариантность?

Если мы где-то вызываем функцию типа T -> R, то мы получаем значение типа R. По определению подтипа, вместо значения типа R мы можем использовать значение типа RSub, подтипа R. Значит, если выражение с вызовом функции T -> R тайпчекается, то оно должно продолжить тайпчекаться, если поменять функцию на функцию типа T -> RSub. Обратное, очевидно, неверно: привести супертип к подтипу в общем случае безопасно нельзя. Получается, что конструктор типа функции является ковариантным по возвращаемому типу.

А что насчёт типа аргумента? Очевидно, поменять T -> R на TSub -> R, где TSub <: T, мы не можем: это потребовало по месту вызова приведения T к TSub — направлении, противоположном отношению субтипизации. Но возможно поменять T -> R на TSup -> R, где T <: TSup — в этом случае по месту вызова будет апкаст аргумента, что всегда разрешено. Выходит, конструктор типа функции контрвариантен по типу аргумента.

А теперь немного подумаем о том, что из себя представляет мутабельная переменная. Это не значение как таковое — это имя, которое мы можем использовать для того, чтобы получить значение, и для того, чтобы значение записать. Иными словами, мутабельную переменную можно представить, как некую метку и пару функций для считывания значения и его записи (в принципе, это близко к тому, как выглядят ссылочные ячейки в SML и IORef в Haskell). Функция считывания значения ковариантна по возвращаемому типу — типу значения в мутабельной переменной, а функция записи — контрвариантна по аргументу, то есть по тому же самому типу. Пара этих функций имеет совместные ограничения, которые комбинируются и образуют инвариантность по типу внутри мутабельной переменной. Иными словами, мутабельная переменная может хранить только значения строго обозначенного типа — ни субтипы, ни супертипы. Так как коллекции предоставляют доступ к, по сути, множественным изменяемым переменным, из этого с необходимостью вытекает, что коллекции должны быть инвариантными по типу содержащихся элементов.

Логично? Логично. Но не для дизайнеров Java.

Именно, встроенные массивы в Java ковариантны — в частности, любой массив можно привести к массиву Object. Во время дизайна Java это решение было вызвано необходимостью — первая версия языка не имела дженериков aka параметрического полиморфизма, только полиморфизм подтипов, но обобщённые алгоритмы нужно было как-то писать. Как несложно продемонстрировать, это решение может привести с неприятному поведению:

class Animal {}
class Dog extends Animal {}
class Cat extends Animal {}

public class Main {
    static void put_cat(Animal animals[]) {
        animals[0] = new Cat();
    }
    public static void main(String args[]) {
        Dog dogs[] = new Dog[]{new Dog()};
        put_cat(dogs);
        Dog certainly_not_a_cat = dogs[0];
    }
}

Dog и Cat оба являются наследниками класс Animal, но не являются наследниками друг друга. Однако что происходит в этой программе, которая, между прочим, компилируется?

В первой строчки main мы создаём массив из одной собаки. Во второй строчке мы вызываем функцию put_cat. Dog[] и Animal[] — разные типы, но за счёт того, что Dog наследует Animal, первый тип массива можно привести ко второму. В функции put_cat единственный элемент типа Animal перезаписывается значением типа Cat — это легально, так как Cat наследует Animal. В третьей строчке мы достаём собаку из массива собак... Только это уже кошка.

Получается, мы привели значение одного типа (Cat) к значению совершенно другого типа (Dog). Более того, используя Object[], мы можем менять тип у любого значения на любой произвольный! Тем не менее, эта программа компилируется. Разве эта проблема не из числа тех, от которых нас должна защищать система типов?!

Разумеется, на самом деле подобный котд в Java не работает — если запустить программу выше, то она упадёт с исключением:

Exception in thread "main" java.lang.ArrayStoreException: Cat
at Main.put_cat(Main.java:7)
at Main.main(Main.java:11)

Именно для того, чтобы избежать подобных проблем, JVM делает дополнительную работу в рантайме. Именно, она хранит для массивов, какой тип реально там хранится и при присваивании элемента массива сверяет этот тип с типом того, что присваивается, и бросает исключение, если эти типы несовместимы. КАЖДОЕ. ПРИСВАИВАНИЕ. В МАССИВ. Мало того, что система типов нам наврала — это ещё и даёт лишний оверхед на проверку в рантайме для программы, в которой, по хорошему, такого поведения вообще не должно быть! И в C#, авторы которого на первых порах старательно копировали Java, утащили в язык и этот недостаток (который Эрик Липперт считает самой большой ошибкой в C#).

После появления дженериков в обоих языках эту дыру прикрыли. Именно, ArrayList<T> в Java и List<T> в C# инвариантны по типу элементов. Если поменять в программе массивы на ArrayList:

import java.util.ArrayList;

class Animal {}
class Dog extends Animal {}
class Cat extends Animal {}

public class Main {
    static void put_cat(ArrayList<Animal> animals) {
        animals.set(0, new Cat());
    }

    public static void main(String args[]) {
        var dogs = new ArrayList<Dog>();
        dogs.add(new Dog());
        put_cat(dogs);
        Dog certainly_not_a_cat = dogs.get(0);
    }
}

, то компилятор не пропустит программу:

Main.java:15: error: incompatible types: ArrayList<Dog> cannot be converted to ArrayList<Animal>
put_cat(dogs);

Можем ли мы сделать ковариантные коллекции? Можем. Но, как мы помним, сеттер для мутабельной переменной контравариантный по принимаемому типу. Значит, для того, чтобы оставить только ковариантность, нужно выкинуть сеттер — или, иными словами, сделать коллекции с операциями только для чтения. По не вполне понятным причинам в Java из коробки нет вменяемых неизменяемых коллекций (те, что кидают исключение на изменяющие операции — не вменяемые), поэтому продемонстрирую на примере C#:

using System.Collections.Generic;

class Animal {}
class Dog: Animal {}
class Cat: Animal {}

class Program
{
    static void put_cat(IReadOnlyList<Animal> animals) {
        animals[0] = new Cat();
    }

    static void Main() {
        var dogs = new Dog[]{new Dog()};
        put_cat(dogs);
        var certainly_not_a_cat = dogs[0];
    }
}

Программа не компилируется — компилятор жалуется на строчку в put_cat:

/home/Program.cs(10,9): error CS0200: Property or indexer 'IReadOnlyList<Animal>.this[int]' cannot be assigned to -- it is read only [/home/home.csproj]

Что ж, это победа: мы победили козни ковариантности, уничтожив его гнусного прислужника — мутабельность! Ковариантность и мутабельность плохо сочетаются, и иметь их по отдельности — это ультимативное решение проблемы.

...Или нет?

Давайте немного поговорим о том, почему вообще присваивание Cat в массив из Animal является небезопасным. Очевидно, в самой функции put_cat у нас есть доступ только к набору значений Animal — без явного каста привести их к какому-то точному типу мы не можем. С другой стороны, Cat апкастится к Animal, который вроде как вполне можно положить в массив Animal. Внутри put_cat никаких проблем нет!

Что действительно является проблематичным — так это dogs на вызывающей стороне. Именно, тип Dog[] апкастится до Animal[] при вызове put_cat — но после вызова put_cat переменная dogs всё ещё доступна! Вызывающая сторона помнит более точный тип dogs, и потому может увидеть, что туда положили Animal, который не обязательно является Dog.

С другой стороны, что, если про изначальный массив dogs мы просто... Забудем? В этом случае мы можем перезаписать значение типом, отличным от изначального — но это нормально, потому что этого всё равно никто не увидит! Таким образом, выкинув последнюю строку из main, мы получим вполне себе нормальную программу с вменяемой семантикой... Которая всё равно будет кидать ArrayStoreException. И это вполне понятно: для того, чтобы определить, что put_cat — безопасная функция, нужно удостовериться, что массив до апкаста после вызова нигде не используется (массив после апкаста можно и сохранить, он не может привести к проблемам). Это требование, однако, никак не выражено в типах, и потому компилятор не может его проверить — иными словами, компилятор не может проверить, что аргумент put_cat не пересекается (или, выражаясь жаргоном, не алиасится) с другими переменными. Вот бы был способ сказать компилятору, что на данное значение ссылается одно и только одно имя... Звучит знакомо?

Если вы помните мой пересказ серии статей Oxidizing OCaml, то там был упомянут strong function update — апдейт поля значением иного типа. Как я писал, сделать это in-place возможно только тогда, когда текущее имя уникально ссылается на значение — в противном случае код может по старому имени прочитать значение нового типа как значение старого типа. Апкаст от Dog[] до Animal[], очевидно, меняет тип, и если мы не хотим копировать значения просто для избегания ломающего систему типов поведения — а мы не хотим — то мы должны удостовериться, что после получения значения типа Animal[] значение типа Dog[] более недоступно — или, иными словами, апкаст сохраняет уникальность ссылки. Если нам получится каким-то образом это сделать, то компилятор сможет дать нам нужную ошибку: именно, указать на то, что dogs используется, не смотря на то, что уникальность была передана.

К сожалению, одной лишь уникальности недостаточно для обеспечения корректности — нужны ещё линейные (или хотя бы афинные) аннотации на значениях для корректной обработки замыканий, захватывающих уникальные ссылки, что уже довольно сильно влияет на систему типов. Так что такое развитие мы навряд ли увидим в Java — как и в любом языке на JVM, в котором с Java есть интероп.

Также подход с readonly-колекциями одновременно избыточен и недостаточен... Но об этом, пожалуй, в другой раз.

Годовые итоги. Лично я плакала больше всех.

Гоните его, насмехайтесь над ним

UPD (24.12.2023): знакомый нашёл жильё. Спасибо, помощь больше не требуется.

Здравствуйте, дорогие подписчики. Конкретно сегодня я обращаюсь к тем из вас, кто живёт в Украине. Сегодня одного моего знакомого, который живёт в Киеве, выгнали из дома родители. Это не в первый раз, но теперь знакомый даже не планирует возвращаться. Сейчас он оперативно ищет жильё — желательно в Киеве или в окрестностях. У него сейчас есть место лишь на несколько дней. Планирует оставаться на продолжительный срок, готов оплачивать арендную плату и коммуналку, самому платить за свою еду. В идеале ищет сожителя.

Если кто-то может помочь — пишите ему в личку: @QoiAA.

Репосты желательны.

...

(#kbd)

...

(#kbd)

#itsec #suckassstory