Функции не просто имеют типы: они являются типами. И виды. И сортирует. Помогите вернуть взорванный разум обратно

Question

Я выполнял свою обычную процедуру «Прочитайте главу ЛЯХ перед сном», чувствуя, что мой мозг расширяется с каждым образцом кода.В этот момент я был убежден, что понял основную ценность Haskell, и теперь мне просто нужно было понять стандартные библиотеки и классы типов, чтобы я мог начать писать настоящее программное обеспечение.

Итак, я читал главу о аппликативных функторах, когда книга внезапно заявила, что функции не просто имеют типы, они являются типами и могут рассматриваться как таковыенапример, делая их экземплярами классов типов).(->) - это конструктор типов, как и любой другой.

Мой ум снова взорвался, и я сразу же вскочил с кровати, загрузил компьютер, пошел в GHCi и обнаружил следующее:

Prelude> :k (->)
(->) :: ?? -> ? -> *

• Что на земле это значит?
• Если (->) является конструктором типа, каковы конструкторы значений?Я могу предположить, но не знаю, как определить его в традиционном формате data (->) ... = ... | ... | ....Это достаточно просто сделать с любым другим конструктором типов: data Either a b = Left a | Right b.Я подозреваю, что моя неспособность выразить это в этой форме связана с чрезвычайно странной сигнатурой типа.
• На что я только что наткнулся?Типы с более высоким родом имеют добрые подписи типа * -> * -> *.Если подумать ... (->) тоже появляется в подписи!Значит ли это, что это не только конструктор типа, но и конструктор типа?Связано ли это с вопросительными знаками в сигнатуре типа?

Я где-то читал (если бы я мог найти это снова, Google не сможет меня) о возможности произвольно расширять системы типов, переходя от значений,к типам ценностей, к типам типов, к типам видов, к чему-то другому, к чему-то другому, к чему-то другому, и так далее, навсегда.Отражено ли это в доброй подписи для (->)?Потому что я также натолкнулся на понятие лямбда-куба и исчисления конструкций, не тратя время на то, чтобы по-настоящему исследовать их, и, если я правильно помню, можно определить функции, которые принимают типы и возвращают типы, принимают значения и возвращают значения, принимать типы и возвращать значения, а также принимать значения, которые возвращают типы.

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

a -> ?

или, возможно,

a -> *

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

Первый пример лучше выражает функцию, тип которой выходит за рамки сигнатуры типа: «функция, которая принимает значение типа a ивозвращает что-то, что не может быть выражено как тип. "

Answer 1

Вы затронули так много интересных вопросов в своем вопросе, поэтому я боюсь, это будет длинный ответ:)

Вид (->)

Тип (->) равен * -> * -> *, если мы не примем во внимание размерность GHC Вставки. Но округлости не происходит, -> в виды (->) являются добрыми стрелками, а не функциональными стрелками. Действительно, чтобы различать их добрые стрелки можно записать как (=>), а затем вид (->) равен * => * => *.

Мы можем рассматривать (->) как конструктор типа или, скорее, тип оператор. Точно так же (=>) можно рассматривать как оператор вида , и как вы предлагаете в своем вопросе, нам нужно подняться на один уровень выше. Мы Вернемся к этому позже в разделе Beyond Kinds , но сначала:

Как выглядит ситуация на языке с типизированной зависимостью

Вы спрашиваете, как выглядит сигнатура типа для функции, которая принимает значение и возвращает тип. Это невозможно сделать в Haskell: функции не могут возвращать типы! Вы можете смоделировать это поведение, используя классы типов и семейства типов, но давайте для иллюстрации изменим язык на зависимо типизированный язык Agda . Это язык с похожим синтаксисом, как у Haskell, где смешиваются типы со значениями это вторая натура.

Чтобы было с чем работать, мы определяем тип данных естественного числа, для удобства в одинарном представлении как в Арифметика Пеано . Типы данных написаны в GADT стиль:

data Nat : Set where
    Zero : Nat
    Succ : Nat -> Nat

Set эквивалентен * в Haskell, "типе" всех (маленьких) типов, такие как натуральные числа. Это говорит нам о том, что тип Nat Set, тогда как в Хаскеле у Ната не было бы типа, он имел бы вид, а именно *. В Агде нет видов, но все имеет тип.

Теперь мы можем написать функцию, которая принимает значение и возвращает тип. Ниже приведена функция, которая принимает натуральное число n и тип, и делает итерации List конструктора n, примененного к этому тип. (В Агде [a] обычно пишется List a)

listOfLists : Nat -> Set -> Set
listOfLists Zero     a = a
listOfLists (Succ n) a = List (listOfLists n a)

Некоторые примеры:

listOfLists Zero               Bool = Bool
listOfLists (Succ Zero)        Bool = List Bool
listOfLists (Succ (Succ Zero)) Bool = List (List Bool)

