Възможно ли е да въведете `min` в нормализираща теория като System-F или Calculus of Constructions?

Тази min дефиниция по-долу работи с две църковни числа и връща най-малкото голямо. Всяко число се превръща в продължение, което изпраща своето предшестващо число към другото, зиг и заг, докато се достигне нула. Освен това, едно от числата добавя f към резултата всеки път, когато се извика, така че в крайна сметка ще имате (\ f x -> f (... (f (f x)) ...)), където броят на 'f' вдясно е броят пъти, когато е извикано първото продължение.

min a b f x = (a_continuator b_continuator)
    a_continuator = (a (\ pred cont -> (cont pred)) (\ cont -> x))
    b_continuator = (b (\ pred cont -> (f (cont pred))) (\ cont -> x))

Изглежда, че min не може да се въведе на System-F. Например, за да го стартирам на GHC, трябваше да използвам unsafeCoerce два пъти:

import Unsafe.Coerce

(#)   = unsafeCoerce
min'  = (\ a b f x -> (a (\ p c -> (c # p)) (\ c -> x) (b (\ p c -> (f (c # p))) (\ c -> x))))
toInt = (\ n -> (n (+ 1) 0))
main  = print (toInt (min'
    (\ f x -> (f (f (f (f (f x))))))               -- 5
    (\ f x -> (f (f (f (f (f (f (f (f x))))))))))  -- 8
    :: Int)

Възможно ли е да въведете min в System-F (или в Изчислението на конструкциите)?


types haskell dependent-type agda type-theory
person MaiaVictor    schedule 18.11.2015    source източник
comment
Не мога да анализирам (cont -> x). Има ли и \ ?   -  person chi    schedule 18.11.2015
comment
Тук нямам ясна представа, но мисля, че църковните цифри имат политип CN = forall a. (a->a)->a->a. Тъй като политиповете не могат да бъдат изведени, бих започнал с анотиране на променливи с цифрови стойности с CN -- има шанс да ги използвате в различни типове.   -  person chi    schedule 18.11.2015
comment
@chi Всъщност не трябва да има `` на другата ламбда. Нямах представа как се озова там. Има ли шанс да ги използвам в различни видове?   -  person MaiaVictor    schedule 18.11.2015
comment
В нетипизираното ламбда изчисление можете да приложите църковно число към всяка функция. В типизиран език без политипове можете да имате число за всеки тип T (което може да се приложи само към функции T->T) -- това ограничение обаче е много неудобно. В многотипен език можете да присвоите тип CN на числа, така че те да могат да работят с всяка функция от тип T->T, независимо от типа T.   -  person chi    schedule 18.11.2015
comment
След известен експеримент чувствам, че подтерминът a (\ p c -> c p) не може да бъде въведен в SystemF (дори след добавяне на някои параметри на типа). Типът му изглежда зависи от действителната стойност на a. Предполагам, че в CoC може да бъде въведен, но само след добавяне не само на променливи на типа/аргументи на типа, но и на други термини, които кодират как полученият тип зависи от a.   -  person chi    schedule 18.11.2015
comment
Това изглежда работи по същия начин като coroutining zip в предишния въпрос, така че мисля, че може да бъде въведен по подобен начин в Agda. Въпреки това, той също ще използва зависима елиминация, този път на естествени числа, и няма начин да се получи това само от кодирането на Чърч. Трябва да добавим правилото за елиминиране към основния език.   -  person András Kovács    schedule 18.11.2015
comment
Това всъщност питам. Вашето решение използва зависими елиминатори, които CoC (по този начин Morte) няма. Значи казвате, че не може да се пише на CoC, нали?   -  person MaiaVictor    schedule 18.11.2015
comment
вярно Това е донякъде лоша новина за тези, които искат минимални основни езици. Бихте могли обаче да разгледате теориите за типове със затворени (генерични) типове вселени, тъй като те могат да бъдат много по-мощни от ванилия CoC, но все още имат доста проста спецификация (и също така не се нуждаят от дефинирани от потребителя типове данни).   -  person András Kovács    schedule 18.11.2015
comment
Начинът, по който казахте, е труден за Google. Бихте ли ми дали някои насоки, @AndrásKovács?   -  person MaiaVictor    schedule 18.11.2015
comment
За съжаление материалът, който прочетох за това, е разпръснат из много несамостоятелни документи и не си спомням нищо от главата си, което би било хубаво специално за вашите цели. Идеята е да се кодират всички типове с помощта на малък набор от конструкции, за достъпни основи можете да разгледате GHC.Generics и неговите употреби. За по-напреднали общи вселени можете да погледнете това или това.   -  person András Kovács    schedule 19.11.2015
comment
Като цяло научих много от документите на Conor McBride (pigworker в SO и reddit) и относно генеричните продукти, по-специално от документите на Anders Löh (kosmikus в SO и reddit). Потърсете в Google Scholar техните неща. Предполагам, че ще трябва да се потопите в теорията на типа, за да разберете добре това. Все пак препоръчвам изживяването от все сърце.   -  person András Kovács    schedule 19.11.2015
comment
Предполагам, че ще трябва да се потопите в теорията на типа, за да разберете добре това. - и как мога да направя това ефективно? Когато обмислям да направя това, това, което ме спира е, че мисля, че бих прекарал повече време в разкриване на полето и измисляне на това, което трябва да прочета, отколкото в самото четене.   -  person MaiaVictor    schedule 19.11.2015
comment
Нека продължим тази дискусия в чата.   -  person András Kovács    schedule 19.11.2015

Отговори (1)


arrow_upward
4
arrow_downward

Функцията (добре позната ли е? изглежда наистина умна) може да се пише, но не работи с кодирани от Църквата nats.

Ето вида, който GHC извежда:

(((t3 -> t2) -> t3 -> t2) -> (b0 -> a0) -> t1 -> t0)
                        -> (((t6 -> t5) -> t6 -> t4) -> (b1 -> a0) -> t1)
                        -> (t5 -> t4)
                        -> a0
                        -> t0))

