đại khái, tôi cóĐược biết đến mô hình phù hợp trong agda
check : UExpr -> Maybe Expr
Và tôi có thời hạn kiểm tra
testTerm : UExpr
Mà tôi hy vọng sẽ check thành công, sau đó tôi muốn trích xuất kết quả Expr và thao tác nó hơn nữa. Về cơ bản
realTerm : Expr
just realTerm = check testTerm
Chẳng hạn định nghĩa này sẽ không đánh máy nếu check testTerm được bật là nothing. Điều này có thể không?
Thỏa thuận thông thường là viết một cái gì đó giống như
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 {()}
Nếu m tính đến một thành công, loại p là One và giá trị được suy ra.
Tôi vừa mới bắt đầu thấy thành ngữ đó với 'True' nhưng không thực sự đào sâu. – luqui
Tôi đã tìm thấy một cách để làm điều đó, đó là loại kỳ quái và kỳ diệu.
testTerm-checks : Σ Expr (\e -> check testTerm ≡ just e)
testTerm-checks = _ , refl
realTerm : Expr
realTerm = proj₁ testTerm-checks
Điều này mang lại cho tôi các jeebies heebie, nhưng không nhất thiết phải theo cách xấu. Vẫn còn quan tâm đến những cách khác để làm điều đó.
Bạn có thể tìm thấy [Loại bỏ một Có thể ở cấp loại] (http://stackoverflow.com/questions/31105947/eliminating-a-maybe-at-the-type-level) hữu ích. – user3237465
Ngược lại với các câu trả lời kỹ thuật dưới đây, tôi muốn chỉ ra rằng bạn đang suy nghĩ không có chức năng. Nó giống như một người muốn loại bỏ bản đơn 'IO' và viết mã bắt buộc ở khắp mọi nơi trong Haskell: nói chung, không có cách nào để trích xuất kiểu cơ bản từ một từ có kiểu' Có thể 'bất cứ điều gì; Đó là ý chính của các ngôn ngữ lập trình chức năng mạnh mẽ như Agda, vì vậy bạn phải vượt qua toàn bộ con đường xung quanh cho đến khi bạn tìm được cách tốt để mã hóa nó thành giá trị của một loại khác. –