어휘 구조

어휘 구조 (Lexical Structure)

Agda 코드는 확장자가 .agda인 UTF-8 인코딩된 일반 텍스트 파일에 작성돼요. 리터레이티브 프로그래밍(Literate Programming)을 위해 더 많은 파일 확장자가 지원돼요.

파일 시작 부분의 UTF-8 바이트 순서 표시(BOM)는 무시돼요.

대부분의 유니코드 문자는 식별자에 사용할 수 있어요 (이름 섹션 참고).

공백이 중요해요 (레이아웃 섹션 참고).

토큰 (Tokens)

키워드와 특수 기호 (Keywords and special symbols)

대부분의 비-공백 유니코드는 Agda 이름의 일부로 사용할 수 있지만 두 종류의 예외가 있어요:

  • 특수 기호 (special symbols): 이름에 전혀 나타날 수 없는 특별한 의미를 가진 문자. 이들은 .;{}()@"이에요.
  • 키워드 (keywords): 이름의 일부로 나타날 수 없지만 다른 문자와 함께 이름에 나타날 수 있는 예약어.

예약된 키워드는 다음과 같아요:

= | -> → : ? \ λ
∀ .. ...
abstract
coinductive
constructor
data
do
eta-equality
field
forall
hiding
import
in
inductive
infix
infixl
infixr
instance
interleaved
let
macro
module
mutual
no-eta-equality
opaque
open
overlap
pattern
postulate
primitive
private
public
quote
quoteTerm
record
renaming
rewrite
syntax
tactic
unfolding
unquote
unquoteDecl
unquoteDef
using
variable
where
with

renaming 지시에서의 키워드는 to가 renaming 지시에서만 예약된다는 점에 주의하세요.

import 문장에서의 키워드는 as가 import 문장에서 특별한 의미를 갖지만 예약되지는 않아요.

이름 (Names)

한정 이름(qualified name)은 점(.)으로 구분된 이름들의 비어 있지 않은 수열이에요. 이름은 이름 부분과 밑줄(_)의 교대 수열이며, 적어도 하나의 이름 부분을 포함해요. 이름 부분은 공백, 밑줄, 특수 기호를 제외한 유니코드 문자의 비어 있지 않은 수열이에요.