Теперь мы можем сделать функцию map, которая работает на listsOfLists. Нам нужно взять натуральное число, которое является числом итераций конструктора списка. Базовые случаи, когда число Zero, тогда listOfList - это просто тождество, и мы применяем функцию. Другой - пустой список, и пустой список возвращается. Случай шага - небольшой шаг, включающий: мы применяем mapN к голове из списка, но это на один слой меньше вложенности, и mapN к остальной части списка.

mapN : {a b : Set} -> (a -> b) -> (n : Nat) ->
       listOfLists n a -> listOfLists n b
mapN f Zero     x         = f x
mapN f (Succ n) []        = []
mapN f (Succ n) (x :: xs) = mapN f n x :: mapN f (Succ n) xs

В типе mapN аргумент Nat называется n, поэтому остальные тип может зависеть от этого. Так что это пример типа, который зависит от значения.

_{Как примечание, есть также две другие именованные переменные здесь, а именно первые аргументы a и b типа Set. Тип переменные неявно повсеместно определены количественно в Haskell, но здесь нам нужно разобрать их и указать их тип, а именно Set. Скобки предназначены для того, чтобы сделать их невидимыми в определение, так как они всегда выводимы из других аргументов.}

Набор абстрактный

Вы спрашиваете, каковы конструкторы (->). Стоит отметить одну вещь является то, что Set (как и * в Haskell) является абстрактным: вы не можете образец соответствия на нем. Так что это Агда незаконно:

cheating : Set -> Bool
cheating Nat = True
cheating _   = False

Опять же, вы можете смоделировать сопоставление с образцом на конструкторах типов в Haskell, использующий семейства типов, один канонический пример дан на Блог Брента Йорги . Можем ли мы определить -> в Агде? Так как мы можем возвращать типы из функции, мы можем определить собственную версию -> следующим образом:

_=>_ : Set -> Set -> Set
a => b = a -> b

(инфиксные операторы пишутся _=>_, а не (=>)) определение имеет очень мало содержания, и очень похоже на введите синоним в Haskell:

type Fun a b = a -> b

За пределами видов: Черепахи внизу

Как и было обещано выше, все в Агде имеет тип, но потом тип из _=>_ должен иметь тип! Это касается вашей точки зрения о родах, то есть, так сказать, на один уровень выше множества (видов). В Агде это называется Set1:

FunType : Set1
FunType = Set -> Set -> Set

И действительно, их целая иерархия! Указан тип «малые» типы: типы данных в haskell. Но тогда у нас есть Set1, Set2, Set3 и т. Д. Set1 это тип типов, который упоминает Set. Эта иерархия призвана избежать несоответствий, таких как у Жирара Парадокс.

Как отмечено в вашем вопросе, -> используется для типов и видов в Haskell, и то же самое обозначение используется для функционального пространства вообще уровни в Агде. Это должно рассматриваться как встроенный оператор типа, и конструкторы лямбда-абстракция (или функция определения). Эта иерархия типов аналогична настройке в Система F омега и более информация может быть найдена в последующих главах Типы Пирса и языки программирования .

Системы чистого типа

В Agda типы могут зависеть от значений, а функции могут возвращать типы, как показано выше, и у нас также была иерархия типы. Систематическое исследование различных систем лямбда исчисления более подробно исследованы в Pure Type Systems. Хороший ссылка Лямбда-исчисления с типами Барендрегом, где PTS представлен на стр. 96, и множество примеров на стр. 99 и далее. Вы также можете прочитать больше о лямбда-кубе там.

Answer 2

Во-первых, тип ?? -> ? -> * является специфичным для GHC расширением.? и ?? предназначены только для распакованных типов, которые ведут себя не так, как * (насколько я знаю, их нужно упаковать).Таким образом, ?? может быть любого нормального типа или типа без коробки (например, Int#);? может быть как тем, так и неупакованным кортежем.Больше информации здесь: Хаскель. Странные виды: Вид (->) - это ??->?-> *

Я думаю, что функция не может вернуть распакованный тип, потому что функции ленивы.Поскольку ленивое значение является либо значением, либо thunk, оно должно быть упаковано.В штучной упаковке просто означает, что это указатель, а не просто значение: это похоже на Integer() против int в Java.

Поскольку вы, вероятно, не собираетесь использовать распакованные типы в коде уровня LYAH, вы можетепредставьте себе, что тип -> это просто * -> * -> *.

Поскольку ? и ?? в основном являются просто более общей версией *, они не имеют ничего общего с сортировками иличто-нибудь в этом роде.

Однако, поскольку -> является просто конструктором типов, вы можете применить его частично;например, (->) e является экземпляром Functor и Monad.Выяснение того, как написать эти примеры, является хорошим упражнением для разминки ума.

Что касается конструкторов значений, то они должны быть просто лямбдами (\ x ->) или объявлениями функций.Поскольку функции так важны для языка, они получают собственный синтаксис.