Еще немного о функциях типа

Мой предыдущий пост о функциях типа вызвал интересную дискуссию здесь и на Reddit .

Поэтому, я думаю, стоит связать несколько слабых мест из предыдущего поста. Итак, вот коллекция дальнейших наблюдений о функциях типа.

Предупреждение: этот пост посвящен некоторым очень техническим деталям того, как мы включили функции типов в систему типов Цейлона. Даже не продолжайте дальше, пока не прочитаете более ранний пост .

«Почему» этого

Наиболее известное применение обобщенных шаблонов высшего порядка — для представления высокоуровневых абстракций типов контейнеров: функторов, монад и друзей. Это не то, что побудило меня экспериментировать с дженериками высшего порядка на Цейлоне, и на практике я все еще мало интересуюсь этими абстракциями, хотя с ними интересно играть.

Нет, меня беспокоило не то, что система типов Цейлона была недостаточно мощной, чтобы представлять Functor или Monad , а то, что система типов Цейлона была недостаточно мощной, чтобы представлять Цейлон . Я покажу вам, что я имею в виду, всего за секунду. Но сначала я хочу утверждать, что функции типа могут рассматриваться как регуляризация языка.

С чисто синтаксической точки зрения всегда казалось немного странным, что каждый вид объявления типа в Цейлоне может иметь список параметров типа, кроме самого параметра типа . Кроме того, заметно, что я могу взять ссылку или мета-ссылку на любой элемент программы, если у него нет списка параметров типа . Теперь такие ограничения могут показаться разумными, если параметризованный параметр типа или ссылка на общее объявление не являются осмысленными понятиями на фундаментальном уровне. Но они явно имеют смысл и даже, по крайней мере, несколько полезны.

Насколько полезен другой вопрос — жюри все еще отсутствует, по крайней мере, на мой взгляд. И поэтому, возможно, мы в конечном итоге придем к выводу, что этот материал не стоит своего веса. Вес, по существу, — это время, которое требуется программистам, незнакомым с Цейлоном, чтобы понять это.

В оригинальном посте я показал, как функции типов необходимы для представления типа ссылки на обобщенную функцию. Одним из мест, где возникает эта проблема, является одна из более уникальных особенностей Цейлона: его типобезопасная метамодель .

Вариант использования для ссылочных типов универсальных функций

Обычно я могу получить объект метамодели, который представляет класс или функцию и захватывает сигнатуру его типа. Например, выражение `String` оценивается как объект метамодели, который захватывает параметры типа и инициализатора класса String :

Для общего объявления я могу сделать аналогичную вещь, пока я готов записать аргументы типа. Например, я могу написать `Singleton<String>` чтобы получить объект метамодели, представляющий класс Singleton после применения аргумента типа String :

Но в Цейлоне, как он существует сегодня, я не могу получить типизированный объект метамодели, который представляет просто `Singleton` , потому что для представления типа этого объекта метамодели мне обязательно понадобится функция типа.

Теперь, с новой экспериментальной поддержкой функций типа, тип выражения `Singleton` может быть <T> => Class<Singleton<T>,[T]>() , позволяя код наподобие этого:

Это всего лишь один пример того, как разрешение ссылок на общие функции делает Ceylon более «законченным».

Два варианта использования для функций анонимного типа

У меня складывается впечатление, что «самым страшным» из того, что я представил в предыдущем посте, является нотация для функций анонимного типа. То есть следующий синтаксис:

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

Но — кто-то может разумно спросить — зачем они нам нужны, если названные версии легче читать ?

Ну, они нам нужны

1. чтобы иметь возможность обозначать тип ссылки на универсальную функцию — помните, у нас нет цеодонируемых типов в Цейлоне — и
2. чтобы было легко частично применить функцию именованного типа, такую ​​как Map .

Например, мы хотим иметь возможность писать что-то вроде <T> => Map<String,T> при работе с обобщенными шаблонами высшего порядка, таким образом превращая функцию типа двух параметров типа в функцию типа одного параметра типа.

Являются ли функции типов «типами»?

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

Просто нет никакой дополнительной системы мета-типов для типов в Цейлоне. Самое близкое, что у нас есть к «типу», — это ограничение общего типа, но это чрезвычайно обедненный тип типа, так как Ceylon вообще не предоставляет никаких средств для абстрагирования от ограничений типа — я даже не могу назначить псевдоним для введите ограничение и используйте его по имени.

