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

Недавно я закончил университетский курс, в котором были представлены Haskell и Agda (зависимый типизированный функциональный язык программирования) и задавался вопросом, можно ли заменить лямбда-исчисление в них комбинаторной логикой. С Haskell это кажется возможным с помощью комбинаторов S и K, что делает его бесшумным. Мне было интересно, что такое эквивалент для Агды. I.e., можно ли сделать язык типизированного функционального программирования эквивалентным Agda без использования каких-либо переменных?

Кроме того, можно каким-то образом заменить квантификацию на комбинаторы? Я не знаю, является ли это совпадением, но универсальная квантификация, например, делает подпись типа похожей на лямбда-выражение. Есть ли способ удалить универсальную количественную оценку из сигнатуры типа без изменения ее значения? Например. в:

forall a : Int -> a < 0 -> a + a < a

Можно ли выразить одно и то же, не используя forall?

Ответ 1

Поэтому я подумал об этом немного больше и добился определенного прогресса. Здесь первый удар по кодированию Martin-Löf восхитительно прост (но непоследовательно) 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), объем лямбда простирается вправо настолько далеко, насколько это возможно, поэтому вы можете часто оставлять абстракции незафиксированными, когда они являются последним аргументом оператора более высокого порядка: вы можете видеть, что я сделал что с Pi. Тип Agda (x : S) -> T становится Pi S \ x:S -> T.

(Отступление. Аннотации типа на лямбда необходимы, если вы хотите иметь возможность синтезировать тип абстракций. Если вы переключитесь на проверку типа в качестве вашего modus operandi, вам все равно понадобятся аннотации для проверки бета-redex, например (\ 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 являются просто заданными конструкторами, поэтому, записывая нетранслируемые типы и позволяя "нотацию Агда" для 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)

С этими определениями я извлек соответствующие открытые подтермы и провел их через перевод.

Набор инструментов кодирования de Bruijn

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

И после того, как вы разобрались с этим, немного скроллинговая обработка ранга-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 для вычисления сдвига, необходимого для перевода в представление Брюйна. Зачем держать собаку и лаять себя?