에피그램(프로그래밍 언어)

이 문서에는 여러 가지 문제가 있습니다.개선을 돕거나 토크 페이지에서 이러한 문제에 대해 논의해 주십시오.(이러한 템플릿메시지를 삭제하는 방법과 타이밍에 대해 설명합니다) 이 문서의 주제는 위키피디아의 일반적인 알림 가이드라인을 충족하지 못할 수 있습니다. 주제와는 무관하고 단순한 언급을 넘어 상당한 내용을 다루는 신뢰할 수 있는 2차 출처를 인용함으로써 주제 인지도를 입증할 수 있도록 도와주시기 바랍니다. 알림을 표시할 수 없는 경우 문서가 병합, 리디렉션 또는 삭제될 수 있습니다.출처 : "Epigram" 프로그래밍 언어– 뉴스 · 신문 · 서적 · 학자 · JSTOR (2019년 8월) (이 템플릿 메시지 삭제 방법 및 삭제 시기 확인) 이 문서에는 참고 자료, 관련 읽기 또는 외부 링크가 포함되어 있지만 인라인 인용이 부족하여 출처가 불분명합니다. 좀 더 정확한 인용문을 도입하여 개선해 주시기 바랍니다. (2019년 8월) (템플릿 메시지 삭제 방법 및 삭제 시기 확인) (이 템플릿메시지를 삭제하는 방법과 타이밍을 확인합니다)

에피그램은 종속형 및 통합 개발 환경(IDE)을 사용하는 기능성 프로그래밍 언어입니다.에피그램의 타입 시스템은 프로그램 사양을 표현할 수 있을 정도로 강력합니다.목표는 일반적인 프로그래밍에서 컴파일러에 의해 정확성이 확인되고 인증될 수 있는 통합 프로그램 및 증명으로 원활하게 이행할 수 있도록 지원하는 것입니다.에피그램은 또한 명제들을 유형 원리라고 부르는 커리-하워드 대응관계를 이용하며, 직관적인 유형 이론에 기초한다.

에피그램 프로토타입은 코너 맥브라이드가 제임스 맥키나와의 공동 작업을 기반으로 구현했습니다.이 개발은 영국 런던대학교의 노팅엄, 더럼, 세인트 앤드류스, 로얄 할로웨이에 있는 에피그램 그룹에 의해 계속된다.에피그램 시스템의 현재 실험 구현은 사용자 설명서, 튜토리얼 및 일부 배경 자료와 함께 자유롭게 사용할 수 있습니다.시스템은 Linux, Windows 및 MacOS에서 사용되고 있다.

현재는 유지보수가 되지 않고 있으며, Observational Type Theory를 구현하기 위한 Version 2는 공식적으로 공개되지 않고 GitHub에 존재합니다.

구문

에피그램은 LaTeX 및 ASCII 버전의 2차원 자연감소 스타일 구문을 사용합니다.다음은 에피그램 튜토리얼의 몇 가지 예입니다.

예

자연수

다음 선언은 자연수를 정의합니다.

 ( ! ( n : Nat 데이터 !------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------

선언문에 의하면Nat종류가 있는 타입입니다. *(즉, 단순한 유형) 및 두 개의 시공자:zero그리고.suc. 컨스트럭터suc싱글을 찍다Nat인수 및 반환Nat이는 해스켈 선언에 해당한다.data Nat = Zero Suc Nat".

LaTeX 에서는, 코드는 다음과 같이 표시됩니다.

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

수평선 표기법은 "위쪽에 있는 것이 참이라고 가정하면 아래쪽에 있는 것이 참이라고 추론할 수 있다"라고 읽을 수 있다.예를 들어, '가정'은n종류Nat,그리고나서suc n종류Nat위쪽에 아무것도 없는 경우 아래 문장은 항상 참입니다.zero종류Nat(모든 경우)."

자연 재귀

${\displaystyle {NatInd}:\begin{matrix}\forall P:{\mathsf {Nat}}\rightarrow P\\\(\forall n:{\mathsf {zero}}\rightarrow P\({\f}\f})$

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

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

ASC에서는II:

NatInd : all P : Nat -> * => P zero -> (all n : Nat => P n -> P (sublic n) -> all n : Nat => P NatInd P mz 0 = mz NatInd P mz ms (s ) = ms Nat Nat Nat Nz

추가

$\displaystyle \ mathsf { plus } \ x \ y \ row line line 。$

$(*displaystyle {mathsf {plus}}\x\y\왼쪽 화살표)$

$(\displaystyle\mathsf {plus\zero}\y 오른쪽 화살표 y)$

$\displaystyle \quad \quad {plus}\{\mathsf {suc}\x}\y\rightarrow {\mathsf {plus}\x}\}\}$

ASC에서는II:

+ x y <= rec x { + x y <= 대/소문자 x { + 0 y => y + (소문자 x) y => suc (+ x y) } }

종속 유형

에피그램은 기본적으로 두 개의 확장자를 제외하고 일반화 대수 데이터형 확장자를 가진 유형 람다 미적분입니다.첫째, 유형은 유형 ${\$ {\$displaystyle \star$ 유형은 유형${\$ {\$displaystyle \star$의 임의 표현이며 유형 등가는 유형의 정규 형식으로 정의됩니다.둘째, P $Q$ \ $displaystyle$P \ $right arrow$Q $대신{\displaystyle }$$$x$$: $P$Q \ $displaystyle$x$$:$P$ \ $right$ $arrow$$$Q \$$$displaystyle$ x$$는 $함수$ 인수$(표시$ $유형$ P$)$ 값에 바인딩됩니다.

Epigram에서 구현된 완전 종속 유형은 강력한 추상화입니다(의존 ML과 달리 종속된 값은 유효한 유형일 수 있습니다).종속 유형에 따라 제공되는 새로운 공식 규격 기능의 샘플은 에피그램 자습서에서 확인할 수 있습니다.

「 」를 참조해 주세요.

• 에피그램의 전임자 중 한 명인 ALF.

추가 정보

• McBride, Conor; McKinna, James (2004). "The view from the left". Journal of Functional Programming. 14: 69–111. doi:10.1017/S0956796803004829.
• 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).

외부 링크

• 공식 웹사이트
• GitHub의 에피그램 1
• GitHub의 에피그램2
• ALF, 레고 및 관련 EPSRC, 2006년 아카이브 버전

레퍼런스