Idris (programmeertaal)

Idris is een pure functionele programmeertaal met afhankelijke typen, optionele luie evaluatie en functies zoals totaliteitscontrole. Idris kan worden gebruikt als bewijsassistent, maar is ontworpen als een programmeertaal voor algemene doeleinden, vergelijkbaar met Haskell.

Het Idris-typesysteem is vergelijkbaar met dat van Agda. De bewijzen zijn vergelijkbaar met die van Coq. Idris heeft zoals Coq tactieken. Dit zijn procedures die gebruikers kunnen oproepen om stellingen helpen te bewijzen. Vergeleken met Agda en Coq geeft Idris prioriteit aan het beheer van neveneffecten en ondersteuning voor ingebedde domeinspecifieke talen. Idris compileert naar C en JavaScript. Er zijn codegeneratoren van derden voor andere platforms, waaronder Java Virtual Machine (JVM), Common Intermediate Language (CIL) en LLVM.

Idris is vernoemd naar een zingende draak uit het Britse kindertelevisieprogramma Ivor the Engine uit de jaren 1970.

Kenmerken

Idris combineert een aantal kenmerken van relatief bekende functionele programmeertalen met kenmerken die zijn geleend van bewijsassistenten.

Functioneel programmeren

De syntaxis van Idris vertoont veel overeenkomsten met die van Haskell. Een hello world-programma in Idris zou er als volgt uit kunnen zien:

module Main

main : IO ()
main = putStrLn "Hello, World!"

De enige verschillen tussen dit programma en zijn Haskell-equivalent zijn de enkele (in plaats van dubbele) dubbele punt in de typesignatuur van de hoofdfunctie, en het weglaten van het woord "where" in de moduledeclaratie.

Inductieve en parametrische datatypen

Idris ondersteunt inductief gedefinieerde gegevenstypen en parametrisch polymorfisme. Dergelijke typen kunnen in de traditionele Haskell 98-achtige syntaxis worden gedefinieerd:

data Tree a = Node (Tree a) (Tree a) | Leaf a

of in de meer algemene gegeneraliseerde algebraïsche datatype (GADT)-achtige syntaxis:

data Tree : Type -> Type where
    Node : Tree a -> Tree a -> Tree a
    Leaf : a -> Tree a

Afhankelijke typen

Met afhankelijke typen is het mogelijk dat waarden in de typen voorkomen; in feite kan elke berekening op waardeniveau worden uitgevoerd tijdens de typecontrole. Het volgende definieert een type voor lijsten, waarvan de lengtes bekend zijn voordat het programma wordt uitgevoerd. Deze lijsten worden traditioneel vectoren genoemd:

data Vect : Nat -> Type -> Type where
  Nil  : Vect 0 a
  (::) : (x : a) -> (xs : Vect n a) -> Vect (n + 1) a

Dit type kan als volgt worden gebruikt:

total
append : Vect n a -> Vect m a -> Vect (n + m) a
append Nil       ys = ys
append (x :: xs) ys = x :: append xs ys

De functie append voegt een vector van m elementen van type a toe aan een vector van n elementen van type a. Omdat de precieze typen van de invoervectoren afhankelijk zijn van een waarde, is het mogelijk om er tijdens het compileren zeker van te zijn dat de resulterende vector precies (n + m) elementen van het type a zal bevatten. Het woord "total" roept de totaliteitscontrole op die een fout rapporteert als de functie niet alle mogelijke gevallen dekt of niet (automatisch) kan worden bewezen dat deze niet in een oneindige lus terechtkomt. Een ander veelvoorkomend voorbeeld is de paarsgewijze optelling van twee vectoren die over hun lengte zijn geparametriseerd:

total
pairAdd : Num a => Vect n a -> Vect n a -> Vect n a
pairAdd Nil       Nil       = Nil
pairAdd (x :: xs) (y :: ys) = x + y :: pairAdd xs ys

Num a betekent dat het type a tot de typeklasse Num behoort. Merk op dat deze functie nog steeds met succes de typecontrole als totaal uitvoert, ook al is er geen geval dat overeenkomt met Nil in de ene vector en een getal in de andere. Omdat het typesysteem kan bewijzen dat de vectoren dezelfde lengte hebben, kunnen we er tijdens het compileren zeker van zijn dat dat geval niet zal voorkomen en dat het niet nodig is om dat geval op te nemen in de definitie van de functie.

Bewijsassistent-functies

Afhankelijke typen zijn krachtig genoeg om de meeste eigenschappen van programma's te coderen, en een Idris-programma kan tijdens het compileren invarianten controleren. Dit maakt Idris tot een bewijsassistent.

Codegeneratie

Standaard genereert Idris native code via C. De andere officieel ondersteunde backend genereert JavaScript.

Idris 2

Idris 2 is een nieuwe zelfgehoste versie van de taal die een lineair typesysteem diepgaand integreert, gebaseerd op kwantitatieve typetheorie. Het compileert momenteel naar Scheme en C.