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

Question 1

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

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

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

Можно ли выразить то же самое без использования forall?

Question 2

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

Теория целевого типа

Для полноты картины приведу правила. Правильность контекста просто говорит о том, что вы можете создавать контексты из пустых, добавляя новые переменные, населяющие Sets.

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

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

Определив их, я извлек соответствующие открытые подтермы и прогнал их по переводу.

Набор инструментов для кодирования де Брюйна

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

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

Question 3

Я предполагаю, что «абстракция скобок» работает также и для зависимых типов при некоторых обстоятельствах. В разделе 5 следующей статьи вы найдете несколько типов K и S:

Возмутительные, но значащие совпадения
Синтаксис и оценка, безопасные для типов,
Конор МакБрайд, Университет Стратклайда, 2010 г.

Преобразование лямбда-выражения в комбинаторное выражение примерно соответствует преобразованию доказательства естественного вывода в доказательство в стиле Гильберта.

Answer 1

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

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

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

Можно ли выразить то же самое без использования forall?

Answer 2

21

Начните с определения наиболее зависимых типов, возможных для K (легкий) и S (довольно волосатый). Было бы интересно добавить константы для Set и Pi, а затем попытаться восстановить базовую (несовместимую) систему Set: Set. Я бы подумал дальше, но мне нужно успеть на самолет.

pigworker

Answer 3

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

Теория целевого типа

Для полноты картины приведу правила. Правильность контекста просто говорит о том, что вы можете создавать контексты из пустых, добавляя новые переменные, населяющие Sets.

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

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

Определив их, я извлек соответствующие открытые подтермы и прогнал их по переводу.

Набор инструментов для кодирования де Брюйна

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

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

Answer 4

это может быть очень глупо, но как эта картина изменится, если вы добавите Fкомбинатор? Fдействует по-разному в зависимости от своего первого аргумента: если Aявляется атомом, Mа Nявляются термами и PQявляется составной частью, то FAMN -> Mи F(PQ)MN -> NPQ. Это не может быть представлено в SK(I)расчетах, но Kможет быть представлено как FF. Можно ли с помощью этого продлить ваш MLTT без баллов?

kram1032

Answer 5

Я почти уверен, что есть проблема с этой процедурой абстракции скобок, особенно с частью «комбинаторы становятся постоянными», которая переводит λx.c в Kc для комбинаторов c ∈ {S, K, U, P}. Проблема в том, что эти комбинаторы полиморфны и могут использоваться с типом, который зависит от x; такой тип не может быть сохранен этим переводом. В качестве конкретного примера переводится термин λ (A : Set) → λ (a : A) → aтипа , который не может использоваться в типе, где тип второго аргумента зависит от первого аргумента. (A : Set) → (a : A) → AS(S(KS)(KK))(KK)

Anders Kaseorg

Answer 6

Я предполагаю, что «абстракция скобок» работает также и для зависимых типов при некоторых обстоятельствах. В разделе 5 следующей статьи вы найдете несколько типов K и S:

Возмутительные, но значащие совпадения
Синтаксис и оценка, безопасные для типов,
Конор МакБрайд, Университет Стратклайда, 2010 г.

Преобразование лямбда-выражения в комбинаторное выражение примерно соответствует преобразованию доказательства естественного вывода в доказательство в стиле Гильберта.

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

Ответы:

Теория целевого типа

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

Представление теории типов

Перевод терминов в комбинаторы

Набор комбинаторов

Система комбинаторного типа

Генерация типов комбинаторов

Набор инструментов для кодирования де Брюйна