Смущен о подтипе функций

Question

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

Чтобы уточнить: предположим, что у нас есть следующее отношение типа:

bool<int<real

Почему функция (real->bool) является подтипом (int->bool)? Не должно ли быть наоборот?

Я бы ожидал, что критерии для функций подтипа будут такими: f1 является подтипом f2, если f2 может принимать любой аргумент, который может принимать f1, и f1 возвращает только значения, которые возвращает f2. Ясно, что есть значения, которые может принимать f1, а f2 - нет.

Answer 1

Вот правило для подтипа функций:

Типы аргументов должны быть противоположными, типы возвращаемых данных должны быть ко-вариантами.

Ко-вариант == сохраняет иерархию «A является подтипом B» для типа параметра результатов.

Контра-вариант == инвертирует ("идет вразрез") иерархию типов для параметра arguments.

Итак, в вашем примере:

f1:  int  -> bool
f2:  bool -> bool

Мы можем с уверенностью заключить, что f2 является подтипом f1. Зачем? Поскольку (1) при рассмотрении только типов аргументов для обеих функций, мы видим, что иерархия типов «bool является подтипом типа int» фактически является ко-вариантом. Он сохраняет иерархию типов между int и bools. (2) Рассматривая только типы результатов для обеих функций, мы видим, что противоречие сохраняется.

Другими словами (простой английский, как я думаю об этом предмете):

противоречивые аргументы: "мой абонент может передать на больше , чем мне требуется, но это нормально, потому что я буду использовать только то, что мне нужно". возвращаемые значения ко-варианта: «Я могу вернуть больше , чем требует вызывающая сторона, но это нормально, он или она просто использует то, что им нужно, и игнорирует все остальное»

Давайте посмотрим на другие примеры, используя структуры, где все является целым числом:

f1:  {x,y,z} -> {x,y}
f2:  {x,y}   -> {x,y,z}

Итак, опять же, мы утверждаем, что f2 является подтипом f1 (который он есть). Если посмотреть на типы аргументов для обеих функций (и использовать символ <для обозначения «является подтипом»), то если f2 <f1, то есть {x, y, z} <{x, y}? Ответ - да. {x, y, z} является ко-вариантом с {x, y}. то есть при определении структуры {x, y, z} мы «унаследовали» от структуры {x, y}, но добавили третий член, z. </p>

Глядя на типы возвращаемых данных для обеих функций, если f2 {x, y, z}? Ответ снова - да. (См. Выше логику).

И все же третий способ думать об этом - предположить, что f2

   F1 = f1;
   F2 = f2;
   {a,b}   = F1({1,2,3});  // call F1 with a {x,y,z} struct of {1,2,3};  This works.
   {a,b,c} = F2({1,2});    // call F2 with a {x,y} struct of {1,2}.  This also works.

   // Now take F2, but treat it like an F1.  (Which we should be able to do, 
   // right?  Because F2 is a subtype of F1).  Now pass it in the argument type 
   // F1 expects.  Does our assignment still work?  It does.
   {a,b} = ((F1) F2)({1,2,3});

Answer 2

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

---

Правило подтипа:

Это означает, что если условия верхнего подтипа выполнены, то нижнее значение сохраняется.

В определении типа функции аргументы функции являются контравариантными , так как мы изменили отношение подтипа между T1 и S1. Результаты функции являются ковариантными , поскольку они сохраняют отношение подтипа между T2 и S2.

С определением вне пути, почему это правило такое? Это хорошо указано в ответе Аарона Фи, и я также нашел определение здесь (поиск по заголовку «Типы функций»):

Альтернативное представление состоит в том, что можно разрешить функцию одного типа S1 → S2 для использования в контексте, где ожидается другой тип T1 → T2 пока ни один из аргументов, которые могут быть переданы функции в этом контексте, не удивит ее (T1 <: S1), и ни один из возвращаемых результатов не удивит контекст (S2 <: T2).

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

Для всех приведенных ниже примеров:

