핵심 언어

핵심 언어 (Core language)

Agda의 프로그램은 *.agda 파일에 작성된 여러 선언으로 구성돼요. 선언은 새 식별자를 도입하고 그 타입과 정의를 부여해요. 다음을 선언할 수 있어요:

  • 데이터 타입
  • 레코드 타입 (공유도 레코드 포함)
  • 함수 정의 (mixfix 연산자, 추상 정의, 불투명 정의 포함)
  • 모듈
  • 로컬 정의 let과 where
  • postulate
  • 변수
  • 패턴 동의어
  • 우선순위 (fixity)
  • 프래그마, 그리고
  • 프로그램 옵션

선언에는 시그니처 부분과 정의 부분이 있어요. 이것들은 프로그램에서 따로 나타날 수 있어요. 이름은 사용되기 전에 선언되어야 하지만, 시그니처와 정의를 분리함으로써 상호 재귀로 사물을 정의하는 것이 가능해요.

문법 (Grammar)

핵심적으로 Agda는 의존 타입 람다 계산법이에요. a가 일반 항을 나타내는 경우 항의 문법은 다음과 같아요:

a ::= x                       -- variable
    | λ x → a                 -- lambda abstraction
    | f                       -- defined function
    | (x : a) → a             -- function space
    | F                       -- data/record type
    | c a                     -- data/record constructor
    | s                       -- sort Seti, Setω+i

문법 개요 (Syntax overview)

Agda 프로그램의 문법은 세 가지 핵심 구성 요소로 정의돼요:

  • 표현식(Expressions)은 함수 본문과 타입을 작성해요.
  • 선언(Declarations)은 타입, 데이터 타입, postulate, 레코드, 함수 등을 선언해요.
  • 프래그마(Pragmas)는 프로그램 옵션을 정의해요.

또한 해석의 서로 다른 레벨에 해당하는 세 가지 주요 문법 수준이 있어요:

  • 구체(Concrete)는 사용자가 정확히 쓴 것을 나타내는 고수준 설탕 문법이에요 (Agda.Syntax.Concrete).
  • 추상(Abstract)은 타입 체킹 전의 것이에요 (Agda.Syntax.Abstract).
  • 내부(Internal)은 타입 체크된 완전히 해석된 핵심 Agda 항에 해당해요 (Agda.Syntax.Internal에 대략 대응).

*.agda 파일을 실행 가능한 것으로 번역하는 과정은 여러 단계가 있어요:

*.agda file
   ==[ parser (Lexer.x + Parser.y) ]==>
Concrete syntax
   ==[ nicifier (Syntax.Concrete.Definitions) ]==>
'Nice' concrete syntax
   ==[ scope checking (Syntax.Translation.ConcreteToAbstract) ]==>
Abstract syntax
   ==[ type checking (TypeChecking.Rules.*) ]==>
Internal syntax
   ==[ Agda.Compiler.ToTreeless ]==>
Treeless syntax
   ==[ different backends (Compiler.MAlonzo.*, Compiler.JS.*, ...) ]==>
Source code
   ==[ different compilers (GHC compiler, ...) ]==>
Executable

다음 섹션에서 이 단계들을 더 자세히 설명할게요.

렉서 (Lexer)

어휘 분석(일명 토큰화)은 문자 수열(원시 *.agda 파일)을 토큰 수열(의미를 가진 문자열)로 변환하는 과정이에요.

Agda의 렉서는 Alex로 생성되며 GHC의 렉서를 각색한 것이에요. 주요 렉싱 함수 lexer는 Agda.Syntax.Parser.Parser가 호출해 입력에서 다음 토큰을 가져와요.

파서 (Parser)

파서는 렉서의 출력을 받아 우리가 구체 문법(Concrete Syntax)이라 부를 데이터 구조를 구축하면서 올바른 문법인지 검사하는 구성 요소예요.

파서는 Happy로 생성돼요.

예: 이름이 부분들의 수열일 때, 렉서는 그것을 문자열로만 보고 파서는 이 단계에서 번역을 해요.

