단락이 모나드 계산에 "재미"의 경우

Question

이 같은 Data.Maybe.monad을 사용하는 기능이 있습니다 유사한

typeCheck ν (f · e) = 
    typeCheck ν e >>= λ { (u , e′) → 
    typeCheck ν f >>= λ { (u′ ▷ t , f′) → 
    u !≡ₜ u′  >>= λ { refl → 
    pure (, (f′ · e′)) }; 
    _ → nothing }} 

가 _ → nothing 케이스를 제거하거나 방법이있다, 또는 적어도 더 위로 이동을 (Idris에게) 다음과 비슷한 것을 얻으십시오 :

typeCheck ν (f · e) = 
    typeCheck ν e >>= λ { (u , e′) → 
    typeCheck ν f >>= λ { _ → nothing; (u′ ▷ t , f′) → 
    u ≡!ₜ u′  >>= λ { refl → 
    pure (, (f′ · e′)) }}} 

Answer 1

Agda는 do-notation입니다. 설명서의 예 :

infer Γ (app e e₁) = do 
    s ofType A => B ← infer Γ e 
    where _ ofType nat → typeError "numbers cannot be applied to arguments" 
    t ofType A₁  ← infer Γ e₁ 
    refl   ← A =?= A₁ 
    pure (app s t ofType B)