Závislý typ - Dependent type
Typové systémy |
---|
Obecné pojmy |
Hlavní kategorie |
Menší kategorie |
Viz také |
v počítačová věda a logika, a závislý typ je typ, jehož definice závisí na hodnotě. Jedná se o překrývající se vlastnost teorie typů a systémy typu. v intuicionistická teorie typů, pro zakódování logiky se používají závislé typy kvantifikátory jako „pro všechny“ a „existuje“. v funkční programovací jazyky jako Agda, ATS, Coq, F*, Epigram, a Idrisi, závislé typy mohou pomoci snížit chyby povolením programátoru přiřadit typy, které dále omezují množinu možných implementací.
Dva běžné příklady závislých typů jsou závislé funkce a závislé páry. Návratový typ závislé funkce může záviset na hodnota (nejen typ) jednoho ze svých argumentů. Například funkce, která přebírá kladné celé číslo může vrátit pole délky , kde délka pole je součástí typu pole. (Všimněte si, že se to liší od polymorfismus a generické programování, z nichž oba obsahují typ jako argument.) Závislá dvojice může mít druhou hodnotu, jejíž typ závisí na první hodnotě. Na příkladu pole lze závislý pár použít k párování pole s jeho délkou bezpečným způsobem.
Závislé typy dodávají systému typů složitost. Rozhodování o rovnosti závislých typů v programu může vyžadovat výpočty. Pokud jsou v závislých typech povoleny libovolné hodnoty, pak rozhodování o rovnosti typů může zahrnovat rozhodnutí, zda dva libovolné programy vytvoří stejný výsledek; proto kontrola typu může se stát nerozhodnutelný.
Dějiny
V roce 1934 Haskell Curry si všiml, že typy používané v zadaný lambda kalkul, a v jeho kombinační logika protějšek, následoval stejný vzor jako axiomy v výroková logika. Jdeme dále, pro každý důkaz v logice byla v programovacím jazyce funkce shody (term). Jedním z Curryho příkladů byla korespondence mezi jednoduše zadaný lambda kalkul a intuicionistická logika.[1]
Predikátová logika je rozšíření výrokové logiky a přidává kvantifikátory. Howarde a de Bruijn rozšířený lambda kalkul, aby odpovídal této výkonnější logice vytvořením typů pro závislé funkce, které odpovídají „pro všechny“, a závislých párů, které odpovídají „existuje“.[2]
(Kvůli této a další práci Howarda jsou propozice jako typy známé jako Curry – Howardova korespondence.)
Formální definice
typ
Volně řečeno, závislé typy jsou podobné typu indexované rodiny množin. Více formálně, vzhledem k typu ve vesmíru typů , jeden může mít rodina typů , který přiřadí každému termínu typ . Říkáme, že typ B (a) se liší podle A.
Funkce, jejíž typ návratové hodnoty se liší podle jejího argumentu (tj. Neexistuje pevná hodnota codomain ) je závislá funkce a je volán typ této funkce závislý typ produktu, pí-typ nebo závislý typ funkce.[3] Z rodiny typů můžeme zkonstruovat typ závislých funkcí , jejichž termíny jsou funkce, které obsahují termín a vrátit termín v . V tomto příkladu je typ závislé funkce obvykle zapsán jako nebo Li je konstantní funkce, odpovídající závislý typ produktu je ekvivalentní obyčejnému typ funkce. To znamená, je v úsudku roven když B nezávisí na X.
Název „pi-type“ vychází z myšlenky, že je lze považovat za a kartézský součin typů. Typy pí lze také chápat jako modely z univerzální kvantifikátory.
Například když píšeme pro n-tuples of reálná čísla, pak by byl typ funkce, která, vzhledem k přirozené číslo n, vrací n-tici skutečných čísel velikosti n. Obvyklý funkční prostor vzniká jako speciální případ, když typ rozsahu ve skutečnosti nezávisí na vstupu. Např. je typ funkcí od přirozených čísel po reálná čísla, který je zapsán jako v zadaném lambda kalkulu.
typ
The dvojí závislého typu produktu je závislý typ páru, závislý typ součtu, typ sigma, nebo (matoucí) závislý typ produktu.[3] Typy sigma lze také chápat jako existenční kvantifikátory. Pokračování výše uvedeného příkladu, pokud, ve vesmíru typů , existuje typ a rodina typů , pak existuje závislý typ páru
Typ závislého páru zachycuje myšlenku uspořádaného páru, kde typ druhého členu závisí na hodnotě prvního. Li
Příklad jako existenční kvantifikace
Nechat být nějaký typ, a nechť . Podle Curry – Howardova korespondence, B lze interpretovat jako logické predikát za podmínek A. Za dané , zda typ B (a) je obydlený označuje, zda A splňuje tento predikát. Korespondenci lze rozšířit na existenciální kvantifikaci a závislé páry: tvrzení je pravda kdyby a jen kdyby typ je obydlený.
Například, je menší nebo rovno právě když existuje jiné přirozené číslo takhle m + k = n. V logice je toto tvrzení kodifikováno existenční kvantifikací:
Systémy lambda kostky
Henk Barendregt vyvinul lambda kostka jako prostředek klasifikace systémů typu podél tří os. Osm rohů výsledného diagramu ve tvaru krychle odpovídá každému typovému systému s jednoduše zadaný lambda kalkul v nejméně výrazném rohu a počet konstrukcí nejexpresivnější. Tři osy krychle odpovídají třem různým zvětšením jednoduše zadaného lambda kalkulu: přidání závislých typů, přidání polymorfismu a přidání vyšších laskavý konstruktory typů (například funkce z typů na typy). Kostku lambda dále zobecňuje systémy čistého typu.
Teorie závislá na typu prvního řádu
Systém čistých typů závislých na prvním řádu, odpovídajících logickému rámci LF, se získá zobecněním typu funkčního prostoru souboru jednoduše zadaný lambda kalkul na závislý typ produktu.
Teorie závislých typů druhého řádu
Systém typů závislých na druhém řádu se získá z povolením kvantifikace nad konstruktory typu. V této teorii operátor závislého produktu zahrnuje oba operátor jednoduše zadaného lambda kalkulu a pořadač Systém F.
Polymorfní lambda kalkul se závislým typem vyššího řádu
Systém vyššího řádu rozšiřuje na všechny čtyři formy abstrakce z lambda kostka: funkce od pojmů k pojmům, typy k typům, pojmy k typům a typy k pojmům. Systém odpovídá počet konstrukcí jehož derivát je počet indukčních konstrukcí je základní systém Coq proof asistent.
Simultánní programovací jazyk a logika
The Curry – Howardova korespondence znamená, že lze konstruovat typy, které vyjadřují libovolně složité matematické vlastnosti. Pokud může uživatel dodat a konstruktivní důkaz že typ je obydlený (tj. že hodnota tohoto typu existuje), pak kompilátor může zkontrolovat důkaz a převést jej na spustitelný počítačový kód, který vypočítá hodnotu provedením konstrukce. Díky funkci kontroly pravopisu jsou jazyky závislé na stroji úzce spjaty důkazní asistenti. Aspekt generování kódu poskytuje silný přístup k formálnímu ověření programu a kontrolní kód, protože kód je odvozen přímo z mechanicky ověřeného matematického důkazu.
Porovnání jazyků se závislými typy
Jazyk | Aktivně vyvinut | Paradigma[fn 1] | Taktika | Důkazní podmínky | Kontrola ukončení | Typy mohou záviset na[fn 2] | Vesmíry | Důkaz irelevance | Extrakce programu | Extrakce vymaže irelevantní pojmy |
---|---|---|---|---|---|---|---|---|---|---|
Ada 202x | Ano[4] | Rozkazovací způsob | Ano[5] | Ano (volitelně)[6] | ? | Libovolný termín[fn 3] | ? | ? | Ada | ? |
Agda | Ano[7] | Čistě funkční | Několik / omezené[fn 4] | Ano | Ano (volitelně) | Libovolný termín | Ano (volitelně)[fn 5] | Důkazní irelevantní argumenty[9] Důkazy irelevantní[10] | Haskell, JavaScript | Ano[9] |
ATS | Ano[11] | Funkční / imperativní | Ne[12] | Ano | Ano | Statické pojmy[13] | ? | Ano | Ano | Ano |
Cayenne | Ne | Čistě funkční | Ne | Ano | Ne | Libovolný termín | Ne | Ne | ? | ? |
Gallina (Coq ) | Ano[14] | Čistě funkční | Ano | Ano | Ano | Libovolný termín | Ano[fn 6] | Ne | Haskell, Systém a OCaml | Ano |
Závislé ML | Ne[fn 7] | ? | ? | Ano | ? | Přirozená čísla | ? | ? | ? | ? |
F* | Ano[15] | Funkční a imperativní | Ano[16] | Ano | Ano (volitelně) | Jakýkoli čistý termín | Ano | Ano | OCaml, F#, a C | Ano |
Guru | Ne[17] | Čistě funkční[18] | hypjoin[19] | Ano[18] | Ano | Libovolný termín | Ne | Ano | Kmín | Ano |
Idrisi | Ano[20] | Čistě funkční[21] | Ano[22] | Ano | Ano (volitelně) | Libovolný termín | Ano | Ne | Ano | Ano, agresivně[22] |
Opírat se | Ano | Čistě funkční | Ano | Ano | Ano | Libovolný termín | Ano | Ano | Ano | Ano |
Matita | Ano[23] | Čistě funkční | Ano | Ano | Ano | Libovolný termín | Ano | Ano | OCaml | Ano |
NuPRL | Ano | Čistě funkční | Ano | Ano | Ano | Libovolný termín | Ano | ? | Ano | ? |
PVS | Ano | ? | Ano | ? | ? | ? | ? | ? | ? | ? |
Šalvěj | Ne[fn 8] | Čistě funkční | Ne | Ne | Ne | ? | Ne | ? | ? | ? |
Twelf | Ano | Logické programování | ? | Ano | Ano (volitelně) | Libovolný (LF) termín | Ne | Ne | ? | ? |
Xanadu | Ne[24] | Rozkazovací způsob | ? | ? | ? | ? | ? | ? | ? | ? |
Viz také
Poznámky pod čarou
- ^ To se týká jádro jazyk, ne na žádnou taktiku (dokazování věty postup ) nebo dílčí jazyk generování kódu.
- ^ S výhradou sémantických omezení, jako jsou vesmírná omezení
- ^ Static_Predicate pro omezené výrazy, Dynamic_Predicate pro kontrolu typu Assert jako jakýkoli výraz v obsazení typu
- ^ Řešič prstenů[8]
- ^ Volitelné vesmíry, volitelný polymorfismus vesmíru a volitelně explicitně specifikované vesmíry
- ^ Vesmír, automaticky odvozená omezení vesmíru (ne stejná jako polymorfismus vesmíru Agdy) a volitelný explicitní tisk omezení vesmíru
- ^ Byl nahrazen ATS
- ^ Papír Last Sage a poslední snímek kódu jsou datovány rokem 2006
Reference
- ^ Sørensen, Morten Heine B .; Pawel Urzyczyn (1998). „Přednášky o Curry-Howardově izomorfismu“. CiteSeerX 10.1.1.17.7385. Citovat deník vyžaduje
| deník =
(Pomoc) - ^ Bove, Ana; Peter Dybjer (2008). „Závislé typy v práci“ (PDF). Citovat deník vyžaduje
| deník =
(Pomoc) - ^ A b "ΠΣ: Závislé typy bez cukru" (PDF).
- ^ „Stránka ke stažení komunity GNAT“.
- ^ „Predikáty RM3.2.4 podtypu“.
- ^ JISKRA je prokazatelná podmnožina Ada
- ^ „Stránka ke stažení Agda“.
- ^ "Agda Ring Solver".
- ^ A b „Oznámit: Agda 2.2.8“. Archivovány od originál dne 18.7.2011. Citováno 2010-09-28.
- ^ "Seznam změn Agda 2.6.0".
- ^ „Stahování ATS2“.
- ^ „e-mail od vynálezce ATS Hongwei Xi“.
- ^ „Applied Type System: An Approach to Practical Programming with Theorem-Proving“ (PDF).
- ^ „Coq CHANGES in Subversion repository“.
- ^ „F * změny na GitHubu“.
- ^ „Poznámky k verzi F * v0.9.5.0 na GitHubu“.
- ^ „Guru SVN“.
- ^ A b Aaron Stump (6. dubna 2009). „Ověřené programování v Guru“ (PDF). Archivovány od originál (PDF) dne 29. prosince 2009. Citováno 28. září 2010.
- ^ Adam Petcher (1. dubna 2008). „Rozhodování o spojitelnosti modulozemních rovnic v teorii provozního typu“ (PDF). Citováno 14. října 2010.
- ^ „Úložiště Idris git“.
- ^ „Idris, jazyk se závislými typy - rozšířený abstrakt“ (PDF). Archivovány od originál (PDF) dne 16.7.2011.
- ^ A b Edwin Brady. „Jak je na tom Idris s jinými závislými typovými programovacími jazyky?“.
- ^ „Matita SVN“. Archivovány od originál dne 8. května 2006. Citováno 2010-09-29.
- ^ „Domovská stránka Xanadu“.
Další čtení
- Martin-Löf, Per (1984). Intuicionistická teorie typů (PDF). Bibliopolis.
- Nordström, Bengt; Petersson, Kent; Smith, Jan M. (1990). Programování v teorii typu Martina-Löfa: Úvod. Oxford University Press. ISBN 9780198538141.
- Barendregt, H. (1992). "Lambda kameny s typy". In Abramsky, S .; Gabbay, D .; Maibaum, T. (eds.). Příručka logiky v informatice. Oxford Science Publications.
- McBride, Conore; McKinna, James (Leden 2004). „Pohled zleva“. Journal of Functional Programming. 14 (1): 69–111. doi:10.1017 / s0956796803004829.
- Altenkirch, Thorsten; McBride, Conore; McKinna, James (Duben 2005). „Proč záleží na závislých typech“ (PDF). Citovat deník vyžaduje
| deník =
(Pomoc) - Norell, Ulf (září 2007). Směrem k praktickému programovacímu jazyku založenému na teorii závislých typů (PDF) (PhD). Göteborg, Švédsko: Katedra výpočetní techniky a inženýrství, Chalmers University of Technology. ISBN 978-91-7291-996-9.
- Oury, Nicolas; Swierstra, Wouter (2008). „Síla Pi“ (PDF). ICFP '08: Sborník z 13. mezinárodní konference ACM SIGPLAN o funkčním programování. 39–50. doi:10.1145/1411204.1411213. ISBN 9781595939197.
- Norell, Ulf (2009). „Závisle napsané programování v Agda“ (PDF). In Koopman, P .; Plasmeijer, R .; Swierstra, D. (eds.). Pokročilé funkční programování. AFP 2008. Přednášky z informatiky. 5832. Springer. str. 230–266. doi:10.1007/978-3-642-04652-0_5. ISBN 978-3-642-04651-3.
- Sitnikovski, Boro (2018). Jemný úvod do závislých typů s Idrisem. Štíhlé publikování. ISBN 978-1723139413.