구체 문법 (Concrete Syntax)

구체 문법은 desugaring이 전혀 없는 프로그램 텍스트의 원시 표현이에요. 이것이 파서가 만드는 것이에요. 아이디어는 구체 문법을 유지하는 방법을 알아내면 사용자가 쓴 대로 정확히 출력할 수 있다는 것이에요.

Nice 구체 문법 (Nice Concrete Syntax)

Nice 구체 문법은 내부적으로 다루기 더 쉬운 구체 문법의 약간 재구성된 버전이에요. 특히 다음을 해요:

  • 상호 블록 감지
  • 고립된 부분으로부터 정의 조립
  • mixfix 연산자의 결합도 정보 수집 및 정의에 부착
  • 잠재적으로 의도치 않았지만 여전히 유효한 선언에 대한 경고 방출. 이는 본질적으로 빈 instance 블록과 잘못 배치된 프래그마 같은 죽은 코드예요.

추상 문법 (Abstract Syntax)

Agda.Syntax.Concrete에서 Agda.Syntax.Abstract로의 번역은 스코프 분석, infix 연산자 우선순위 파악, 정의 정리를 수반해요.

추상 문법 Agda.Syntax.Abstract는 구체 문법의 desugaring과 스코프 분석 후의 결과예요. 타입 체커는 추상 문법에서 작업해 내부 문법을 생산해요.

내부 문법 (Internal Syntax)

이것은 백엔드 중 하나로 넘겨지기 전의 문법의 마지막 단계예요. 항은 잘 스코프되고 잘 타입되어 있어요.

내부 문법을 생산하는 동안 항은 안전성에 대해 검사돼요. 이 안전성 검사는 함수에 대한 종료 검사와 커버리지 검사를, 데이터 타입에 대한 양성 검사를 의미해요.

instance 해석과 오버로드된 생성자(같은 이름을 가진 서로 다른 생성자)의 모호성 해소 같은 타입-지향 연산도 여기서 발생해요.

내부 문법 Agda.Syntax.Internal은 위에 제시된 Term 문법을 나타내기 위해 다음 haskell 데이터 타입을 사용해요.

data Term = Var {-# UNPACK #-} !Int Elims -- ^ @x es@ neutral
        | Lam ArgInfo (Abs Term)        -- ^ Terms are beta normal. Relevance is ignored
        | Lit Literal
        | Def QName Elims               -- ^ @f es@, possibly a delta/iota-redex
        | Con ConHead ConInfo Elims
        -- ^ @c es@ or @record { fs = es }@
        --   @es@ allows only Apply and IApply eliminations,
        --   and IApply only for data constructors.
        | Pi (Dom Type) (Abs Type)      -- ^ dependent or non-dependent function space
        | Sort Sort
        | Level Level
        | MetaV {-# UNPACK #-} !MetaId Elims

Treeless 문법 (Treeless Syntax)

Treeless 문법은 컴파일러 백엔드의 입력으로 사용되기 위한 것이에요. 내부 문법보다 더 저수준이며 타입 체킹에는 사용되지 않아요. Treeless 문법의 몇 가지 특징은 다음과 같아요:

  • 케이스 트리 대신 case 표현식
  • 인스턴스화된 데이터 타입/생성자 없음

예를 들어 Glasgow Haskell Compiler (GHC) 백엔드는 treeless 문법을 적절한 GHC Haskell 프로그램으로 번역해요. 사용될 수 있는 또 다른 백엔드는 treeless 문법을 JavaScript 코드로 번역하는 JavaScript 백엔드예요.

프로그램의 treeless 표현은 A-normal form (ANF)을 가져요. 즉 모든 case 표현식이 단일 변수를 대상으로 하고, 모든 대안은 하나의 생성자만 벗겨낼 수 있어요.

백엔드는 임의의 표현식에 대해 case를 수행하고 깊은 패턴을 사용할 수 있는 언어의 문법보다 ANF 문법을 더 쉽게 다룰 수 있어요.

더 알아보기 (Learn more)