已知的模式匹配

粗略地說，我有已知的模式匹配

check : UExpr -> Maybe Expr

而且我有一個測試項

testTerm : UExpr

我希望將check成功，之後我想提取得到的Expr和操縱它進一步。基本上

realTerm : Expr 
just realTerm = check testTerm

這樣的，這個定義將無法進行類型檢查，如果check testTerm竟然是nothing。這可能嗎？

來源

2016-09-14 luqui

你可能會發現[消除類型級別的可能]（http://stackoverflow.com/questions/31105947/eliminating-a-maybe-at-the-type-level）有用。 – user3237465

與以下技術答案形成對比的是，我想指出你在考慮非功能性問題。這就像有人希望擺脫'IO' monad並在Haskell中的任何地方寫入命令式代碼：通常，無論如何都無法從類型爲'Maybe'的術語中提取基礎類型;它是Agda等功能強大的編程語言的要點，所以您必須一直傳遞monad，直到找到一種將其編碼爲另一種類型的值爲止。 –

通常的交易是若m計算，以一個成功的寫類似

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 {()}

，p的類型是一個和值推斷。

來源

2016-09-14 07:17:16 pigworker

我剛剛開始看到'True'的成語，但並沒有真正深入。謝謝。 – luqui

那麼我找到了一種方法來做到這一點，這是奇怪的和神奇的。

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

realTerm : Expr 
realTerm = proj₁ testTerm-checks

這給了我heebie jeebies，但不一定是壞的方式。仍然對其他方式感興趣。

來源

2016-09-14 07:17:24 luqui

已知的模式匹配

回答

相關問題