Что такое комбинаторный логический эквивалент интуиционистской теории типов?

так что я подумал об этом немного больше и сделал некоторый прогресс. Вот первый удар по кодированию Мартина-Лефа восхитительно простой (но непоследовательный) Set : Set система в комбинаторном стиле. Это не лучший способ закончить, но это самое простое место, чтобы начать. Синтаксис этой теории типов-это просто лямбда-исчисление с аннотациями типов, Pi-типами и набором юниверсов.

Теория Целевого Типа

для полноты картины, я представлю правила. Контекст validity просто говорит, что вы можете создавать контексты из пустых, примыкая к новым переменным, населяющим 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), область лямбда расширяется вправо, насколько это возможно, поэтому вы часто можете оставлять абстракции без скобок, когда они являются последним аргументом оператора более высокого порядка: вы можете видеть, что я сделал это с Pi. Ваш тип Agda (x : S) -> T становится Pi S \ x:S -> T.

(отступление. Введите аннотации на лямбда необходимы, если вы хотите иметь возможность синтезировать тип абстракции. Если вы переключитесь на тип проверка как ваш modus operandi, вам все еще нужны аннотации, чтобы проверить бета-redex, как (\ x -> t) s, так как у вас нет способа угадать типы частей из целого. Я советую современным дизайнерам проверять типы и исключать бета-редексы из самого синтаксиса.)

(отступление. Эта система несовместима как Set:Set позволяет кодировать различные "парадоксы лжеца". Когда Мартин-Леф предложил эту теорию, Жирар послал ему кодировку этого в своей собственной непоследовательной системе U. последующий парадокс из-за Хуркенса-самая аккуратная токсичная конструкция, которую мы знаем.)

синтаксис комбинатора и нормализация

теперь мы можем определить нетипизированный комбинаторный синтаксис (со свободным переменные):

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 встраивание переменных и >>= perfoming substitution), будет удобно представлять промежуточные этапы в процессе преобразования терминов с привязкой к их комбинаторной форме.

здесь нормализация:

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)

я использую представление индекса де Брейна в манере Bellegarde и Hook (как популяризировано птицей и Патерсоном). Тип 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

The K комбинатор используется для подъема значения некоторого типа A к постоянной функции над некоторым другим типом G.

  G : Set   A : Set
-------------------------------
  K : (a : A) -> (g : G) -> A

The S combinator используется для подъема приложений над типом, от которого могут зависеть все детали.

  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, только с условиями. Соответственно, мы можем проверить деривации ввода алгоритмически, но мы не можем просто typecheck combinator термины, как мы могли бы с оригинальной системой. Что может сработать, так это потребовать ввода в typechecker аннотаций типа для использования 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 Encoding Toolkit

вот как строить pil. Во-первых, я определяю класс Finнаборы ite, используемые для переменных. Каждый такой набор имеет конструктор-сохранение embedding в набор выше, плюс новый 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

The wk функция должна встраивать элементы x как большой элементов y, так что лишние вещи в y меньше, и таким образом в de Bruijn индексные термины, связанные более локально.

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

и как только вы разберетесь с этим, немного черепа ранга n сделает все остальное.

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 typechecker достаточно информации, чтобы вычислить сдвиг, необходимый для перевода в представление de Bruijn. Зачем держать собаку и лаять самому?