agda 中的已知模式匹配

Question

大致上，我有

check : UExpr -> Maybe Expr

我有一个测试术语

testTerm : UExpr

我希望 check 成功，之后我想提取结果 Expr 并进一步操作它。基本上

realTerm : Expr
just realTerm = check testTerm

如果 check testTerm 结果是 nothing，则此定义将无法进行类型检查。这可能吗？

Answer 1

通常的做法是这样写

Just : {X : Set} -> Maybe X -> Set
Just (just x) = One -- or whatever you call the fieldless record type
Just nothing = Zero

justify : {X : Set}(m : Maybe X){p : Just m} -> X
justify (just x) = x
justify nothing {()}

如果m计算成功，则p的类型为One，推断出值。

Answer 2

好吧，我找到了一种方法，有点奇怪和神奇。

testTerm-checks : Σ Expr (\e -> check testTerm ≡ just e)
testTerm-checks = _ , refl

realTerm : Expr
realTerm = proj₁ testTerm-checks

这给了我 heebie jeebies，但不一定是坏事。仍然对其他方法感兴趣。

agda 中的已知模式匹配

Known pattern match in agda

haskell

agda