믹스픽스 연산자
믹스픽스 연산자 (Mixfix Operators)
타입 이름, 함수 이름, 생성자 이름은 그것을 밑줄 문자 _로 구분해 하나 이상의 이름 부분(part)으로 구성할 수 있고, 그 결과 이름은 연산자로 사용할 수 있어요. 왼쪽에서 오른쪽으로 각 인자는 각 밑줄 _의 자리로 들어가요.
예를 들어 if, then, else 이름 부분을 밑줄로 결합해 if_then_else_라는 단일 이름으로 만들 수 있어요:
if_then_else_ : {A : Set} → Bool → A → A → A
if true then x else y = x
if false then x else y = y
함수 이름 if_then_else_를 어떤 인자 x, y, z에 적용하는 것은 다음과 같이 쓸 수 있어요:
전체 이름 if_then_else_ x y z를 사용한 표준 적용:
_ = if_then_else_ x y z
인자를 이름 부분 사이에 배치한 연산자 적용 if x then y else z:
_ = if x then y else z
전체 이름의 다른 부분, 예를 들어 밑줄을 하나 또는 둘 남긴 형태:
_ = (if_then y else z) x
_ = (if x then_else z) y
_ = if x then y else_ z
_ = if x then_else_ y z
_ = if_then y else_ x z
_ = (if_then_else z) x y
믹스픽스 연산자는 함수에 국한되지 않고 타입과 생성자의 이름으로도 허용돼요:
-- 인픽스 타입 연산자 _≡_
data _≡_ {A : Set} : (a b : A) → Set where
refl : {a : A} → a ≡ a
-- 인픽스 생성자 _∷_
data List (A : Set) : Set where
nil : List A
_∷_ : A → List A → List A
우선순위 (Precedence)
각 연산자는 우선순위(precedence)와 결부되어 있는데, 이는 부동소수점 숫자(음수와 분수도 가능!)예요. 연산자의 기본 우선순위는 20이에요. 동일성(equality)을 구성하는 타입 연산자는 보통 4 같은 낮은 우선순위가 주어져요:
infix 4 _≡_
우선순위에 대한 다음 논의에서는 다음 연산자들을 가정해요:
_and_ : Bool → Bool → Bool
true and x = x
false and _ = false
_⇒_ : Bool → Bool → Bool
true ⇒ b = b
false ⇒ _ = true
표현식 false and true ⇒ false를 생각해 봐요. _and_와 _⇒_ 중 어느 것에 우선순위가 주어지느냐에 따라 (false and true) ⇒ false(값은 true)로 읽거나 false and (true ⇒ false)(값은 false)로 읽을 수 있어요.
_and_에 _⇒_보다 더 높은 우선순위를 주면 첫 번째 결과를 얻어요:
infix 30 _and_
-- infix 20 _⇒_ (기본값)
variable
x y z : Bool
p-and : x and y ⇒ z ≡ (x and y) ⇒ z
p-and = refl
e-and : false and true ⇒ false ≡ true
e-and = refl
하지만 새 연산자 _and’_를 선언하고 _⇒_보다 낮은 우선순위를 주면 두 번째 결과를 얻어요:
_and’_ : Bool → Bool → Bool
_and’_ = _and_
infix 15 _and’_
-- infix 20 _⇒_ (기본값)
p-⇒ : x and’ y ⇒ z ≡ x and’ (y ⇒ z)
p-⇒ = refl
e-⇒ : false and’ true ⇒ false ≡ false
e-⇒ = refl
고정성(fixity)은 renaming 지시어로 임포트할 때 바꿀 수 있어요:
open M using (_∙_)
open M renaming (_∙_ to infixl 10 _*_)
이 코드는 연산자 _∙_의 두 인스턴스를 스코프로 가져와요: 첫 번째는 _∙_라는 이름에 원래 고정성, 두 번째는 _*_라는 이름에 우선순위 10의 왼쪽 결합 연산자처럼 동작하도록 고정성이 바뀐 형태예요.
결합성 (Associativity)
표현식 true ⇒ false ⇒ false를 생각해 봐요. _⇒_가 왼쪽 또는 오른쪽으로 결합하느냐에 따라 (false ⇒ true) ⇒ false = false 또는 false ⇒ (true ⇒ false) = true로 읽을 수 있어요.
연산자 _⇒_를 infixr로 선언하면 오른쪽으로 결합해요:
infixr 20 _⇒_
p-right : x ⇒ y ⇒ z ≡ x ⇒ (y ⇒ z)
p-right = refl
e-right : false ⇒ true ⇒ false ≡ true
e-right = refl
연산자 _⇒’_를 infixl로 선언하면 왼쪽으로 결합해요:
infixl 20 _⇒’_
_⇒’_ : Bool → Bool → Bool
_⇒’_ = _⇒_
p-left : x ⇒’ y ⇒’ z ≡ (x ⇒’ y) ⇒’ z
p-left = refl
e-left : false ⇒’ true ⇒’ false ≡ false
e-left = refl
폐쇄·전치·후치 연산자 (Closed, pre-, and postfix operators)
내부 홀(hole) _만 있는 연산자를 폐쇄(closed) 연산자라고 해요. 예: [_]나 begin_end 또는 ⟨_∣_⟩. 이들은 고정성 선언이 필요 없어요. 그럼에도 하나를 제공하면 FixityDeclarationForNonOperator 경고가 발생해요. 이 경고는 연산자가 전혀 아닌 infix 42 true 같은 이름에 고정성을 선언해도 발생해요.
일반적으로 우선순위는 내부 홀에는 적용되지 않아요. 결과적으로 연산자를 폐쇄·전치(pre-), 후치(post-), 인픽스로 분류하는 것은 이름의 양 끝(시작 또는 끝)에 있는 홀만 고려해요.
인픽스 연산자는 양쪽에 홀이 있어요. 예: _⇒_와 _and_, 그리고 _≡⟨_⟩_도. 이들은 왼쪽 결합, 오른쪽 결합, 또는 비결합일 수 있어요.
전치 연산자는 왼쪽에 홀이 있어요. 예: -_ 또는 if_then_else_. 이들은 자연스럽게 항상 오른쪽으로 결합해요. 예를 들어 - - 5는 - (- 5)를 의미해요; 대안인 (- -) 5는 무의미해요.
후치 연산자는 오른쪽에 홀이 있어요. 예: _! 또는 _∎ 또는 _[_/_]. 이들은 자연스럽게 항상 왼쪽으로 결합해요.
폐쇄 연산자는 어느 쪽에도 없어요.
Agda는 현재 전치·후치 연산자에 대한 특정 우선순위 선언이 부족해서 infix, infixl, infixr 중 아무거나 받아들여요. 예를 들어 infix 6 -_는 작동해요.
참고: 전치·후치 연산자의 사용에서 우선순위가 중요하지 않아야 할 때조차, Agda는 잘못된 우선순위를 가진 항을 거부해요. 예를 들어
4 + - 3은_+_가-_보다 높은 우선순위를 가지지 않는 한 거부돼요. (이슈 #1448 참고.)
모호성과 스코프 (Ambiguity and Scope)
연산자의 고정성을 아직 선언하지 않았다면, Agda는 그것을 모호하게 사용하려고 하면 불평해요:
e-ambiguous : Bool
e-ambiguous = true ⇒ true ⇒ true
Could not parse the application true ⇒ true ⇒ true
Operators used in the grammar:
⇒ (infix operator, level 20)
고정성 선언은 모듈 본문의 어디에나 나타날 수 있어요. 그것들은 그것이 나타나는 전체 스코프에 적용돼요 (즉, 앞뒤 모두, 하지만 밖은 아님).
핵심 연산자 (Core operators)
적용(juxtaposition)과 함수 타입 생성자 →는 파서에서 직접 처리되며 사용자가 우선순위와 결합성을 할당할 수 없어요. 하지만 연산자 프레임워크에서 그것들을 다음과 같이 이해할 수 있어요:
함수 타입 생성자 →는 최소 우선순위(-∞)의 오른쪽 결합 연산자예요. 사용자가 정의한 어떤 연산자든 →보다 강하게 결합해요.
적용은 최대 우선순위(+∞)의 왼쪽 결합 연산자예요. 그것은 사용자가 정의한 어떤 연산자보다 강하게 결합해요.
텔레스코프의 연산자 (Operators in telescopes)
Agda는 아직 텔레스코프에서 선언된 연산자의 고정성 선언을 지원하지 않아요. 이슈 #1235 참고.
이것은 let 바인딩을 통해 연산자에 별명을 붙이면 해결할 수 있는데, 여기에 고정성 선언을 포함할 수 있어요:
module _ {A : Set} (_+_ : A → A → A) (let infixl 5 _+_; _+_ = _+_) where