Функции не просто имеют типы: Они являются типами. И виды. И сорта. Помогите собрать взорванный мозг воедино
Я занимался своей обычной рутиной "Прочитал главу LYAH перед сном", чувствуя, как мой мозг расширяется с каждым примером кода. В этот момент я был убежден, что понял основную крутость Haskell, и теперь мне оставалось только разобраться в стандартных библиотеках и классах типов, чтобы начать писать реальные программы.
Итак, я читал главу о прикладных функторах, как вдруг книга заявила, что функции не просто имеют типы, они являются типами и могут рассматриваться как таковые (например, делая их экземплярами классов типов). (->) - это такой же конструктор типов, как и любой другой.
Мой разум был потрясен еще раз, и я немедленно вскочил с кровати, включил компьютер, зашел в GHCi и обнаружил следующее:
Prelude> :k (->)
(->) :: ?? -> ? -> *
- Что это значит?
- Если (->) - это конструктор типов, то каковы конструкторы значений? Я могу предположить, но не представляю, как определить его в традиционном
data (->) ... = ... | ... | ...формате. Это достаточно легко сделать с помощью любого другого конструктора типов:data Either a b = Left a | Right b. Я подозреваю, что моя неспособность выразить это в такой форме связана с чрезвычайно странной сигнатурой типа. - На что я только что наткнулся? Типы более высокого рода имеют сигнатуры типа
* -> * -> *. Если подумать... (->) тоже встречается в подписях видов! Значит ли это, что это не только конструктор типов, но и конструктор видов? Связано ли это с вопросительными знаками в сигнатуре типа?
Я где-то читал (жаль, что не могу найти снова, Google меня подводит) о возможности произвольно расширять системы типов, переходя от значений, к типам значений, к видам типов, к родам родов, к чему-то еще из родов, к чему-то еще из чего-то еще и так до бесконечности. Отражается ли это в сигнатуре вида для (->)? Потому что я также сталкивался с понятием лямбда-куба и исчислением конструкций, не потратив времени на их изучение, и, если я правильно помню, можно определить функции, которые принимают типы и возвращают типы, принимают значения и возвращают значения, принимают типы и возвращают значения, а также принимают значения, которые возвращают типы.
Если бы мне нужно было угадать сигнатуру типа для функции, которая принимает значение и возвращает тип, я бы, вероятно, выразил ее следующим образом:
a -> ?
или, возможно,
a -> *
Хотя я не вижу фундаментальной неизменной причины, почему второй пример не может быть легко интерпретирован как функция от значения типа a к значению типа *, где * - это просто синоним типа string или что-то в этом роде.
Первый пример лучше выражает функцию, тип которой выходит за рамки сигнатуры типа, на мой взгляд: "функция, которая принимает значение типа a и возвращает что-то, что не может быть выражено в виде типа."