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

Я делал свой обычный "Прочитайте главу LYAH перед сном", чувствуя, что мой мозг расширяется с каждым образцом кода. На этом этапе я убедился, что понял основную остроту Haskell, и теперь мне просто нужно было понять стандартные библиотеки и классы классов, чтобы я мог начать писать реальное программное обеспечение.

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

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

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

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

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

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

a -> ?

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

a -> *

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

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

Ответ 1

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

Вид (- > )

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

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

Как выглядит ситуация на зависимом языке

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

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

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

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

Теперь мы можем написать функцию, которая принимает значение и возвращает тип. Ниже приведена функция, которая принимает натуральное число n и тип, и выполняет итерацию конструктора List n, примененного к этому тип. (В Agda, [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

Вне видов: Черепахи на всем пути вниз

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

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

И на самом деле, есть целая иерархия из них! Набор - это тип "маленькие" типы: типы данных в haskell. Но тогда мы имеем Set1, Set2, Set3 и т.д. Set1 - тип типов, который упоминает Set. Эта иерархия заключается в том, чтобы избежать несоответствий, таких как Girard's Парадокс.

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

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

В Agda типы могут зависеть от значений, а функции могут возвращать типы, как показано выше, и у нас также была иерархия типы. Систематическое исследование различных систем лямбда исчисления более подробно исследуются в системах чистого типа. Хороший ссылка Lambda Calculi with Types от Barendregt, где PTS представлены на стр. 96, и многие примеры на стр. 99 и далее. Вы также можете прочитать больше о лямбда-кубе там.

Ответ 2

Во-первых, тип ?? -> ? -> * является расширением GHC. ? и ?? находятся здесь, чтобы иметь дело с unboxed типами, которые ведут себя иначе, чем просто * (который, насколько мне известно, должен быть помещен в коробку). Таким образом, ?? может быть любым нормальным типом или unboxed типом (например, Int#); ? может быть либо из тех, либо из незагруженного кортежа. Здесь есть дополнительная информация: Haskell Weird Kinds: Вид (- > ) есть? → ? → *

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

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

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

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

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