Цейлон рассуждает об ограничениях типов и назначении типов для переменных типов, используя жестко закодированные правила, записанные примитивно в спецификации языка и средства проверки типов, а не путем абстрагирования типов типов.

Тип функции и подтипы

Но если функция типа является типом, каковы ее подтипные отношения с другими типами и функциями других типов?

Ну, во-первых, напомним, что у некоторых функций типов есть экземпляры: ссылки на общие функции. Мы не хотели вводить значения в язык, которые не являются Object s, поэтому мы объявили, что каждая функция типа является подтипом Object . Это сохраняет полезное свойство, что наша система типов имеет единственный корневой тип Anything .

Далее, напомним, что обычный тип функции является ковариантным по своему типу возвращаемого значения и контравариантным по своим типам параметров. Например, тип функции:

это подтип:

Поскольку, если функция принимает два Object и возвращает String , то это, очевидно, также функция, которая принимает две String и возвращает Object .

Даны два типа функций с одним параметром:

Тогда F(P) является подтипом G(Q) если P является супертипом Q и F является подтипом G

Аналогичные правила применяются к функциям типа. Рассмотрим две функции типа одного параметра типа:

Тогда A является подтипом B тогда и только тогда:

• верхняя граница U на X является супертипом верхней границы V на Y , и
• для любого типа T F<T> является подтипом G<T> .

То есть, если A<X> принимает каждый аргумент типа T который принимает B<Y> , и для каждого такого T применяемый тип A<T> является подтипом применяемого типа B<T> , то мы можем разумно заменить B на A в хорошо напечатанном коде.

(Конечно, эти правила обобщают функции типа с несколькими параметрами типа.)

Общие типы функций и подтипы

Теперь давайте сузим наше внимание, чтобы рассмотреть только функции типов, которые представляют типы универсальных функций. Чтобы упростить задачу, мы рассмотрим универсальные функции следующей формы с одним параметром типа и одним параметром-значением:

Здесь F<X> — это тип возвращаемого значения, выражение типа, включающее параметр типа X , а P<X> — тип параметра, который также включает X

Тип этой универсальной функции — как мы видели в предыдущем посте — это функция типа:

Итак, давайте рассмотрим две функции типа общего вида, которые мы рассматриваем:

Затем мы быстро видим, что A является подтипом B тогда и только тогда:

• верхняя граница U на X является супертипом верхней границы V на Y , и
• для любого типа T возвращаемый тип F<T> для A является подтипом возвращаемого типа G<T> для B , а тип параметра P<T> для A является супертипом типа параметра Q<T> для B

Например, этот универсальный тип функции:

является подтипом этого универсального типа функции:

Найдите минутку, чтобы убедить себя, что это правильно, интуитивно понятно.

(Опять же, эти правила естественным образом обобщаются на функции с несколькими типами параметров и / или несколькими значениями параметров.)

Функции типа и вывод типа

Когда мы вызываем обобщенную функцию первого порядка в Цейлоне, нам обычно не нужно явно указывать аргументы типа. Вместо этого мы обычно можем вывести их из значений аргументов выражения вызова. Например, если у нас есть эта универсальная функция:

Тогда мы всегда можем безопасно вывести In и Out , потому что есть уникальный и наиболее точный выбор аргументов типа:

В этом примере мы можем с уверенностью заключить, что In — это Integer , а Out — это String , без потери точности.

К сожалению, как только дженерики высшего порядка вступают в игру, вывод функций типа становится гораздо более неоднозначной проблемой. Рассмотрим эту обобщенную функцию второго порядка, которая абстрагирует функцию map() от типа контейнера, представляя переменную функции типа Box для представления неизвестного типа контейнера:

А теперь рассмотрим следующий вызов этой функции:

Какой тип мы должны вывести для Element , и какой тип функции для Box ?

• Integer и List ?
• Integer и Iterable ?
• Integer и ArrayList ?
• Integer и MutableList ?
• Integer и ListMutator ?
• Integer и Collection ?
• Object и Category ?