Ето най-близкото до желания тип, което мога да получа:

postulate t1 t2 : Set

A = ((t2 -> t1) -> t1) -> (((t2 -> t1) -> t1) -> t1) -> t1
B = (t2 -> t1) -> ((t2 -> t1) -> t1) -> t1
C = t1 -> t1

min : (A -> A) -> (B -> B) -> (C -> C)
min a b = \ f x -> a (\ p c -> c p) (\ c -> x) (b (\ p c -> f (c p)) (\ c -> x))

За да работи с кодиран от църквата nats, min трябва да приеме два аргумента от тип (a -> a) -> a -> a, т.е. A трябва да бъде от тип a -> a, т.е.

a ~ (t2                 -> t1) -> t1
a ~ (((t2 -> t1) -> t1) -> t1) -> t1

т.е. t2 ~ (t2 -> t1) -> t1, което е цикъл. Няма рекурсивни типове в System F или CoC и следователно терминът не може да се въвежда такъв, какъвто е.

Въпреки това пренебрегнах нещата Rank2Types. Така или иначе,

newtype Church = Church { runChurch :: forall a. (a -> a) -> a -> a }

min' a b = Church $ \f x -> runChurch a (\p c -> c p) (\c -> x) (runChurch b (\p c -> f (c p)) (\c -> x))

също е безкраен тип грешка.