이름 부분은 위의 키워드 중 하나일 수 없고, 작은따옴표(')(문자 리터럴에 사용됨, 아래 리터럴 참고)로 시작할 수 없어요.

예:

  • 유효: data?, ::, if_then_else_, 0b, _⊢_∈_, x=y
  • 무효: data_?, foo__bar, _, a;b, [_.._]

이름의 밑줄은 이름이 연산자로 사용될 때 인자가 들어갈 위치를 나타내요. 예를 들어 적용 _+_ 1 2는 1 + 2로 쓸 수 있어요. 자세한 내용은 Mixfix 연산자를 참고하세요. 대부분의 문자 수열이 유효한 이름이므로 공백은 다른 언어보다 더 중요해요. 위 예에서 + 주변의 공백이 필요한데, 1+2는 유효한 이름이기 때문이에요.

한정 이름은 다른 모듈에서 정의된 엔티티를 참조하는 데 사용돼요. 예를 들어 Prelude.Bool.true는 모듈 Prelude.Bool에서 정의된 이름 true를 가리켜요. 자세한 내용은 모듈 시스템을 참고하세요.

리터럴 (Literals)

리터럴 값에는 네 가지 유형이 있어요: 정수, 부동 소수점, 문자, 문자열. 대응하는 타입은 빌트인을, 사용자 정의 타입에 대한 리터럴 지원 방법은 리터럴 오버로딩을 참고하세요.

정수 (Integers)

10진, 16진(0x 접두사), 또는 2진(0b 접두사) 표기의 정수 값. 문자 _를 사용해 숫자 그룹을 분리할 수 있어요. 음이 아닌 숫자는 기본적으로 내장 자연수에 매핑되지만 오버로드될 수 있어요. 음수에는 기본 해석이 없고 오버로딩을 통해서만 사용할 수 있어요.

예: 123, 0xF0F080, -42, -0xF, 0b11001001, 1_000_000_000, 0b01001000_01001001.

부동 소수점 (Floats)

표준 표기법(대괄호는 선택 사항을 나타내요)의 부동 소수점 숫자:

float    ::= [-] decimal . decimal [exponent]
           | [-] decimal exponent
exponent ::= (e | E) [+ | -] decimal

이들은 내장 float에 매핑되고 오버로드할 수 없어요.

예: 1.0, -5.0e+12, 1.01e-16, 4.2E9, 50e3.

문자 (Characters)

문자 리터럴은 작은따옴표(')로 둘러싸여 있어요. '나 \가 아닌 단일 (유니코드) 문자이거나, 이스케이프된 문자일 수 있어요. 이스케이프된 문자는 백슬래시 \와 이스케이프 코드로 시작해요. 이스케이프 코드는 0과 0x10ffff (1114111) 사이의 10진 또는 16진(x 접두사) 자연수이거나, 다음 특수 이스케이프 코드 중 하나예요:

코드 ASCII 코드 ASCII 코드 ASCII 코드 ASCII
a 7 b 8 t 9 n 10
v 11 f 12 \ \ ' '
" " NUL 0 SOH 1 STX 2
ETX 3 EOT 4 ENQ 5 ACK 6
BEL 7 BS 8 HT 9 LF 10
VT 11 FF 12 CR 13 SO 14
SI 15 DLE 16 DC1 17 DC2 18
DC3 19 DC4 20 NAK 21 SYN 22
ETB 23 CAN 24 EM 25 SUB 26
ESC 27 FS 28 GS 29 RS 30
US 31 SP 32 DEL 127

문자 리터럴은 내장 문자 타입에 매핑되고 오버로드할 수 없어요.

예: 'A', '∀', '\x2200', '\ESC', '\32', '\n', '\'', '"'.

문자열 (Strings)

문자열 리터럴은 큰따옴표 "로 둘러싸인 (이스케이프될 수 있는) 문자들의 수열이에요. 문자 리터럴과 같은 규칙을 따르지만, 작은따옴표 ' 대신 큰따옴표 "가 이스케이프되어야 한다는 점만 달라요. 문자열 리터럴은 기본적으로 내장 문자열 타입에 매핑되지만 오버로드될 수 있어요.

예: "Привет \"мир\"\n".

홀 (Holes)

홀은 Emacs 모드가 지원하는 대화형 개발의 필수 부분이에요. {!와 !} 사이에 둘러싸인 모든 텍스트는 홀이고 중첩된 홀을 포함할 수 있어요. 내용이 없는 홀은 ?로 쓸 수 있어요. 홀의 내용에 대해 동작하는 여러 Emacs 명령이 있어요. 타입 체커는 홀의 내용을 무시하고 그것을 알 수 없는(unknown) 것으로 취급해요 (암시 인자 참고).

예: {! f {!x!} 5 !}

주석 (Comments)

한 줄 주석은 이중 대시 -- 다음에 임의의 텍스트로 작성돼요. 여러 줄 주석은 {-와 -}로 둘러싸여 있고 중첩될 수 있어요. 주석은 문자열 리터럴에 나타날 수 없어요.

예:

{- Here is a {- nested -}
   comment -}
s : String --line comment {-
s = "{- not a comment -}"

프래그마 (Pragmas)

프래그마는 {-#와 #-}로 둘러싸인 시스템에 특별한 의미를 가진 특수 주석이에요. 프래그마의 전체 목록은 Pragmas를 참고하세요.

레이아웃 (Layout)

Agda는 Haskell과 비슷한 규칙으로 레이아웃에 민감하며, 레이아웃이 필수라는 점이 예외예요: 명시적 {, }와 ;를 사용해 레이아웃을 피할 수 없어요.

레이아웃 블록은 문장의 수열을 포함하며 레이아웃 키워드 중 하나로 시작돼요:

abstract
constructor
do
field
instance
let
macro
mutual
opaque
postulate
primitive
private
variable
where

레이아웃 키워드 다음의 첫 번째 토큰이 블록의 들여쓰기를 결정해요. 이보다 더 들여쓰기된 모든 토큰은 이전 문장의 일부이고, 같은 레벨의 토큰은 새 문장을 시작하며, 덜 들여쓰기된 토큰은 블록 밖에 있어요.

data Nat : Set where -- starts a layout block
    -- comments are not tokens
  zero : Nat      -- statement 1
  suc  : Nat →    -- statement 2
         Nat      -- also statement 2

one : Nat -- outside the layout block
one = suc zero

레이아웃 키워드의 들여쓰기는 중요하지 않다는 점에 주의하세요.

레이아웃 키워드로 시작되는 여러 레이아웃 블록이 줄 바꿈 없이 연속으로 있으면(블록 주석 안의 줄 바꿈은 세지 않음), 마지막 블록보다 더 들여쓰기된 블록들은 수동(passive) 상태가 되어 새 문장으로 더 확장될 수 없어요:

private module M where postulate
          A : Set                 -- module-block goes passive
          B : Set                 -- postulate-block can still be extended
        module N where            -- private-block can still be extended

Agda 파일은 하나의 최상위 레이아웃 블록을 포함하며, 최상위 모듈의 내용은 들여쓰기될 필요가 없다는 특별 규칙이 적용돼요.

module Example where
NotIndented : Set₁
NotIndented = Set

리터레이트 Agda (Literate Agda)

Agda는 LaTeX, Markdown, reStructuredText 같은 여러 조판 도구로 리터레이티브 프로그래밍을 지원해요. 예를 들어 LaTeX에서는 \begin{code}, \end{code}로 둘러싸이지 않으면 파일의 모든 것이 주석이에요. 리터레이트 Agda 파일은 특별한 파일 확장자를 가져요. .agda 대신 LaTeX용 .lagda와 .lagda.tex, Markdown용 .lagda.md, reStructuredText용 .lagda.rst 등이에요. 리터레이트 Agda 파일의 한 용도는 Agda 코드를 포함하는 문서를 생성하는 것이에요. 자세한 내용은 HTML 생성과 LaTeX 생성을 참고하세요.

\documentclass{article}
% some preamble stuff
\begin{document}
Introduction usually goes here
\begin{code}
module MyPaper where
  open import Prelude
  five : Nat
  five = 2 + 3
\end{code}
Now, conclusions!
\end{document}

더 알아보기 (Learn more)