Comunica la funzione dipendente nel ramo dell'istruzione condizionale che la condizione è vera

Question

Ho una funzione con una firma di tipo (x, y : SomeType) -> (cond x y) = True -> SomeType. Quando controllo la condizione in if-then-else/case/with statement, come faccio a passare alla funzione in un ramo corrispondente il fatto, quella condizione è vera?

Answer 1

È possibile utilizzare DecEq per rendere questo facile:

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" 

Ma non si dovrebbe.

L'utilizzo di booleani (tramite = o So) può dirvi che qualcosa è vero, ma non perché. Il perché è molto importante se si desidera comporre prove insieme o spezzarle. Immaginate se add abbia chiamato una funzione che aveva bisogno di x + y < 20 - non possiamo semplicemente superare la nostra prova che x + y < 10 = True perché Idris non sa nulla dell'operazione, solo che è vero.

Invece, dovresti scrivere quanto sopra con un tipo di dati che contiene perché è vero. LTE è un tipo che fa che per i confronti di meno-che:

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" 

Ora, se add chiamato una funzione che aveva bisogno di un LTE (x + y) 20 possiamo scrivere una funzione di ampliare il vincolo:

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

Questo è non qualcosa che possiamo facilmente fare con i soli booleani.