Beroende typ

Dependent type ( engelsk dependent type ) inom datavetenskap och logik är en typ som beror på något värde. Beroende typer spelar en nyckelroll i intuitionistisk typteori och konstruktionen av funktionella programmeringsspråk som ATS , Agda , Epigram och Idris .

Till exempel är en typ som beskriver n - tuplar av reella tal beroende eftersom den "beror" på värdet av n .

Att bestämma om beroende typer är lika i ett program kan kräva beräkning. Om godtyckliga värden är tillåtna i beroende typer, kan typlikhetsbeslutet inkludera kontroll av likheten mellan resultatet av arbetet med två godtyckliga program. Således blir typkontroll en olöslig uppgift .

Curry-Howard isomorfism låter dig bygga typer för att uttrycka godtyckligt komplexa matematiska egenskaper. Om ett konstruktivt bevis tillhandahålls för att en typ är "befolkad" (det vill säga att det finns minst ett värde av den typen), kommer kompilatorn att kunna verifiera detta bevis och omvandla det till körbar kod som utvärderar värdet. Förekomsten av beviskontroll gör språk som skrivs av beroendetyp liknar programvara för bevisautomatisering (som Coqs interaktiva teoremprover ).

Lambdakubsystem

Henk Barendregt utvecklade lambdakuben som ett sätt att klassificera typsystem längs tre axlar. Vart och ett av de åtta hörnen i kubdiagrammet motsvarar ett typsystem. I den fattigaste spetsen av kuben finns den enkelt skrivna lambdakalkylen , och i den rikaste spetsen finns konstruktionskalkylen . Kubens tre axlar motsvarar tre olika tillägg till den enkelt skrivna lambdakalkylen: tillägget av beroende typer, tillägget av polymorfism och tillägget av typkonstruktörer av högre ordning.

Formell definition

På ett mycket förenklat sätt kan en beroende typ ses som typen av en indexerad familj av uppsättningar. Mer formellt, för en typ (var är typernas universum) kan du definiera en typfamilj , som mappar varje term till en typ , som skrivs som . En funktion vars intervall varierar beroende på dess argument kallas en beroende funktion . Typen av denna funktion kallas beroende typ produkt , pi-typ eller helt enkelt beroende typ . Den beroende typen skrivs för detta fall som $A:{\mathcal {U}}$ ${\mathcal {U}}$ $B$ $a:A$ $B(a):{\mathcal {U}}$ $B:A\to {\mathcal {U}}$

\Pi _{{(x:A)}}B(x)

eller

\Pi(x:A),B(x)

Om är en konstant, så förenklas den beroende typen till en normal funktion . Med andra ord är det likvärdigt med funktionstypen . Namnet " pi-typ " understryker att en sådan typ är en kartesisk produkt av typer. Pi-typer kan också representeras som universella kvantifieringsmodeller . $B$ $A till B$ $\Pi _{{(x:A)}}B$ $A till B$

Till exempel, om är en tuppel av reella tal , då är den typ av funktioner som, för alla naturliga tal , returnerar en tupel av reella tal av storlek . Det vanliga funktionsutrymmet är det speciella fallet när intervallet inte beror på indataparametern: till exempel - typen av funktioner från naturliga till verkliga, som anges i den enkelt skrivna lambdakalkylen . ${\mbox{Vec}}({{\mathbb R}},n)$ $n$ $\Pi _{{(n:{{\mathbb N}})))}{\mbox{Vec}}({{\mathbb R}}),n)$ $n$ $n$ $\Pi _{{(n:{{\mathbb N}})))}\;{{\mathbb R}}$ ${{\mathbb N}}\to {{\mathbb R}}$

Polymorfa funktioner är ett viktigt exempel på beroende funktioner, det vill säga funktioner som har en beroende typ. För en viss typ fungerar sådana funktioner på värden av den typen, eller värden av en typ som härrör från den typen. En polymorf funktion som returnerar värden av typenkommer att ha en polymorf typ skriven som $C$

\Pi _{{(A:{\mathcal {U))))}A\till C

Litteratur

Chlipala, A. Certifierad programmering med beroende typer: En pragmatisk introduktion till Coq Proof Assistant . - MIT Press, 2013. - 440 sid. — ISBN 9780262026659 . ( text från författarens webbplats (eng.) )
Jeremy Paul Condit. Beroende typer av programvara för säkra system. — Doktorsavhandling. — University of California i Berkeley, 2007.