Определить эффект функции по ее типу

Одним из интересных свойств системы типов Haskell (*) является то, что иногда вы можете сказать точно, что делает функция, основываясь только на ее сигнатуре типа (при условии, что не задействована unsafe IO темная магия).

Например, любая функция с сигнатурой типа a -> a должна быть функцией идентификации, а любая функция типа (a,b) -> a эквивалентна fst. В некоторых случаях вы не можете определить функцию полностью: существует бесконечное количество различных возможных функций типа a -> Int, но все они константы — все они игнорируют первый параметр.

Я нахожу это свойство захватывающим, но подозреваю, что оно применимо только к "тривиальным" функциям, таким как id и const. Я прав?

Кроме того, мои рассуждения здесь основаны только на интуиции - например, в a -> a мы "ничего не знаем" о a (в отличие от функций с ограничениями, таких как Num a => a -> a), поэтому "не можем ничего сделать" с ним, кроме как вернуть без изменений. Есть ли формальный способ справиться с такого рода вычетами?

* Я знаю, что система типов Haskell основана на системе типов Хиндли-Милнера, но я недостаточно знакома с ней, чтобы делать какие-либо предположения


haskell hindley-milner type-theory
person Benesh    schedule 24.05.2014    source источник
comment
Я не смог придумать подходящее название, и меня не устраивает текущий вариант — предложения и/или правки приветствуются. Спасибо!   -  person Benesh    schedule 24.05.2014
comment
Статья Филипа Уодлера «Теоремы» бесплатно! занимается этой темой. Я не понимаю это достаточно хорошо, чтобы написать ответ.   -  person    schedule 24.05.2014
comment
@delnan Спасибо! Вот ссылка для будущих читателей. Похоже, что для этого требуются базовые знания теории типов.   -  person Benesh    schedule 24.05.2014
comment
Возможно, это не очень полезная функция, но \x -> undefined можно присвоить сигнатуру типа a -> a.   -  person Neil Forrester    schedule 24.05.2014
comment
@NeilForrester Так может undefined, и действительно, преобразования программ, основанные на параметричности, несостоятельны при наличии такой функции, как seq. См. также Бесплатные теоремы в присутствии *seq [PDF]   -  person Rein Henrichs    schedule 24.05.2014
comment
@NeilForrester - ты прав. Однако его истинный тип AFAIK - a -> ⊥   -  person Benesh    schedule 24.05.2014
comment
@Бенеш ⊥ не является типом. ⊥ — обитатель всех типов. Его истинный тип — forall a. a -> a.   -  person Rein Henrichs    schedule 24.05.2014

Ответы (1)


arrow_upward
10
arrow_downward

Концепция, о которой вы говорите, известна как параметричность. Универсальная количественная оценка типов дает параметрический полиморфизм и свойство «единообразия», которое интуитивно представляет собой представление о том, что «мы ничего не знаем о» a в forall a. a -> a и поэтому «не можем ничего сделать» с ним, кроме как вернуть его без изменений. Свойство единообразия говорит о том, что тип f :: [a] -> [a] не зависит от типа a или, точнее, зависит от него равномерно: все, что "делают" с [a], должно быть "выполнимо" для всех вариантов a. Вадлер использует это, чтобы показать, что отображение значений в списке, а затем перестановка списка эквивалентны первой перестановке и последующему отображению.

Формальный способ работы с этими интуитивными представлениями дан, например, в Теоремы бесплатно и включает изоморфизм между типами и отношениями (фактически категория PER отношений частичной эквивалентности (per's)), который показывает, что это единообразие является универсальное свойство в категории.

Одним из интересных результатов параметричности является то, что вы можете идти «в обе стороны»: от типа к теоремам об этом типе и от типа к обитателям этого типа. Свободные теоремы Вадлера являются примером первого и Djinn, доказывающего теоремы (обитателями типа являются «доказательства» типа «теоремы»), является примером последнего.

person Rein Henrichs    schedule 24.05.2014