| Idris | |
|---|---|
| Nyelvóra | Funkcionális |
| Megjelent | 2007 [3] [4] [5] |
| Szerző | Edwin Brady |
| Fájlkiterjesztés _ | .idrvagy.lidr |
| Kiadás | Idris 2 0.5.1-es verzió [1] (2021. szeptember 20. ) |
| Típusrendszer | szigorú , statikus , függő típusú támogatás |
| Befolyásolt | Agda , Coq , [2] Epigram , Haskell , [2] ML , [2] Rust |
| Engedély | BSD-3 |
| Weboldal | idris-lang.org |
Az Idris egy tiszta , teljes funkcionális általános célú programozási nyelv Haskell - szerű szintaxissal és függő típusok támogatásával [6] . A típusrendszer hasonló az Agda típusrendszerhez .
A nyelv támogatja a Coq - hoz hasonló automatikus korrektorokat , beleértve a taktikát, de nem összpontosít rájuk, hanem általános célú programozási nyelvként van elhelyezve . Létrehozásának céljai: "elégséges" teljesítmény, a mellékhatások egyszerű kezelése és a beágyazható tartományspecifikus nyelvek megvalósításának eszközei .
Haskellben implementálva, Hackage csomagként [ 7 ] érhető el . Az Idris forráskódja közbülső reprezentációk halmazává áll [8] , és ezekből C -kódba, amelyet a Cheney algoritmus másolási szemétgyűjtő segítségével hajtanak végre . Szintén hivatalosan implementálva van a JavaScript kódra való fordítás lehetősége (beleértve a Node.js -t is ). Léteznek harmadik féltől származó kódgenerátorok Java , JVM , CIL , Erlang , PHP és (korlátozottan) LLVM számára .
A nyelv az éneklő sárkányról, Idrisről kapta a nevét az 1970-es brit gyermektévéműsorból, az Ivor the Tank Engine [9] .
A nyelv egyesíti a főbb népszerű funkcionális programozási nyelvek jellemzőit az automatikus ellenőrző rendszerekből kölcsönzött funkciókkal, hatékonyan elmosva a határvonalat a két nyelvosztály között.
A nyelv második verziója (2020-ban, a „kvantitatív típuselmélet” [10] alapján) jelentősen eltér az elsőtől: a lineáris típusok teljes támogatása hozzáadásra került , a kód alapértelmezés szerint a Scheme -ben van lefordítva , a nyelvi fordító magában a nyelvben van írva .
A nyelv szintaxisa (mint az Agdáé ) közel áll Haskelléhez [11] . szia világ! így néz ki az Idris-en:
modul Fő main : IO () main = putStrLn "Hello, World!"A különbség a program és a Haskell megfelelője között az egyetlen (dupla helyett) kettőspont a fő függvény aláírásában és a "hol" szó hiánya a modul deklarációjában.
A legtöbb modern funkcionális programozási nyelvhez hasonlóan ez a nyelv is támogatja a rekurzív (indukcióval meghatározott) adattípusokat és a parametrikus polimorfizmust . Az ilyen típusok a hagyományos "Haskell98" szintaxis szerint határozhatók meg:
adatfa a = Csomópont ( a fa ) ( a fa ) | _ levél aés az általánosabb GADT szintaxisban:
adatok Fa : Típus -> Írja be ahová Csomópont : Fa a -> Fa a -> Fa a levél : a -> Fa aA függő típusok segítségével a típusellenőrzés szakaszában lehetőség van a típusokat paraméterező értékeket tartalmazó számítások elvégzésére. A következő kód egy statikusan megadott hosszúságú listát határoz meg, amelyet hagyományosan vektornak neveznek :
adatok Vect : Nat -> Type -> Type where Nil : Vect 0 a (::) : ( x : a ) -> ( xs : Vect na ) -> Vect ( n + 1 ) aEz a típus a következőképpen használható:
összes hozzáfűzés : Vect na -> Vect ma -> Vect ( n + m ) a append Nil ys = ys append ( x :: xs ) ys = x :: append xs ysA függvény a típuselemek vektorát hozzáfűzi ma atípuselemek nvektorához a. Mivel a bemeneti vektorok pontos típusa a fordítási időben biztosan ismert értékektől függ, a kapott vektor pontosan (n + m)a típusú elemeket fogja tartalmazni a.
A " " szó az elemzés teljességének ellenőrzéséttotal hívja meg az ellen, amely a végtelen ciklusba való belépés elkerülése érdekében hibát jelez, ha a függvény nem fedi le az összes lehetséges esetét , vagy nem lehet (automatikusan) bizonyítani.
Egy másik példa: két hosszuk szerint paraméterezett vektor páronkénti összeadása:
összesen pár Add : Num a => Vect na -> Vect na -> Vect na pairAdd Nil Nil = Nincs párAdd ( x :: xs ) ( y :: ys ) = x + y :: pairAdd xs ysNumazt jelenti, hogy a típus a típusosztályhoza tartozik . A függvény sikeresen átment a típusellenőrzésen, nem fordulhat elő az az eset, amikor az egyik vektor nulla lesz, míg a második egy szám. A típusrendszer fordításkor ellenőrzi, hogy a két vektor hossza megegyezik-e. Ez leegyszerűsíti a függvény szövegét, amely már nem szükséges ennek a speciális esetnek a kezeléséhez. Num
A függő típusok elég erősek ahhoz, hogy leírják a programok legtöbb tulajdonságát, így az Idris programok fordítási időben bizonyítani tudják az invariánsokat . Ez a nyelvet interaktív próbarendszerré változtatja .
Az Idris kétféle munkamódszert támogat az automatikus ellenőrző rendszerrel: egymást követő taktikahívások írásával ( Coq stílusban, míg a rendelkezésre álló taktikák készlete nem olyan gazdag, mint a Coq-ban, de szabványos metaprogramozási eszközökkel bővíthető ) vagy lépésről lépésre. - Step proof fejlesztés ( Epigram és Agda stílus ).