Agda中已知模式匹配

Question

大致上，我有

check : UExpr -> Maybe Expr

And I have a test term

testTerm : UExpr

我希望您能够成功地进行“检查”，并提取生成的“Expr”以进一步操作。基本上，

realTerm : Expr
just realTerm = check testTerm

如果 check testTerm 结果为 nothing，那么这个定义不能通过类型检查。这种情况可能发生吗？

- luqui

---

你可能会发现在类型层面上消除Maybe很有用。 - effectfully

与下面的技术答案相比，我想要指出你的思维是非功能性的。这就像一个想要摆脱IO单子并在Haskell中无处不写命令式代码的人：通常情况下，无法从类型为Maybe的表达式中提取出底层类型；这是强大功能性编程语言（如Agda）的精髓，所以你必须一直传递单子，直到找到一种有效的方法将其编码成另一种类型的值。 - 盛安安

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并且值被推断出来。

- pigworker

---

我刚开始看到这个与True有关的习语，但并没有深入了解。谢谢。 - luqui

Answer 2

我发现一种方法可以做到这一点，有点奇怪和神奇。

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

realTerm : Expr
realTerm = proj₁ testTerm-checks

这让我有点毛骨悚然，但并不一定是坏事。仍然对其他方法感兴趣。

- luqui