एपिग्राम (प्रोग्रामिंग भाषा)

Epigram

Paradigm	Functional
द्वारा डिज़ाइन किया गया	Conor McBride James McKinna
Developer	Unmaintained
पहली प्रस्तुति	2004 (2004)
Stable release	1 / October 11, 2006 (2006-10-11)
टाइपिंग अनुशासन	strong, static, dependent
ओएस	Cross-platform: Linux, Windows, macOS
लाइसेंस	MIT
वेबसाइट	web.archive.org/web/20120717070845/http://www.e-pig.org/darcs/Pig09/web/
Influenced by
ALF
Influenced
Agda, Idris

एपिग्राम आश्रित प्रकारों के साथ एक कार्यात्मक प्रोग्रामिंग भाषा है, और एकीकृत विकास वातावरण (आईडीई) आमतौर पर भाषा के साथ पैक किया जाता है। प्रोग्राम विशिष्टताओं को व्यक्त करने के लिए एपिग्राम की प्रकार प्रणाली पर्याप्त मजबूत है। लक्ष्य सामान्य प्रोग्रामिंग से एकीकृत कार्यक्रमों और प्रमाणों में एक सुचारु संक्रमण का समर्थन करना है जिनकी शुद्धता को संकलक द्वारा जांच और प्रमाणित किया जा सकता है। एपिग्राम करी-हावर्ड पत्राचार का उपयोग करता है, इसे प्रस्तावों को प्रकार सिद्धांत भी कहा जाता है, और यह अंतर्ज्ञानवादी प्रकार सिद्धांत पर आधारित है।

एपिग्राम प्रोटोटाइप को जेम्स मैककिन्ना के साथ संयुक्त कार्य के आधार पर कॉनर मैकब्राइड द्वारा कार्यान्वित किया गया था। इसका विकास नॉटिंघम, डरहम, इंग्लैंड, स्कॉट एंड्रयू और रॉयल होलोवे, यूनाइटेड किंगडम (यूके) में लंदन विश्वविद्यालय में एपिग्राम समूह द्वारा जारी रखा गया है। एपिग्राम प्रणाली का वर्तमान प्रायोगिक कार्यान्वयन एक उपयोगकर्ता मैनुअल, एक ट्यूटोरियल और कुछ पृष्ठभूमि सामग्री के साथ मुफ्त में उपलब्ध है। इस सिस्टम का उपयोग Linux, Microsoft Windows और macOS के अंतर्गत किया गया है।

वर्तमान में इसका रखरखाव नहीं किया गया है, और संस्करण 2, जिसका उद्देश्य ऑब्जर्वेशनल टाइप थ्योरी को लागू करना था, कभी भी आधिकारिक तौर पर जारी नहीं किया गया था लेकिन GitHub में मौजूद है।

सिंटेक्स

एपिग्राम LaTeX और ASCII में संस्करणों के साथ, दो-आयामी, प्राकृतिक कटौती शैली वाक्यविन्यास का उपयोग करता है। यहां द एपिग्राम ट्यूटोरियल से कुछ उदाहरण दिए गए हैं:

उदाहरण

प्राकृतिक संख्याएँ

निम्नलिखित घोषणा प्राकृतिक संख्याओं को परिभाषित करती है:

     (         !       (          !   (  n : Nat  !
data !---------! where !----------! ; !-----------!
     ! Nat : * )       !zero : Nat)   !suc n : Nat)

घोषणापत्र में ऐसा कहा गया है Nat टाइप सिस्टम#प्रकारों के प्रकार वाला एक प्रकार है * (यानी, यह एक सरल प्रकार है) और दो कंस्ट्रक्टर: zero और suc. निर्माता suc एक सिंगल लेता है Nat तर्क और रिटर्न ए Nat. यह हास्केल (प्रोग्रामिंग भाषा) घोषणा के बराबर हैdata Nat = Zero | Suc Nat.

LaTeX में, कोड इस प्रकार प्रदर्शित होता है:

${\underline {\mathrm {data} }}\;\left({\frac {}{{\mathsf {Nat}}:\star }}\right)\;{\underline {\mathrm {where} }}\;\left({\frac {}{{\mathsf {zero}}:{\mathsf {Nat}}}}\right)\;;\;\left({\frac {n:{\mathsf {Nat}}}{{\mathsf {suc}}\ n:{\mathsf {Nat}}}}\right)$

