Cho biết chức năng phụ thuộc trong nhánh lệnh điều kiện có điều kiện là đúng

Question

Tôi có chức năng có chữ ký loại (x, y : SomeType) -> (cond x y) = True -> SomeType. Khi tôi kiểm tra điều kiện trong câu lệnh if-then-else/case/with, làm thế nào để chuyển cho hàm trong một nhánh tương ứng thực tế, điều kiện đó là đúng?

Answer 1

Bạn có thể sử dụng DecEq để làm điều này dễ dàng:

add : (x, y : Nat) -> x + y < 10 = True -> Nat 
add x y _ = x + y 

main : IO() 
main = 
    let x = S Z 
    in let y = Z 
    in case decEq (x + y < 10) True of 
      Yes prf => print (add x y prf) 
      No _ => putStrLn "x + y is not less than 10" 

Nhưng bạn không nên.

Sử dụng booleans (qua = hoặc So) có thể cho bạn biết rằng điều gì đó là đúng, nhưng không phải là lý do tại sao. lý do tại sao là rất quan trọng nếu bạn muốn kết hợp các bản in lại với nhau hoặc tách chúng ra. Hãy tưởng tượng nếu add được gọi là một chức năng cần thiết x + y < 20 - chúng tôi không thể vượt qua bằng chứng của chúng tôi rằng x + y < 10 = True vì Idris không biết gì về hoạt động, chỉ cần đó là sự thật.

Thay vào đó, bạn nên viết ở trên với loại dữ liệu có chứa lý do tại sao đó là sự thật. LTE là một loại mà làm thế để so sánh ít hơn:

add : (x, y : Nat) -> LTE (x + y) 10 -> Nat 
add x y _ = x + y 

main : IO() 
main = 
    let x = S Z 
    in let y = Z 
    in case isLTE (x + y) 10 of 
      Yes prf => print (add x y prf) 
      No _ => putStrLn "x + y is not less than 10" 

Bây giờ, nếu add gọi là chức năng mà cần một người LTE (x + y) 20 chúng ta có thể viết một hàm để mở rộng các hạn chế:

widen : a `LTE` b -> (c : Nat) -> a `LTE` (b + c) 
widen LTEZero c = LTEZero 
widen (LTESucc x) c = LTESucc (widen x c) 

Đây là không phải cái gì chúng ta có thể dễ dàng làm với booleans.