← На главную

В OCaml эмулируют guarded methods через GADT-свидетель Refl

03.08.2026 16:15 · hackernews

Guarded methods дают возможность навешивать ограничения на receiver только у отдельных методов: такой метод вызывается, лишь когда тип receiver удовлетворяет заданному условию. В OCaml такие методы нельзя объявить напрямую, но их можно закодировать через type equality witness.

Проблема возникает в языках с параметрическим полиморфизмом вроде Java: если написать class MyClass<T extends S>, ограничение действует на весь класс. Хочется иногда ограничивать только конкретные методы. Например, для класса MyList<A> было бы удобно определить flatten, который работает только когда A — это список. Если вынести метод в статический контекст или companion object, теряется единообразная отправка сообщений экземпляру. Kotlin и C# предлагают extension methods, но метод всё равно живёт вне класса, и ради доступа к внутренностям могут понадобиться лишние public члены.

Самый «идейный» вариант — guarded methods: метод остаётся внутри класса, но его receiver уточняется. В синтаксисе, предложенном Габриэлем Шерером в слайдах доклада про симметрию объектно-ориентированного и функционального программирования, это выглядело бы как method flatten : 'b olist with 'a = 'b olist. В OCaml такого синтаксиса нет, однако его можно сэмулировать.

Для этого нужен GADT-свидетель равенства типов:

type (_, _) eq = Refl : ('a, 'a) eq

Значение Refl можно создать только когда два типа действительно равны, поэтому передача такого значения — это доказательство равенства. Для flatten достаточно потребовать параметр ('a, 'b list) eq -> 'b list. В реализации рекурсивно разбираем список через uncons, и на каждом шаге паттерн-матчинг по Refl даёт компилятору знание, что 'a = 'b list, так что голову можно использовать как список. Аналогично добавляется метод sum: он принимает ('a, int) eq -> int и работает только для списков целых чисел.

Всё проверяется статически: если вызвать a # sum Refl для списка списков, компилятор выдаст ошибку несовместимости типов int list и int. Такой код можно писать, но явная передача свидетелей делает вызовы тяжеловатыми. В Scala, как подметил Николя Ринаудо, похожий приём используется с неявным witness, поэтому вызывающему не приходится передавать Refl вручную. В OCaml это скорее интересный и практичный пример использования equality witness, чем обязательный приём для повседневной работы.

Читать оригинал →