핵심 언어 기능

핵심 언어 기능 (Core Language Features)

Idris의 핵심 언어가 제공하는 기능을 정리한 목록이에요. 각 기능에 대한 자세한 설명은 대부분 별도의 참조 문서 페이지에서 다루고 있어요.

출처: 문서

본문

Idris는 다음과 같은 핵심 언어 기능을 갖추고 있어요.

  • 전체 스펙트럼 의존 타입 (full-spectrum dependent types)

  • 엄격한 평가 (strict evaluation) — 명시적 지연을 위해 Lazy : Type -> Type 타입 생성자를 추가로 제공

  • 람다(Lambda), 파이(Pi, forall), let 바인딩

  • 패턴 매칭 정의

  • 접근 수정자 public, abstract, private 내보내기(export)

  • 함수 옵션 partial, total

  • where 절(clauses)

  • "magic with"

  • 묵시적 인자 (implicit arguments, 최상위 타입에서)

  • "묶인(bound)" 묵시적 인자 — {n : Nat} -> {a : Type} -> Vect n a

  • "묶이지 않은(unbound)" 묵시적 인자 — 타입에서 Vect n a는 위의 형태와 동등하며, n과 a는 묵시적으로 묶여요. 이는 인자 위치에서 소문자로 시작하는 이름에 적용돼요.

  • '택틱(tactic)' 묵시적 인자 — 통일(unification)이 아니라 택틱 스크립트를 실행하거나 기본 인자를 주는 방식으로 풀리는 인자

  • 단위 타입 ()과 빈 타입 Void

  • 튜플 (중첩된 쌍으로 desugar됨)

  • 의존 쌍 문법 (x : T ** P x) — 타입 T의 어떤 x에 대해 P x가 성립함을 뜻함

  • 인라인 case 표현식

  • 이종 동등성 (heterogeneous equality)

  • do 표기법

  • 관용구 괄호 (idiom brackets)

  • 인터페이스 (Interfaces, 타입 클래스와 유사) — 기본 메서드와 메서드 간 의존성 지원

  • rewrite prf in expr

  • 메타변수 (Metavariables)

  • 인라인 증명/택틱 스크립트

  • 묵시적 강제 변환 (implicit coercion)

  • codata

  • 데이터/공-데이터 혼합을 위한 Inf : Type -> Type 타입 생성자. 실제로 codata는 재귀 인자를 Inf 아래에 두는 방식으로 구현돼요.

  • 패턴 및 용어 문법적 설탕(syntactic sugar)을 정의하기 위한 문법 규칙(syntax rules) — 표준 라이브러리에서 if ... then ... else 표현식과 Agda 스타일의 preorder 추론 문법을 정의하는 데 사용돼요.

  • UniqueType 유니버스를 사용한 유일성(Uniqueness) 타입 시스템

  • %static 인자 주석을 통한 부분 평가(partial evaluation)

  • 오류 메시지 반영 (error message reflection)

  • 소거자(Eliminators)

  • 레이블 타입 'name

  • %logging n

  • %unifyLog

더 알아보기 (Learn more)