Afhængig type

Afhængig type ( engelsk afhængig type ) i datalogi og logik er en type , der afhænger af en eller anden værdi. Afhængige typer spiller en nøglerolle i intuitionistisk typeteori og konstruktionen af funktionelle programmeringssprog som ATS , Agda , Epigram og Idris .

For eksempel er en type, der beskriver n - tupler af reelle tal, afhængig, fordi den "afhænger" af værdien af n .

At beslutte, om afhængige typer er ens i et program, kan kræve beregning. Hvis vilkårlige værdier er tilladt i afhængige typer, kan typelighedsbeslutningen omfatte kontrol af ligheden af resultatet af arbejdet i to vilkårlige programmer. Typekontrol bliver således en uløselig opgave .

Curry-Howard isomorfisme giver dig mulighed for at bygge typer til at udtrykke vilkårligt komplekse matematiske egenskaber. Hvis der leveres et konstruktivt bevis for, at en type er "beboet" (det vil sige, at der er mindst én værdi af den type), vil compileren være i stand til at verificere dette bevis og omdanne det til eksekverbar kode, der evaluerer værdien. Tilstedeværelsen af beviskontrol gør afhængigt indtastede sprog svarende til bevisautomatiseringssoftware (såsom Coq interaktive teorem-beviser ).

Lambda terningsystemer

Henk Barendregt udviklede lambda-terningen som et middel til at klassificere typesystemer langs tre akser. Hvert af de otte hjørner af terningdiagrammet svarer til et typesystem. Ved det fattigste toppunkt af kuben er den enkelt indtastede lambdaregning , og i det rigeste toppunkt er konstruktionsregningen . Terningens tre akser svarer til tre forskellige tilføjelser til den enkelt indtastede lambdaregning: tilføjelse af afhængige typer, tilføjelse af polymorfi og tilføjelse af typekonstruktører af højere orden.

Formel definition

På en meget forenklet måde kan en afhængig type opfattes som typen af en indekseret familie af sæt. Mere formelt kan du for en type (hvor er universet af typer) definere en typefamilie , som knytter hvert led til en type , som skrives som . En funktion, hvis rækkevidde varierer afhængigt af dens argument, kaldes en afhængig funktion . Typen af denne funktion kaldes afhængig type produkt , pi-type eller simpelthen afhængig type . Den afhængige type er skrevet for denne sag 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)

Hvis er en konstant, så forenkles den afhængige type til en normal funktion . Det svarer med andre ord til funktionstypen . Navnet " pi-type " understreger, at en sådan type er et kartesisk produkt af typer. Pi-typer kan også repræsenteres som universelle kvantificeringsmodeller . $B$ $A til B$ $\Pi _{{(x:A)}}B$ $A til B$

For eksempel, hvis er en tuple af reelle tal , så er den type funktioner, der for ethvert naturligt tal returnerer en tuple af reelle tal af størrelse . Det sædvanlige funktionsrum er det specielle tilfælde, når intervallet ikke afhænger af inputparameteren: for eksempel - typen af funktioner fra naturlig til reel, angivet i den enkelt indtastede lambda-regning . ${\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}}\til {{\mathbb R}}$

Polymorfe funktioner er et vigtigt eksempel på afhængige funktioner, det vil sige funktioner, der har en afhængig type. For en given type fungerer sådanne funktioner på værdier af den type, eller værdier af en type, der er afledt af den type. En polymorf funktion, der returnerer værdier af typen, vil have en polymorf type skrevet som $C$

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

Litteratur

Chlipala, A. Certificeret programmering med afhængige typer: En pragmatisk introduktion til Coq Proof Assistant . - MIT Press, 2013. - 440 s. — ISBN 9780262026659 . ( tekst fra forfatterens hjemmeside (eng.) )
Jeremy Paul Condit. Afhængige typer af software til sikre systemer. — Ph.d.-afhandling. - University of California i Berkeley, 2007.