短絡する「面白くない」例

Question

私はこのようなData.Maybe.monadを使用する関数があります。

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

を_ → nothingケースをなくす、あるいは少なくともアップ（似たさらにそれを移動するためのいずれかの方法はあります次のようなものが得られます。

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)