В общем, может быть несколько разных разумных вариантов, и нет действительно хороших критериев для выбора между ними. Поэтому в этом случае мы требуем, чтобы аргументы типа были указаны явно:

Однако есть шаблон, который мы можем использовать, чтобы сделать вывод функции типа возможным. В этом случае мы могли бы определить следующий интерфейс:

Теперь давайте представим, что наш класс ArrayList наследует Functor , так что любой ArrayList<Element> является Functor<List,Element> .

И давайте переопределим fmap() следующим образом:

Затем, наконец, для того же выражения экземпляра, которое мы имели раньше:

Теперь мы можем однозначно сделать вывод, что Box — это List а In — это Integer , поскольку эти типы кодируются как аргументы типа для Functor в главном экземпляре супертипа Functor для выражения ArrayList { 10, 20, 30 } .

Экземпляры функций типа

В оригинальном посте мы отметили, что функция типа, которая возвращает тип функции, является типом универсальной функции. Например, функция типа:

Тип этой универсальной функции:

Но тогда естественно спросить: если некоторые функции типов являются типами универсальных функций, то какие типы функций являются типами?

Что ж, если вы задумаетесь на секунду об отношениях между типами и значениями, я думаю, вы увидите, что они должны быть типами объявлений общих значений . То есть этот тип функции:

будет тип этого значения, записанный в псевдо-Цейлон:

То есть, когда представлен тип X , list<X> преобразуется в List<X> .

Конечно, в Цейлоне нет реальных обобщенных значений, самое близкое, что у нас есть, это нулевая обобщенная функция:

чей тип на самом деле:

Не планируется вводить общие значения в Цейлон, поэтому такие типы, как <X> => List<X> , не имеют экземпляров. Они полезны только в качестве аргументов типов для универсальных типов высшего порядка.

Функции типа и главная типизация

Наконец, давайте рассмотрим довольно технический момент.

Очень важным свойством системы типов Цейлона является способность образовывать основные экземпляры любого объединения или пересечения различных экземпляров универсального типа.

Например, для ковариантного типа List<T> :

• List<X> | List<Y> List<X> | List<Y> имеет основной экземпляр List<X|Y>
• List<X> & List<Y> имеет основной экземпляр List<X&Y>

Для контравариантного типа Comparable<T> :

• Comparable<X> | Comparable<Y> Comparable<X> | Comparable<Y> имеет основной экземпляр Comparable<X&Y>
• Comparable<X> & Comparable<Y> имеет основной экземпляр Comparable<X|Y>

Естественно, важно, чтобы мы могли делать одни и те же трюки для пересечений и объединений экземпляров типов более высокого порядка. Как и в случае, это работает очень естественно, используя следующие тождества:

• <<X> => F<X>> | <<Y> => G<Y>> <<X> => F<X>> | <<Y> => G<Y>> является подтипом <T> => F<T> | G<T> <T> => F<T> | G<T> и
• <<X> => F<X>> & <<Y> => G<Y>> является подтипом <T> => F<T> & G<T> .

Таким образом, если мы имеем следующий ковариантный тип второго порядка:

Затем мы получаем следующие основные экземпляры:

• Functor<E,A> | Functor<F,B> Functor<E,A> | Functor<F,B> имеет главный экземпляр Functor<E|F,<T> => A<T>|B<T>> , и
• Functor<E,A> & Functor<F,B> имеет главный экземпляр Functor<E&F, <T> => A<T>&B<T>> .

Вам не нужно знать эти тождества, когда вы пишете код на Цейлоне, но приятно знать, что функции типов не подрывают базовые алгебраические свойства, из-за чего с системой типов Цейлона так приятно работать. Здесь все сходится, без странных дыр и угловых чехлов.

Слово о «ранге»

В предыдущем посте я описал нашу поддержку ссылок на универсальные функции как полиморфизм «произвольного ранга», что вызвало краткое обсуждение того, как измерять ранг универсального типа. Теперь я думаю, что термин «ранг», вероятно, не имеет особого смысла в связи с Цейлоном, поскольку в наших типах функций нет ничего особенного: это всего лишь экземпляры совершенно обычного универсального типа Callable . Как предполагает Камацу на Reddit , мне кажется, что более подходящее слово, вероятно, будет «непредсказуемым».