Каков подход вывода F # к дженерикам? - PullRequest
Новая
       62

Каков подход вывода F # к дженерикам?

1 голос
/ 25 мая 2019

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

Это компилируется, а id равно 'a -> 'a, что (если я не ошибаюсь) означает, что каждый вызов использует «свежий» тип. 

let id x = x

let id1 = id 1
let id2 = id "two"

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

Здесь mul сообщается как int -> int -> int

let mul x y = x * y

let mul1 = mul 1 2
let mul2 = mul 1.1 2.2 // fails here

Если я переупорядочиваюих, тогда mul - это float -> float -> float: 

let mul x y = x * y

let mul2 = mul 1.1 2.2
let mul1 = mul 1 2 // fails here

Не могли бы вы объяснить (желательно не в академических) терминах, что такое правила и, возможно, как они работают с точки зрения реализации проверки типов?Проходит ли он функции, чтобы проверять их типы каждый раз, когда на них ссылаются?Или есть какой-то другой подход?

Ответы [ 2 ]

5 голосов
/ 25 мая 2019

Во-первых, обратите внимание, что этого не произойдет, если мы объявим mul как встроенную функцию: 

let inline mul x y = x * y

let mul1 = mul 1 2  // works
let mul2 = mul 1.1 2.2 // also works

Здесь предполагаемый тип mul будет выглядеть следующим образом: 

x: ^a -> y: ^b ->  ^c
    when ( ^a or  ^b) : (static member ( * ) :  ^a *  ^b ->  ^c)

Этот тип означает, что параметры x и y могут иметь любой тип (даже не обязательно того же типа), если хотя бы у одного из них есть статический член с именем *, который принимает аргументы тех же типов, что и x и y. Тип возврата mul будет таким же, как и для элемента *.

Так почему же вы не получаете такое же поведение, когда mul не встроен? Поскольку ограничения членов (то есть ограничения типов, которые говорят, что у типа должны быть определенные члены) разрешены только для встроенных функций - именно поэтому переменные типа имеют ^ впереди вместо обычного ': чтобы показать, что мы ' мы имеем дело с другим, менее ограниченным типом переменной типа.

Так почему же существует это ограничение для не встроенных функций? Из-за чего .NET поддерживает. Ограничения типа, такие как «T реализует интерфейс I», выражаются в байт-коде .NET и, таким образом, разрешены во всех функциях. Ограничения типа, такие как «T должен иметь определенный член с именем X с типом U», не могут быть выражены и поэтому не допускаются в обычных функциях. Поскольку встроенные функции не имеют соответствующего метода в сгенерированном байт-коде .NET, нет необходимости, чтобы их тип был выразим в байт-коде .NET, и поэтому ограничения к ним не применяются.

3 голосов
/ 25 мая 2019

Этот аспект вывода типа F # не особенно академичен, но он прекрасно работает на практике.Способ вывода типа F # заключается в том, что компилятор изначально обрабатывает все как переменную типа (универсальный тип) и собирает ограничения на них.Затем он пытается решить эти ограничения.

Например, если у вас есть: 

let callWithTen f = f 10

Затем первоначально компилятор присваивает типы, такие что callWithTen имеет тип 'a и f имеет тип 'b.Он также собирает следующие ограничения:

  • 'a = 'a0 -> 'a1, поскольку callWithTen синтаксически определен как функция
  • 'a0 = 'b, поскольку переменная f является аргументом функции
  • 'b = 'b0 -> 'b1, поскольку переменная f используется в качестве функции
  • 'b0 = int, поскольку аргумент f является int.
  • 'b1 = 'a1 потому что результат вызова f является результатом callWithTen.

Решая эти ограничения, компилятор выводит, что callWithTen имеет тип (int -> 'b1) -> 'b1.

Если в вашем коде +, вы не можете точно определить, что именно является числовым типом.Некоторые другие языки ML решают эту проблему, имея + для целых чисел и +. для чисел с плавающей запятой, но это очень уродливо, поэтому F # использует другой подход, который несколько нерегулярен.

КакНасколько я знаю, F # имеет ограничение по линии 'a supports (+).Итак, что происходит в вашем случае (в несколько упрощенном описании), это то, что add является функцией 'a0 -> 'a0 -> 'a0, где 'a0 supports (+).

При обработке остальной части кода компилятор также собирает ограничения 'a0 = int (при первом вызове) и 'a0 = float (при втором вызове).Сначала он разрешает первый, что нормально (потому что int поддерживает +), но затем он терпит неудачу во втором ограничении, потому что int != float и сообщает об ошибке там.

...