Вы затрагиваете так много интересных моментов в своем вопросе, что я боюсь, что это будет длинный ответ :)
Вид (->)
Тип (->) - это * -> * -> *, если не принимать во внимание вставки GHC boxity. Но цикличности не происходит, -> в виде (->) — это добрые стрелки, а не функциональные стрелки. Действительно, чтобы их различать, стрелки типа можно было бы записать как (=>), а тогда вид (->) будет * => * => *.
Мы можем рассматривать (->) как конструктор типа или, может быть, скорее как оператор типа. Точно так же (=>) можно рассматривать как добрый оператор, и, как вы предлагаете в своем вопросе, нам нужно подняться на один «уровень» вверх. Мы вернемся к этому позже в разделе За пределами видов, но сначала:
Как ситуация выглядит на зависимо типизированном языке
Вы спрашиваете, как будет выглядеть сигнатура типа для функции, которая принимает значение и возвращает тип. Это невозможно сделать в Haskell: функции не могут возвращать типы! Вы можете имитировать это поведение, используя классы типов и семейства типов, но давайте для иллюстрации изменим язык на язык с зависимой типизацией Агда. Это язык с синтаксисом, похожим на Haskell, где жонглирование типами со значениями является второй натурой.
Чтобы было с чем работать, мы определяем тип данных натуральных чисел для удобства унарного представления, как в арифметике Пеано. . Типы данных записываются в стиле GADT:
data Nat : Set where
Zero : Nat
Succ : Nat -> Nat
Set эквивалентен * в Haskell, «типу» всех (маленьких) типов, таких как натуральные числа. Это говорит нам о том, что тип Nat равен Set, тогда как в Haskell у Nat не будет типа, у него будет вид, а именно *. В Агде нет видов, но все имеет тип.
Теперь мы можем написать функцию, которая принимает значение и возвращает тип. Ниже приведена функция, которая принимает натуральное число 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
Вне видов: черепахи на всем пути вниз
Как было обещано выше, все в Agda имеет тип, но тогда тип _=>_ должен иметь тип! Это касается вашего вопроса о сортах, которые, так сказать, на один уровень выше Set (видов). В Агде это называется Set1:
FunType : Set1
FunType = Set -> Set -> Set
А на самом деле их целая иерархия! Set — это тип «маленьких» типов: типов данных в haskell. Но тогда у нас есть Set1, Set2, Set3 и так далее. Set1 — это тип типов, в котором упоминается Set. Эта иерархия предназначена для того, чтобы избежать несоответствий, таких как парадокс Жирара.
Как замечено в вашем вопросе, -> используется для типов и видов в Haskell, и одна и та же нотация используется для функционального пространства на всех уровнях в Agda. Это следует рассматривать как встроенный оператор типа, а конструкторы — это лямбда-абстракции (или определения функций). Эта иерархия типов аналогична настройке в System F omega, а дополнительную информацию можно найти в последующие главы книги Типы Пирса и языки программирования.
Системы чистого типа
В Agda типы могут зависеть от значений, а функции могут возвращать типы, как показано выше, и у нас также была иерархия типов. Систематическое исследование различных систем лямбда-исчислений более подробно исследуется в Pure Type Systems. Хороший справочник — Лямбда-исчисления с типами от Barendregt, где PTS — это представлено на странице 96, и множество примеров на странице 99 и далее. Вы также можете прочитать больше о лямбда-кубе там.
person
danr
schedule
31.01.2012