क्षैतिज-रेखा संकेतन को यह मानकर पढ़ा जा सकता है कि (जो शीर्ष पर है) वह सत्य है, हम यह अनुमान लगा सकते हैं कि (जो नीचे है) सत्य है। उदाहरण के लिए, मान लीजिए n प्रकार का है Nat, तब suc n प्रकार का है Nat. यदि शीर्ष पर कुछ भी नहीं है, तो निचला कथन हमेशा सत्य होता है:zero प्रकार का है Nat (सभी मामलों में)।

प्राकृतिक पर प्रत्यावर्तन

${\mathsf {NatInd}}:{\begin{matrix}\forall P:{\mathsf {Nat}}\rightarrow \star \Rightarrow P\ {\mathsf {zero}}\rightarrow \\(\forall n:{\mathsf {Nat}}\Rightarrow P\ n\rightarrow P\ ({\mathsf {suc}}\ n))\rightarrow \\\forall n:{\mathsf {Nat}}\Rightarrow P\ n\end{matrix}}$

${\mathsf {NatInd}}\ P\ mz\ ms\ {\mathsf {zero}}\equiv mz$

${\mathsf {NatInd}}\ P\ mz\ ms\ ({\mathsf {suc}}\ n)\equiv ms\ n\ (NatInd\ P\ mz\ ms\ n)$

...और ASCII में:

NatInd : all P : Nat -> * => P zero ->
         (all n : Nat => P n -> P (suc n)) ->
         all n : Nat => P n
NatInd P mz ms zero => mz
NatInd P mz ms (suc n) => ms n (NatInd P mz ms n)

जोड़

${\mathsf {plus}}\ x\ y\Leftarrow {\underline {\mathrm {rec} }}\ x\ \{$

${\mathsf {plus}}\ x\ y\Leftarrow {\underline {\mathrm {case} }}\ x\ \{$

${\mathsf {plus\ zero}}\ y\Rightarrow y$

$\quad \quad {\mathsf {plus}}\ ({\mathsf {suc}}\ x)\ y\Rightarrow {\mathsf {suc}}({\mathsf {plus}}\ x\ y)\ \}\ \}$

...और ASCII में:

plus x y <= rec x {
  plus x y <= case x {
    plus zero y => y
    plus (suc x) y => suc (plus x y)
  }
}

आश्रित प्रकार

एपिग्राम अनिवार्य रूप से दो एक्सटेंशन को छोड़कर, सामान्यीकृत बीजगणितीय डेटा प्रकार एक्सटेंशन के साथ एक टाइप किया हुआ लैम्ब्डा कैलकुलस है। सबसे पहले, प्रकार प्रथम श्रेणी की इकाइयाँ हैं $\star$; प्रकार प्रकार की मनमानी अभिव्यक्तियाँ हैं $\star$, और प्रकार तुल्यता को प्रकार के सामान्य रूपों के संदर्भ में परिभाषित किया गया है। दूसरा, इसका एक आश्रित कार्य प्रकार है; के बजाय $P\rightarrow Q$, $\forall x:P\Rightarrow Q$, कहाँ $x$ में बंधा हुआ है $Q$ उस मान के लिए जो फ़ंक्शन का तर्क (प्रकार का) है $P$) अंततः लेता है।

पूर्ण आश्रित प्रकार, जैसा कि एपिग्राम में लागू किया गया है, एक शक्तिशाली अमूर्तता है। (आश्रित एमएल के विपरीत, निर्भर मूल्य किसी भी वैध प्रकार का हो सकता है।) आश्रित प्रकारों द्वारा लाई गई नई औपचारिक विनिर्देश क्षमताओं का एक नमूना द एपिग्राम ट्यूटोरियल में पाया जा सकता है।

यह भी देखें

• एएलएफ (प्रमाण सहायक), एपिग्राम के पूर्ववर्तियों के बीच एक प्रमाण सहायक।

अग्रिम पठन

• McBride, Conor; McKinna, James (2004). "The view from the left". Journal of Functional Programming. 14: 69–111. doi:10.1017/S0956796803004829. S2CID 6232997.
• McBride, Conor (2004). The Epigram Prototype, a nod and two winks (Report).
• McBride, Conor (2004). The Epigram Tutorial (Report).
• Altenkirch, Thorsten; McBride, Conor; McKinna, James (2005). Why Dependent Types Matter (Report).
• Chapman, James; Altenkirch, Thorsten; McBride, Conor (2006). Epigram Reloaded: A Standalone Typechecker for ETT (Report).
• Chapman, James; Dagand, Pierre-Évariste; McBride, Conor; Morris, Peter (2010). The gentle art of levitation (Report).

बाहरी संबंध

• Official website
• Epigram 1 on GitHub
• Epigram2 on GitHub
• EPSRC on ALF, lego and related; archived version from 2006