person user3237465    schedule 19.11.2015
comment
Вижте това за дискусия относно min-подобни конструкции. - person András Kovács; 19.11.2015
comment
@András Kovács, благодаря, това е необичайно четима хартия, която съдържа продължения. Така че трябва да решим t2 = (t2 -> t1) -> t1 и следователно имаме нужда от рекурсивни типове. - person user3237465; 19.11.2015
comment
@AndrásKovács, какво мислиш за Self Types? Решава ли проблема без други проблеми? - person MaiaVictor; 21.11.2015
comment
@Viclib Мисля, че min може да бъде въведено в него, след като направим някакво разширение на системата в статията, по-специално трябва да изчислим типове от Nat-s, което изисква индукционен мотив Nat -> ☐, но статията има само Nat -> *. Това обаче не трябва да е твърде трудно, можем да използваме йерархия от вселени като в Agda/Coq или * : *, ако сме мързеливи. Хартията е страхотна находка. - person András Kovács; 22.11.2015
comment
@András Kovács, системата вече има * : *. Но тогава можем просто да използваме кодирани от Скот данни. Не мисля, че е възможно да се типизира self k = k self (което е най-основното нещо, което можем да направим с хиперфункции) в която и да е звукова система: self self е незабавен цикъл. - person user3237465; 22.11.2015
comment
@user3237465: Виждам само * : ☐ в хартия. Що се отнася до въвеждането на min, ние просто трябва да предоставим допълнително доказателство, че типовете на съвместните сгъвания винаги се подреждат. Вижте кода на Agda. На пръв поглед изглежда осъществимо и със себе си, ако добавим голяма елиминация. - person András Kovács; 22.11.2015
comment
@András Kovács, предполагам, че има * : ☐ в хартията само поради изтриването на System F-omega неща. Слайдовете съдържат * : *. Кодът е просветляващ, благодаря. Невъзможно е да се дефинира self k = k self, но не и self : ∀ n -> Min ⊤ n -> ℕ; self 0 k = k _; self (suc n) k = k (self n). - person user3237465; 22.11.2015
comment
@Viclib, András Kovács, написах повече или по-малко директен превод на сърутиниране на сгъвания към Agda. - person user3237465; 23.11.2015
comment
@user3237465, не съм сигурен, че разбирам за какво говорите. Какъв точно е изводът? За да бъде въведено min в звукова система, всичко, от което се нуждаем, е self и безкрайна йерархия от вселени - това ли каза? Аз (много) повърхностно разбирам какво прави вашият код, но не виждам никакъв самореферентен тип там, така че не съм сигурен какво трябва да прави това. - person MaiaVictor; 24.11.2015
comment
@Viclib, self-типовете ви дават принципа на индукция, който е необходим за дефиниране на foldK. Но с принципа на индукция можете да напишете min, като използвате директно съпоставяне на образец. Така че да, self-типовете ви дават възможността да направите min въведено, но също така ви дават възможността да напишете обичайната триредова дефиниция на min. Но не знам дали аз-типовете наистина са безпроблемни. - person user3237465; 24.11.2015
comment
@user3237465 имаш предвид обичайната рекурсивна функция? min (S a) (S b) = min a b; min Z b = b; min a Z = a? Това няма смисъл, защото те се нуждаят от Y-Combinator (дори при нетипизираното ламбда изчисление), което не може да бъде въведено, нали? - person MaiaVictor; 24.11.2015
comment
@Viclib, ако a е кодиран от Church и b е кодиран от Scott, тогава не се нуждаете от Y-комбинатора. Елиминаторите ви дават и двете като Parigot кодиране. (Обсъдихме това и аз се съгласих, че min дефинира този начин е твърде строг, но това беше грешно: ето е програма, която прекратява незабавно. С кодирането на Church сте заседнали с tail, но не и с head). Тук е zipWith дефинирано в термини на елиминатори. - person user3237465; 24.11.2015
comment
ААА разбирам. Е, ще опитам да разширя Morte с self и да напиша вашето foldK там, това може да е страхотно упражнение. Но какво се случва на ред 7 след знака =? Защо interleave използва {} вместо () в аргументите? Освен това не съм сигурен къде се използва self TBH, типът на foldK не се отнася за себе си, той се отнася за FoldK... - person MaiaVictor; 25.11.2015
comment
@Viclib, щях да стана удобен със зависимите типове, преди да се опитам да внедря програма за проверка на типа, особено с недобре известни правила, които не са насочени към синтаксиса. FoldK прави вид продължение от число. Неявните аргументи са затворени в {} — това е просто за удобство, можете да направите всичко изрично. Въпросът за foldK е, че неговият тип зависи от n. С кодираните от Църква nats няма начин да изразите тази зависимост — те ви дават силата на предикативната система F (модуло голяма елиминация). self ви дава елиминатори, които са крайъгълният камък на теориите за зависим тип. - person user3237465; 25.11.2015