haskell - Agda中的已知模式匹配

大概我有

check : UExpr -> Maybe Expr

我有一个测试词

testTerm : UExpr

我希望它能够成功check，之后我要提取生成的Expr并对其进行进一步的处理。基本上

realTerm : Expr
just realTerm = check testTerm

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

最佳答案

通常的做法是写类似

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的类型为1并推断出该值。

关于haskell - Agda中的已知模式匹配，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/39484310/