Ответ 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 и далее. Вы также можете прочитать больше о лямбда-кубе там.