Pertanyaan Pencocokan pola yang dikenal di agda


Kira-kira, saya punya

check : UExpr -> Maybe Expr

Dan saya memiliki masa uji

testTerm : UExpr

Yang saya harap akan check berhasil, setelah itu saya ingin mengekstrak hasilnya Expr dan memanipulasinya lebih jauh. Pada dasarnya

realTerm : Expr
just realTerm = check testTerm

Sehingga definisi ini akan gagal untuk typecheck jika check testTerm ternyata nothing. Apakah ini mungkin?


5
2017-09-14 07:02


asal


Jawaban:


Kesepakatan biasa adalah menulis sesuatu seperti itu

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

Jika m menghitung untuk sukses, jenis p adalah Satu dan nilainya disimpulkan.


10
2017-09-14 07:17



Saya menemukan satu cara untuk melakukannya, yang agak aneh dan ajaib.

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

realTerm : Expr
realTerm = proj₁ testTerm-checks

Ini memberi saya kekaguman, tetapi tidak harus dengan cara yang buruk. Masih tertarik dengan cara lain untuk melakukannya.


2
2017-09-14 07:17