Типы

0

0

Есть типы. Типом считается выражение вида:
1. t
2. (T1) -> (T2)
где t - type variable, T1 и T2 - любые типы. Скобки можно опускать, если выражение не становится двусмысленным. Операция -> считается правоассоциативной. Тип (a -> b) означает функцию, преобразующую экземпляры типа a в экземпляры типа b. Функции нескольких аргументов записываются, так (пусть нам нужно записать функцию двух аргументов f(A,B), где A имеет тип a, B имеет тип b, а результат имеет тип c):
a -> (b -> c),
или a -> b -> c.

Как проще всего проверить эквивалентность типов? Типы считаются эквивалентными, если один тип можно получить из другого путём переобозначения type variables, и наоборот. Например, типы (a -> b -> a) и (b -> a -> b) - эквивалентны. Я подозреваю, что можно придумать преобразование, которое бы приводило любой тип к некоторой нормальной форме. Если нормальные формы совпадают, то типы эквиваленты. Так ли это?

Как проще всего проверить приводимость типов? Тип a считаются приводимым к типу b, если экземпляр типа a является экземпляром типа b. Например, типы (a -> b -> a), (a -> Int), (a -> a), ((a -> b) -> (b -> a)) приводим к типу (a -> b).

Подозреваю, что эти задачи должны просто решаться с помощью теории графов.

Ссылка

←	Изощрённый вопрос по ant

как считать все значения из cha

→

То что ты хочешь сделать по уму называется унификацией термов (term unification). Погугли на этот счет или посмотри как это сделано в прологе. Хотя в прологе унификация достаточно обрезанная, но в целом идея должна быть понятна.

Burbaka ★★
(10.11.07 17:37:07 MSK)

Ссылка

>Типы считаются эквивалентными, если один тип можно получить из другого путём переобозначения type variables, и наоборот.

Например пройти выражение слева на право нумеруя переменные. Первая встреченная v1, зетем v2, если переменная пронумерованна, то заменяем на уже присвоенный номер. После этого эквивалентность превращается в равенство.

На языке унификации - типы эквивалентны, если унифицирующая подстановка переименовывает переменные не склеивая их.

>Как проще всего проверить приводимость типов? Тип a считаются приводимым к типу b, если экземпляр типа a является экземпляром типа b. Например, типы (a -> b -> a), (a -> Int), (a -> a), ((a -> b) -> (b -> a)) приводим к типу (a -> b).

Другими словами выражение a приводим к b, если тип, к которому они приводятся унификацией эквивалентен а.

Унификация вещь не сложная. Для двух выражений E1 E2 может получится так, что существуют некоторые подстановки s1 s2, которые приводя их к одинаковому E3. Оказывается, что если существует хотя бы одна пара, по среди их всех есть универсальные u1, u2, E0, такие что E1[u1] = E0 E2[u2] = E0, и для любых s1 s2, таких что E1[s1] = E3 и E2[s2] = E3 существует подстановка s, такая что E0[s] = E3.

Запись E[s] - результат применения подстановки s к E.

Доказывается несложно, индукцией по построению термов. Если оба терма переменные, u1, u2 - заменяет их на одну и туже. Если один терм вида E1 = (F t1 t2 t3 .. ), а другой E2=v переменная, то, если E1 содержит свободное вхождение v, то унификатора не существует, если нет, то u2 заменяет v на E1. И наконец если они оба имею вид (F1 t1 t2 t3...) (F2 t1 t2 t3...), то Если F1 != F2, то унификатора не существует, если F1=F2, то унифицируем все по порядку.

Ну и конечно a->b это сокращенно (-> a b)

ival ★★
(11.11.07 14:43:52 MSK)

Алгоритм Хиндли-Милнера?

karma
(11.11.07 18:53:01 MSK)

Ответ на: комментарий от karma 11.11.07 18:53:01 MSK

> Алгоритм Хиндли-Милнера?

ребята, я хоть и не знаю алгоритм Хиндли-Милнера, но задача топикстартера в его постановке настолько тривиальна, что это даже язык не повернется назвать алгоритмом, да еще и с несколькими именами.

dilmah ★★★★★
(11.11.07 19:04:05 MSK)