1. S1 := {x, y}
2. T1 := {x, y, z}
3. T2 := {a}
4. S2 := {a, b}

Пример с контравариантными типами аргументов и ковариантными типами возвращаемых данных

Пусть:

1. f1 имеют тип S1 → S2 ⟹ {x, y} → {a, b}
2. f2 имеют тип T1 → T2 ⟹ {x, y, z} → {a}

Теперь предположим, что type(f1) <: type(f2). Мы знаем это из приведенного выше правила, но давайте представим, что нет, и просто посмотрим, почему это имеет смысл.

Мы бежим map( f2 : {x, y, z} → {a}, L : [ {x, y, z} ] ) : [ {a} ]

Если мы заменим f2 на f1, мы получим:

map( f1 : {x, y} → {a, b}, L : [ {x, y, z} ] ) : [ {a, b} ]

Это хорошо работает, потому что:

1. Независимо от того, что функция f1 делает со своим аргументом, она может игнорировать дополнительное поле записи z и не иметь проблем.
2. Независимо от того, что контекст map делает с результатами, он может игнорировать дополнительное поле записи b и проблем нет.

Заключительное:

{x, y} → {a, b} ⟹ {x, y, z} → {a} ✔

Пример с ковариантными типами аргументов и ковариантными типами возвращаемых данных

Пусть:

1. f1 имеют тип T1 → S2 ⟹ {x, y, z} → {a, b}
2. f2 имеют тип S1 → T2 ⟹ {x, y} → {a}

Предположим, type(f1) <: type(f2)

Мы бежим map( f2 : {x, y} → {a}, L : [ {x, y} ] ) : [ {a} ]

Если мы заменим f2 на f1, мы получим:

map( f1 : {x, y, z} → {a, b}, L : [ {x, y} ] ) : [ {a, b} ]

Здесь мы можем столкнуться с проблемой, потому что f1 ожидает и может работать с полем записи z, и такого поля нет ни в одной записи в списке L. ⚡

Пример с контравариантными типами аргументов и контравариантными типами возвращаемых данных

Пусть:

1. f1 имеют тип S1 → T2 ⟹ {x, y} → {a}
2. f2 имеют тип T1 → S2 ⟹ {x, y, z} → {a, b}

Предположим type(f1) <: type(f2)

Мы бежим map( f2 : {x, y, z} → {a, b}, L : [ {x, y, z} ] ) : [ {a, b} ]

Если мы заменим f2 на f1, мы получим:

map( f1 : {x, y} → {a}, L : [ {x, y, z} ] ) : [ {a} ]

У нас нет проблем с игнорированием поля записи z при передаче в f1, но если контекст, вызывающий map, ожидает список записей с полем b, мы увидим ошибку. ⚡

Пример с ковариантными типами аргументов и контравариантным возвратом

Посмотрите на приведенные выше примеры для двух мест, где это может пойти не так.

Заключение

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

Answer 3

На вопрос дан ответ, но я хотел бы привести здесь простой пример (относительно типа аргумента, который является неинтуитивным).

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

typedef FuncTypeA = Object Function(Object obj); // (Object) => Object
typedef FuncTypeB = String Function(String name); // (String) => String

void process(FuncTypeA myFunc) {
   myFunc("Bob").toString(); // Ok.
   myFunc(123).toString(); // Fail.
   myFunc(true).toString(); // Fail.
}

FuncTypeB myFuncB = (String name) => name.toUpperCase();

process(myFuncB);

Однако приведенный ниже код будет работать , потому что теперь вы можете передавать объекты любого типа в myFuncB, и мы только передаем строки.

typedef FuncTypeA = Object Function(String name); // (String) => Object
typedef FuncTypeB = String Function(Object obj); // (Object) => String

void process(FuncTypeA myFuncA) {
   myFunc("Bob").toString(); // Ok.
   myFunc("Alice").toString(); // Ok.
}

FuncTypeB myFuncB = (Object obj) => obj.toString();

process(myFuncB);