Что такое комбинаторный логический эквивалент теории интуиционистских типов?
Недавно я закончил университетский курс, в котором участвовали Хаскелл и Агда (зависимый типизированный функциональный язык программирования), и мне было интересно, можно ли заменить в них лямбда-исчисление комбинаторной логикой. В Haskell это представляется возможным с помощью комбинаторов S и K, что делает его бессмысленным. Мне было интересно, что эквивалент был для Агды. Т.е. можно ли сделать зависимый тип функционального языка программирования эквивалентным Agda без использования каких-либо переменных?
Кроме того, возможно ли как-то заменить количественную оценку комбинаторами? Я не знаю, является ли это совпадением, но универсальная квантификация, например, делает сигнатуру типа похожей на лямбда-выражение. Есть ли способ удалить универсальное количественное определение из сигнатуры типа без изменения его значения? Например, в:
forall a : Int -> a < 0 -> a + a < a
Можно ли выразить то же самое, не используя форму?
2 ответа
Поэтому я подумал об этом немного больше и добился определенного прогресса. Вот первая попытка кодирования Мартина-Лёфа, восхитительно простая (но непоследовательная) Set : Set система в комбинаторном стиле. Это не хороший способ закончить, но это самое легкое место для начала. Синтаксис этой теории типов - это просто лямбда-исчисление с аннотациями типов, Pi-типами и множеством юниверсов.
Теория типа цели
Ради полноты я представлю правила. Достоверность контекста просто говорит, что вы можете создавать контексты из пустых, добавляя свежие переменные, населяющие Set s.
G |- valid G |- S : Set
-------------- ----------------------------- x fresh for G
. |- valid G, x:S |- valid
И теперь мы можем сказать, как синтезировать типы для терминов в любом данном контексте и как изменить тип чего-либо в соответствии с вычислительным поведением содержащихся в нем терминов.
G |- valid G |- S : Set G |- T : Pi S \ x:S -> Set
------------------ ---------------------------------------------
G |- Set : Set G |- Pi S T : Set
G |- S : Set G, x:S |- t : T x G |- f : Pi S T G |- s : S
------------------------------------ --------------------------------
G |- \ x:S -> t : Pi S T G |- f s : T s
G |- valid G |- s : S G |- T : Set
-------------- x:S in G ----------------------------- S ={beta} T
G |- x : S G |- s : T
В небольшом отличии от оригинала я сделал лямбду единственным оператором привязки, поэтому вторым аргументом Pi должна быть функция, вычисляющая способ, которым тип возвращаемого значения зависит от ввода. По соглашению (например, в Agda, но, к сожалению, не в Haskell) область действия лямбды расширяется настолько, насколько это возможно, поэтому вы можете оставить абстракции без скобок, когда они являются последним аргументом оператора более высокого порядка: вы можете видеть, что я сделал что с Пи. Ваш Агда тип (x : S) -> T становится Pi S \ x:S -> T,
(Отступление. Аннотации типов в лямбда-выражениях необходимы, если вы хотите иметь возможность синтезировать тип абстракций. Если вы переключаетесь на проверку типов в качестве своего modus operandi, вам все равно нужны аннотации для проверки типа бета-переопределения, например (\ x -> t) s, так как вы не можете угадать типы частей из целого. Я советую современным дизайнерам проверять типы и исключать бета-переопределения из самого синтаксиса.)
(Отступление. Эта система противоречива как Set:Set позволяет кодировать множество "парадоксов лжеца". Когда Мартин-Лёф предложил эту теорию, Жирар послал ему кодирование её в своей непоследовательной Системе U. Последующий парадокс из-за Хюркенса - самая изощренная токсическая конструкция, которую мы знаем.)
Синтаксис и нормализация комбинатора
В любом случае, у нас есть два дополнительных символа, Pi и Set, поэтому мы могли бы, возможно, управлять комбинаторным переводом с помощью S, K и двух дополнительных символов: я выбрал U для юниверса и P для продукта.
Теперь мы можем определить нетипизированный комбинаторный синтаксис (со свободными переменными):
data SKUP = S | K | U | P deriving (Show, Eq)
data Unty a
= C SKUP
| Unty a :. Unty a
| V a
deriving (Functor, Eq)
infixl 4 :.
Обратите внимание, что я включил средства для включения свободных переменных, представленных типом a в этом синтаксисе. Помимо того, что рефлекс с моей стороны (каждый синтаксис, достойный этого имени, является бесплатной монадой с return встраивание переменных и >>= выполнение замены), будет удобно представлять промежуточные этапы в процессе преобразования терминов с привязкой к их комбинаторной форме.
Вот нормализация:
norm :: Unty a -> Unty a
norm (f :. a) = norm f $. a
norm c = c
($.) :: Unty a -> Unty a -> Unty a -- requires first arg in normal form
C S :. f :. a $. g = f $. g $. (a :. g) -- S f a g = f g (a g) share environment
C K :. a $. g = a -- K a g = a drop environment
n $. g = n :. norm g -- guarantees output in normal form
infixl 4 $.
(Упражнение для читателя состоит в том, чтобы определить тип точно для нормальных форм и отточить типы этих операций.)
Представление Теории Типа
Теперь мы можем определить синтаксис для нашей теории типов.
data Tm a
= Var a
| Lam (Tm a) (Tm (Su a)) -- Lam is the only place where binding happens
| Tm a :$ Tm a
| Pi (Tm a) (Tm a) -- the second arg of Pi is a function computing a Set
| Set
deriving (Show, Functor)
infixl 4 :$
data Ze
magic :: Ze -> a
magic x = x `seq` error "Tragic!"
data Su a = Ze | Su a deriving (Show, Functor, Eq)
Я использую представление индекса де Брюйна в манере Беллегарда и Хука (как популяризировали Берд и Патерсон). Тип Su a имеет еще один элемент, чем a, и мы используем его как тип свободных переменных под связывателем, с Ze в качестве новой связанной переменной и Su x будучи сдвинутым представлением старой свободной переменной x,
Перевод терминов в комбинаторы
И после этого мы получаем обычный перевод, основанный на абстракции скобок.
tm :: Tm a -> Unty a
tm (Var a) = V a
tm (Lam _ b) = bra (tm b)
tm (f :$ a) = tm f :. tm a
tm (Pi a b) = C P :. tm a :. tm b
tm Set = C U
bra :: Unty (Su a) -> Unty a -- binds a variable, building a function
bra (V Ze) = C S :. C K :. C K -- the variable itself yields the identity
bra (V (Su x)) = C K :. V x -- free variables become constants
bra (C c) = C K :. C c -- combinators become constant
bra (f :. a) = C S :. bra f :. bra a -- S is exactly lifted application
Ввод комбинаторов
Перевод показывает, как мы используем комбинаторы, что дает нам представление о том, какими должны быть их типы. U а также P это просто конструкторы множеств, поэтому, для написания непереведенных типов и разрешения "нотации Agda" для Pi, мы должны иметь
U : Set
P : (A : Set) -> (B : (a : A) -> Set) -> Set
K комбинатор используется для поднятия значения некоторого типа A к постоянной функции над некоторым другим типом G,
G : Set A : Set
-------------------------------
K : (a : A) -> (g : G) -> A
S комбинатор используется для подъема приложений над типом, от которого могут зависеть все части.
G : Set
A : (g : G) -> Set
B : (g : G) -> (a : A g) -> Set
----------------------------------------------------
S : (f : (g : G) -> (a : A g) -> B g a ) ->
(a : (g : G) -> A g ) ->
(g : G) -> B g (a g)
Если вы посмотрите на тип S вы увидите, что оно точно определяет контекстно- зависимое правило приложения теории типов, поэтому оно подходит для отражения конструкции приложения. Это его работа!
Тогда у нас есть приложение только для закрытых вещей
f : Pi A B
a : A
--------------
f a : B a
Но есть загвоздка. Я написал типы комбинаторов в обычной теории типов, а не в комбинаторной теории типов. К счастью, у меня есть машина, которая сделает перевод.
Комбинаторная система типов
---------
U : U
---------------------------------------------------------
P : PU(S(S(KP)(S(S(KP)(SKK))(S(KK)(KU))))(S(KK)(KU)))
G : U
A : U
-----------------------------------------
K : P[A](S(S(KP)(K[G]))(S(KK)(K[A])))
G : U
A : P[G](KU)
B : P[G](S(S(KP)(S(K[A])(SKK)))(S(KK)(KU)))
--------------------------------------------------------------------------------------
S : P(P[G](S(S(KP)(S(K[A])(SKK)))(S(S(KS)(S(S(KS)(S(KK)(K[B])))(S(KK)(SKK))))
(S(S(KS)(KK))(KK)))))(S(S(KP)(S(S(KP)(K[G]))(S(S(KS)(S(KK)(K[A])))
(S(S(KS)(KK))(KK)))))(S(S(KS)(S(S(KS)(S(KK)(KP)))(S(KK)(K[G]))))
(S(S(KS)(S(S(KS)(S(KK)(KS)))(S(S(KS)(S(S(KS)(S(KK)(KS)))
(S(S(KS)(S(KK)(KK)))(S(KK)(K[B])))))(S(S(KS)(S(S(KS)(S(KK)(KS)))(S(KK)(KK))))
(S(KK)(KK))))))(S(S(KS)(S(S(KS)(S(KK)(KS)))(S(S(KS)(S(KK)(KK)))
(S(S(KS)(KK))(KK)))))(S(S(KS)(S(S(KS)(S(KK)(KS)))(S(KK)(KK))))(S(KK)(KK)))))))
M : A B : U
----------------- A ={norm} B
M : B
Итак, вот оно, во всей его нечитаемой славе: комбинационная презентация Set:Set!
Там все еще есть небольшая проблема. Синтаксис системы не дает возможности угадать G, A а также B параметры для S и аналогично для K Просто из условия. Соответственно, мы можем проверять типизацию производных алгоритмически, но мы не можем просто проверять термины комбинатора типов, как мы могли бы с исходной системой. Что может сработать, так это потребовать, чтобы входные данные для проверки типов содержали аннотации типов при использовании S и K, эффективно записывая вывод. Но это еще одна банка червей...
Это хорошее место, чтобы остановиться, если вы достаточно заинтересованы, чтобы начать. Остальное "за кадром".
Генерация типов комбинаторов
Я сгенерировал эти комбинаторные типы, используя перевод абстракции в скобках из соответствующих терминов теории типов. Чтобы показать, как я это сделал, и сделать этот пост не совсем бессмысленным, позвольте мне предложить мое оборудование.
Я могу написать типы комбинаторов, полностью абстрагированных от их параметров, следующим образом. Я использую свой удобный pil функция, которая комбинирует Pi и лямбду, чтобы избежать повторения типа домена, и довольно услужливо позволяет мне использовать функциональное пространство Haskell для связывания переменных. Возможно, вы можете почти прочитать следующее!
pTy :: Tm a
pTy = fmap magic $
pil Set $ \ _A -> pil (pil _A $ \ _ -> Set) $ \ _B -> Set
kTy :: Tm a
kTy = fmap magic $
pil Set $ \ _G -> pil Set $ \ _A -> pil _A $ \ a -> pil _G $ \ g -> _A
sTy :: Tm a
sTy = fmap magic $
pil Set $ \ _G ->
pil (pil _G $ \ g -> Set) $ \ _A ->
pil (pil _G $ \ g -> pil (_A :$ g) $ \ _ -> Set) $ \ _B ->
pil (pil _G $ \ g -> pil (_A :$ g) $ \ a -> _B :$ g :$ a) $ \ f ->
pil (pil _G $ \ g -> _A :$ g) $ \ a ->
pil _G $ \ g -> _B :$ g :$ (a :$ g)
Определив их, я извлек соответствующие открытые подтермы и провел их через перевод.
A de Bruijn Набор инструментов для кодирования
Вот как построить pil, Во-первых, я определяю класс Fin ите наборы, используемые для переменных. У каждого такого набора есть сохраняющий конструктор emb добавляя в набор выше, плюс новый top элемент, и вы можете отличить их друг от друга: embd Функция сообщает вам, если значение находится в изображении emb,
class Fin x where
top :: Su x
emb :: x -> Su x
embd :: Su x -> Maybe x
Мы можем, конечно, создать экземпляр Fin за Ze а также Suc
instance Fin Ze where
top = Ze -- Ze is the only, so the highest
emb = magic
embd _ = Nothing -- there was nothing to embed
instance Fin x => Fin (Su x) where
top = Su top -- the highest is one higher
emb Ze = Ze -- emb preserves Ze
emb (Su x) = Su (emb x) -- and Su
embd Ze = Just Ze -- Ze is definitely embedded
embd (Su x) = fmap Su (embd x) -- otherwise, wait and see
Теперь я могу определить "меньше или равно" с помощью операции ослабления.
class (Fin x, Fin y) => Le x y where
wk :: x -> y
wk функция должна включать элементы x как самые большие элементы y так, чтобы лишние вещи в y меньше, и, таким образом, в терминах индекса де Брюйна, связаны более локально.
instance Fin y => Le Ze y where
wk = magic -- nothing to embed
instance Le x y => Le (Su x) (Su y) where
wk x = case embd x of
Nothing -> top -- top maps to top
Just y -> emb (wk y) -- embedded gets weakened and embedded
И как только вы разберетесь с этим, небольшая радуга занимает все остальное.
lam :: forall x. Tm x -> ((forall y. Le (Su x) y => Tm y) -> Tm (Su x)) -> Tm x
lam s f = Lam s (f (Var (wk (Ze :: Su x))))
pil :: forall x. Tm x -> ((forall y . Le (Su x) y => Tm y) -> Tm (Su x)) -> Tm x
pil s f = Pi s (lam s f)
Функция высшего порядка не просто дает вам термин, представляющий переменную, она дает вам перегруженную вещь, которая становится правильным представлением переменной в любой области видимости переменной. То есть тот факт, что я сталкиваюсь с проблемой различения различных областей по типу, дает типографской проверке типов в Haskell достаточно информации для вычисления сдвига, необходимого для перевода в представление де Брюина. Зачем держать собаку и лаять себя?
Я думаю, что "Bracket Abstraction" работает также для зависимых типов при некоторых обстоятельствах. В разделе 5 следующей статьи вы найдете несколько типов K и S:
Возмутительные, но значимые совпадения
Зависимый типобезопасный синтаксис и оценка
Конор МакБрайд, Университет Стратклайда, 2010
Преобразование лямбда-выражения в комбинаторное выражение примерно соответствует преобразованию доказательства естественного вывода в доказательство типа Гильберта.