LINUX.ORG.RU

Вопрос по выводу типов по Хиндли-Милнеру

 , ,


2

3

Читаю про вывод типов, и возник вопрос по этому абзацу:

По-существу, Хиндли-Милнер (или «Дамас-Милнер») это алгоритм для вывода типов значений на основании того, как они используются. Буквально, он формализует интуитивное представление о том, что тип может быть выведен из поддерживаемых им операций. Рассмотрим следующий код на псевдо-Scala[4]:

def foo(s: String) = s.length
 
// заметьте: без указания типов
def bar(x, y) = foo(x) + y

Просто посмотрев на определение функции bar, мы можем сказать, что ее тип должен быть (String, Int)=>Int. Это не сложно вывести. Мы просто смотрим на тело функции и видим два способоа использовать параметры x и y. x передается в foo, который ожидает String. Следовательно x должен иметь тип String для того, чтобы этот код скомпилировался. Более того, foo возвращает значение типа Int. Метод + класса Int ожидает параметр, также Int, следовательно y должен быть типа Int. Наконец, мы знаем, что + возвращает Int, а значит это и есть тип, возвращаемый bar.

Но что будет в случае, если функция foo полиморфна, и принимает несколько типов, и если операцию + имеет не только число, но и строка? И еще несколько типов? Как же тогда можно вывести тип?

Причем тут тег «haskell»? В чем проблема, когда есть классы типов?

iVS ★★★★★ ()
Ответ на: комментарий от iVS

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

В чем проблема, когда есть классы типов?

А можно поподробней?

callbackhell ()

В хаскеле нет полиморфизма в привычном виде. Зато есть тайпклассы: некоторый общий интерфейс, который может быть определён для типа. Потому сигнатура у функции с одним именем всегда одна (хоть и может быть специализирована). Например, сигнатура для (+) из тайпкласса Num такая:

(+) :: Num a => a -> a -> a

Поняв, что, например, первым аргументом нам подсунули Int, мы поймём, что второй аргумент и возвращаемое значение имеют тот же тип Int (типизация строгая, неявных преобразований нет). Если же у нас недостаточно данных для того, чтобы понять, какой именно тип используется в качестве аргумента, то выведется общий тип:

foo a b = a + b :: Num a => a -> a -> a

По скале не спец, но, вроде, там так же.

devsdc ★★ ()
Ответ на: комментарий от callbackhell

Ну, например, тот же Num (не весь) из моего сообщения выше:

class Num a where
  (+) :: a -> a -> a
  (-) :: a -> a -> a

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

instance Num Int where
  (+) = foo
  (-) = bar

После этого любые функции, которые требуют какое-то общее число (а в хаскеле часто всё в общем виде пишут), могут работать с твоим типом.

devsdc ★★ ()
Ответ на: комментарий от devsdc

В хаскеле нет полиморфизма в привычном виде. Зато есть тайпклассы: некоторый общий интерфейс, который может быть определён для типа.

Это называется ad-hoc polymorphism.

hateyoufeel ★★★★★ ()
Ответ на: комментарий от devsdc

В хаскеле нет полиморфизма в привычном виде.

Да ну?

KblCb ★★★★★ ()

Но что будет в случае, если функция foo полиморфна, и принимает несколько типов

Можно переформулировать: функция foo принимает параметр, который может принимать значения из нескольких типов. Т.е. мы вводим операцию над типами «или» и создаёт новый анонимный тип, например `String|Int`. Т.е. `def foo(s: String|Int)`. То, что в реальном синтаксисе обычно идёт несколько объявлений foo, сути не меняет, можно считать, что это такой сахар.

и если операцию + имеет не только число, но и строка? И еще несколько типов? Как же тогда можно вывести тип?

Для операции мы вводим опять же анонимный тип, который объединяет все типы, имеющие оператор «+». Аналогично можно определять типы, имеющие метод с определённым именем. Т.е. в результате компилятор выведет что-то вроде `def bar(x: Int|String, y: {has operator+()})`.

Правда, скорее всего, нам подойдёт не каждый оператор «+», а только тот, который принимает справа Int (у нас же foo возвращает Int). И компилятор этот факт, конечно, тоже должен вывести.

Legioner ★★★★★ ()
Последнее исправление: Legioner (всего исправлений: 1)
Ответ на: комментарий от Legioner

Т.е. в результате компилятор выведет что-то вроде `def bar(x: Int|String, y: {has operator+()})`.

В случае Haskell анонимных типов быть не может. Каждый тип или конкретный тип или класс типов (явно определённый, с явно определёнными экземплярами). А при выполнении с конкретными параметрами полиморфная функция обязана выбрать конкретный экземпляр.

def bar(x: Int|String, y: {has operator+()})

Такое я только в Typed Racket видел:

(: bar (-> (U Int String) 
       (Instance (Class [+ (-> Number Number)])) 
       Int)

Но автовывода для функций там нет. Только для выражений.

monk ★★★★★ ()

Читаю про вывод типов

Только проблема в том что в хаскеле уже давно не Хиндли-Милнер.

Когда читаешь по системе типов современного хаскеля, хочется схватиться за голову и заорать: «Нет е..ие инопланетяние! Только не мой мозг!!!».

А комментарий сторонних наблюдателей: «Эй, чувак, у тебя в PDF-ридере шрифты слетели!». Счастливчики...

А решением обозначенной тобой проблемы стали тайпклассы. Самое первое расширение системы типов для хаскеля.

Macil ★★★★★ ()

Но что будет в случае, если функция foo полиморфна, и принимает несколько типов, и если операцию + имеет не только число, но и строка? И еще несколько типов? Как же тогда можно вывести тип?

Надо же anonimous, опять решил, что он что-то понял и снова задал тупой вопрос.
А по теме: есть два простых способа решения этой проблемы. Первый - как это УЖЕ РЕШЕНО в haskell. Второй - как это УЖЕ РЕШЕНО в ocaml.

Aswed ★★★★★ ()
Вы не можете добавлять комментарии в эту тему. Тема перемещена в архив.