Нахождение правильного типа функции в стандарте ML - PullRequest
Новая
       10

Нахождение правильного типа функции в стандарте ML

0 голосов
/ 26 января 2019

Обычно тесты, содержащие вопрос о SML, содержат вопросы, в которых вас просят найти сигнатуру / тип функции.

Например - Какой тип следующей функции: 

fun foo f g x y = f (f x (g x) y) y;

Решение: 

val foo = fn : ('a -> 'b -> 'b -> 'a) -> ('a -> 'b) -> 'a -> 'b -> 'b -> 'a

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

Ответы [ 2 ]

0 голосов
/ 30 января 2019

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

  • Пример Ionuț G. Stan срезает очень мало углов и имеет довольно многословную запись.Этот механический подход очень безопасен, объясняет все и занимает некоторое время.

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

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

0 голосов
/ 27 января 2019

Начните с того, что вы знаете, затем немного разберитесь здесь и немного там, пока не останется неизвестных.

Вот одна из возможностей:

Вызовите неизвестные типы FOO,F, G, X и Y соответственно.

Затем найдите что-то маленькое и простое и начните присваивать типы. 

(g x)

- это, безусловно, приложениефункции с одним аргументом.
Установите X = a и G = a -> b.

Затем посмотрите на включающее выражение: 

(f x (g x) y)
   |   |
   v   v
   a   b

Такдалеко, мы знаем, что F = a -> b -> Y -> C, для некоторых C.

снова выйдем наружу: 

f (f x (g x) y) y

, так как оба x и (f x (g x) y) являются первыми аргументамиf, они должны быть одного типа a, и та же идея применима к y и (g x), давая им тип b.

Итак, F = a -> b -> b -> a и, поскольку внешнему f дается только два аргумента, тип правой части должен быть b -> a.

Таким образом 

X = a
Y = b
G = a -> b
F = a -> b -> b -> a
FOO = (a -> b -> b -> a) -> (a -> b) -> a -> b -> (b -> a)

И, так как стрелкиассоциировать справа FOO эквивалентно 

(a -> b -> b -> a) -> (a -> b) -> a -> b -> b -> a
...