Ағылшыншамен салыстырыңыз: абзацты басыңыз — түпнұсқа терезеде ашылады. Абзац астындағы EN түймесі оны мәтін ішінде көрсетеді.
Мазмұны
Кіріспе
Функционалдық бағдарламалау тілі
Functional programming language
Эпиграмма – тәуелді типтері бар функционалдық бағдарламалау тілі, сондай-ақ тілмен бірге әдетте жинақталатын интеграцияланған даму ортасы (IDE). Эпиграмманың типтік жүйесі бағдарламаның сипаттамаларын беруге жеткілікті. Мақсаты – қарапайым бағдарламалаудан интеграцияланған бағдарламалар мен дәлелдемелерге біртекті көшуді қолдау, олардың дұрыстығын компилятор тексеруге және сертификаттауға болады. Эпиграмма Curry-Howard сәйкестігін пайдаланады, сонымен қатар «ұйғарымдарды типтер принципі» деп атайды және интуиционистік типтер теориясына негізделген. Эпиграмманың прототипі Конор Макбрайд Джеймс МакКиннамен бірлескен жұмысының нәтижесінде жасалған. Оның дамуын Ноттингем, Дарем, Сент-Эндрюс және Лондон университетінің (Ұлыбритания) Корольдік Холлоуэйдегі Эпиграмма тобы жалғастыруда. Эпиграмма жүйесінің қазіргі тәжірибелік нұсқасы пайдаланушы нұсқаулығымен, оқулықпен және бірқатар анықтамалық материалдармен бірге тегін қолжетімді. Жүйе Linux, Windows және macOS жүйелерінде қолданылған. Қазіргі уақытта қолдау көрсетілмейді, ал Observational Type Theory-ді іске асыруға бағытталған 2-ші нұсқа ресми түрде жарияланбаған, бірақ GitHub-та бар.
Epigram is a functional programming language with dependent types, and the integrated development environment (IDE) usually packaged with the language. Epigram's type system is strong enough to express program specifications. The goal is to support a smooth transition from ordinary programming to integrated programs and proofs whose correctness can be checked and certified by the compiler. Epigram exploits the Curry–Howard correspondence, also termed the propositions as types principle, and is based on intuitionistic type theory. The Epigram prototype was implemented by Conor McBride based on joint work with James McKinna. Its development is continued by the Epigram group in Nottingham, Durham, St Andrews, and Royal Holloway, University of London in the United Kingdom (UK). The current experimental implementation of the Epigram system is freely available together with a user manual, a tutorial and some background material. The system has been used under Linux, Windows, and macOS. It is currently unmaintained, and version 2, which was intended to implement Observational Type Theory, was never officially released but exists in GitHub.
Синтаксисі
Эпиграмма екі өлшемді, табиғи дедукция стиліндегі синтаксисті пайдаланады, LaTeX және ASCII нұсқалары бар. Мысалдарды «Эпиграмма оқулығынан» қарастырайық:
Epigram uses a two dimensional, natural deduction style syntax, with versions in LaTeX and ASCII. Here are some examples from The Epigram Tutorial:
Табиғи заттарға қайталану
Және ASCII-де:
And in ASCII:
Қосу
Және ASCII-де:
And in ASCII:
Тәуелді типтер
Эпиграмма негізінен типтелген лямбда-есептеу, жалпыланған алгебралық дерек типінің кеңейтімдерімен, екі кеңейтімнен басқа. Біріншіден, типтер – бірінші дәрежелі объектілер, олардың өзінің типі бар; типтер – кез келген типтегі өрнектер, ал типтік теңдестік типтердің нормалды түрлері арқылы анықталады. Екіншіден, оның тәуелді функция типі бар; орнына , , мұнда функция аргументінің ( типі бар) алған мәніне байланысты ішінде байланысқан. Epigram-да жүзеге асырылған толық тәуелді типтер – қуатты абстракция. (Тәуелді ML-ден айырмашылығы, тәуелділікке алынған мән(дер) кез келген жарамды типті болуы мүмкін.) Тәуелді типтердің қамтамасыз ететін жаңа формальды сипаттама мүмкіндіктерінің мысалын Epigram оқулығынан табуға болады.
Epigram is essentially a typed lambda calculus with generalized algebraic data type extensions, except for two extensions. First, types are first class entities, of type ; types are arbitrary expressions of type , and type equivalence is defined in terms of the types' normal forms. Second, it has a dependent function type; instead of , , where is bound in to the value that the function's argument (of type ) eventually takes. Full dependent types, as implemented in Epigram, are a powerful abstraction. (Unlike in Dependent ML, the value(s) depended upon may be of any valid type.) A sample of the new formal specification capabilities dependent types bring may be found in The Epigram Tutorial.