Вывод типа в Голанге / Хаскеле

9

Я читал, что на самом деле Go не имеет истинного вывода типа в том смысле, в котором функциональные языки, такие как ML или Haskell, имеют, но я не смог найти простого для понимания сравнения двух версий. Может ли кто-нибудь объяснить в общих чертах, как вывод типа в Go отличается от вывода типа в Haskell, и плюсы / минусы каждого?

a3onstorm
источник

Ответы:

13

Посмотрите этот ответ StackOverflow относительно вывода типа Go. Я сам не знаком с Go, но на основании этого ответа он выглядит как односторонний «вывод типа» (если позаимствовать некоторую терминологию C ++). Это означает, что если у вас есть:

x := y + z

затем тип xопределяется путем выяснения типа y + z, что довольно легко сделать для компилятора. Для этого типы yи zдолжны быть известны априори : это можно сделать с помощью аннотаций типов или вывести из литералов, назначенных им.


Напротив, большинство функциональных языков имеют вывод типа, который использует всю возможную информацию в модуле (или функцию, если алгоритм вывода является локальным) для получения типа переменных. Сложные алгоритмы вывода (такие как Хиндли-Милнер) часто вовлекают некоторую форму объединения типов (немного похоже на решение уравнений) за кулисами. Например, в Haskell, если вы напишите:

let x = y + z

тогда Haskell может определить тип не только, xно yи zпросто, основываясь на том факте, что вы выполняете сложение для них. В этом случае:

x :: Num a => a
y :: Num a => a
z :: Num a => a

(Нижний регистр aздесь обозначает полиморфный тип , часто называемый «обобщением» в других языках, таких как C ++. Эта Num a =>часть является ограничением, указывающим, что aподдержка типа имеет некоторое представление о добавлении.)

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

let fix f = f (fix f)

Обратите внимание, что нигде мы не указали тип fи не указали тип fix, но компилятор Haskell может автоматически выяснить, что:

f :: t -> t
fix :: (t -> t) -> t

Это говорит о том, что:

  • Параметр fдолжен быть функцией от произвольного типа tдо того же типа t.
  • fixэто функция, которая получает параметр типа t -> tи возвращает результат типа t.
Rufflewind
источник
4
более точно, Haskell можно сказать , что x, y, zтакая же Numтип Эрика, но они все еще могут быть Integers, DoubleS, Ratio IntegerS ... Haskell готов сделать произвольный выбор между числовыми типами, но не для других классов типов.
Джон Дворак
7

Вывод типа в Go чрезвычайно ограничен и чрезвычайно прост. Он работает только в одной языковой конструкции (объявление переменной) и просто берет тип с правой стороны и использует его в качестве типа для переменной с левой стороны.

Вывод типов в Haskell можно использовать везде, его можно использовать для определения типов для всей программы. Он основан на унификации, что означает, что (концептуально) все типы выводятся «сразу», и все они могут влиять друг на друга: в Go информация о типах может перетекать только из правой части объявления переменной в левую. стороны, никогда не в другом направлении и никогда вне объявления переменной; в Haskell информация о типах свободно распространяется во всех направлениях по всей программе.

Тем не менее, система типов Haskell настолько мощна, что вывод типа может фактически не выводить тип (или, точнее, должны быть введены ограничения, чтобы тип всегда мог быть выведен). Система типов Go настолько проста (без подтипов, без параметрического полиморфизма), и ее вывод настолько ограничен, что всегда успешен.

Йорг Миттаг
источник
4
«В Хаскеле информация о типах свободно распространяется во всех направлениях через всю программу»: я считаю, что это дает очень хорошую интуицию. +1
Джорджио
Утверждения, которые дает этот ответ в последнем абзаце, немного вводят в заблуждение. У Haskell нет подтипов. Кроме того, параметрический полиморфизм не вызывает никаких проблем для полноты вывода типов: Хиндли-Милнер в полиморфном лямбда-исчислении всегда находит наиболее общий тип. Haskell может не определить типы, но это будет связано со сложными функциями системы типов, такими как GADT, где при наивной формулировке не существует основного (т. Е. «Наилучшего выбора») типа.
Эдвард З. Ян