4 ms·

Is it possible with Idris to programmatically create the `decideValidity` function? Conceptually it seems trivial to do, I could imagine building it with meta

by munro 12y ago

Is it possible with Idris to programmatically create the `decideValidity` function? Conceptually it seems trivial to do, I could imagine building it with meta programming. My crazy pseudo code-- :D decideValidity : (p : Proof) -> a -> Either (p a) (Not (p a))

pavpanchekha 12y ago
No—there are many properties that cannot be decided. For example, many programs can be proven to halt in finite time. For example, you can imagine a way to prove that the program return 0 always halts. However, testing for this property is impossible (Halting Problem). More generally, it is not possible to test a general predicate for satisfaction. Even things that are decidable in principle may not be decidable quickly (SAT). On the other hand, there is a lot of space for simple predicates like "str.length < 10" to be decided automatically, since the proofs for these can be constructed with only forward search.
- munro 12y ago
  Wouldn't the proposed function then just not compile for the instances were it would be impossible to test, as desired? It would still be useful for where it does work, like in the code you provided. Seems like a lack of meta programming to me if it's not currently possible.
  - tel 12y ago
    You can sort of do this sometimes. Consider Idris' decidable equality module: https://github.com/idris-lang/Idris-dev/blob/master/libs/prelude/Decidable/Equality.idr https://github.com/idris-lang/Idris-dev/blob/master/libs/pre... Idris has type classes and it produces a polymorphic total function `decEq` for any type which instantiates the class DecEq. decEq :: DecEq t => (x : t) -> y -> Dec (x = y) where Dec denotes a decidable type, something like (but not actually) data Dec t where Yes : t -> Dec t No : Not t -> Dec t So now we have a proposition in our type-level prolog called `DecEq` and some types, the ones with decidable equality, can instantiate it instance DecEq () where decEq _ _ = Yes refl -- Equality is symmetric, so is the negation of equality total negEqSym : {a : t} -> {b : t} -> (a = b -> _|_) -> (b = a -> _|_) negEqSym p h = p (sym h) -- Proof that zero isn't equal to any number greater than zero total OnotS : Z = S n -> _|_ OnotS refl impossible instance DecEq Nat where decEq Z Z = Yes refl decEq Z (S _) = No OnotS decEq (S _) Z = No (negEqSym OnotS) -- recurse on the arguments together and modify the eventual -- decided proof so as to match the arguments actually passed. -- -- I.e. we might find that Yes (n = m) but we need Yes (S n = S m) -- decEq (S n) (S m) with (decEq n m) | Yes p = Yes $ cong p | No p = No $ \h : (S n = S m) => p $ succInjective n m h Finally, at compile time Idris will try to infer the concrete types instantiating variables throughout the program. If any of the variables are bounded by `DecEq` then it must be able to solve the typeclass prolog to establish decidable equality for that type. If it fails to fulfill that obligation then it'll fail at compile time. -- this fails since functions on naturals are -- far, far, far from decidable... Idris cannot achieve the -- obligation to find `DecEq (Nat -> Nat)`. decEq : (x : Nat -> Nat) -> y -> Dec (x = y)
tel 12y ago
It'd be more like decideValidity : (p : A -> Type) -> (a : A) -> Either (p a) (Not (p a)) and for some classes of propositions this is a really useful type, e.g. the notion of decidable equality[0]. For general propositions you're talking about unbounded proof search, however. Undecidable propositions will fail to terminate (thus causing problems in a total language). Decidable propositions may still be exponentially slow to decide. Some classes of propositions may be known to be decidable, but knowing generally whether or not a proposition is undecidable is undecidable (Halting). [0] https://github.com/agda/agda-stdlib/blob/master/src/Relation/Nullary/Core.agda https://github.com/agda/agda-stdlib/blob/master/src/Relation...

by munro 12y ago

pavpanchekha 12y ago

No—there are many properties that cannot be decided. For example, many programs can be proven to halt in finite time. For example, you can imagine a way to prove that the program return 0 always halts. However, testing for this property is impossible (Halting Problem). More generally, it is not possible to test a general predicate for satisfaction. Even things that are decidable in principle may not be decidable quickly (SAT). On the other hand, there is a lot of space for simple predicates like "str.length < 10" to be decided automatically, since the proofs for these can be constructed with only forward search.

munro 12y ago
Wouldn't the proposed function then just not compile for the instances were it would be impossible to test, as desired? It would still be useful for where it does work, like in the code you provided. Seems like a lack of meta programming to me if it's not currently possible.
- tel 12y ago
  You can sort of do this sometimes. Consider Idris' decidable equality module: https://github.com/idris-lang/Idris-dev/blob/master/libs/prelude/Decidable/Equality.idr https://github.com/idris-lang/Idris-dev/blob/master/libs/pre... Idris has type classes and it produces a polymorphic total function `decEq` for any type which instantiates the class DecEq. decEq :: DecEq t => (x : t) -> y -> Dec (x = y) where Dec denotes a decidable type, something like (but not actually) data Dec t where Yes : t -> Dec t No : Not t -> Dec t So now we have a proposition in our type-level prolog called `DecEq` and some types, the ones with decidable equality, can instantiate it instance DecEq () where decEq _ _ = Yes refl -- Equality is symmetric, so is the negation of equality total negEqSym : {a : t} -> {b : t} -> (a = b -> _|_) -> (b = a -> _|_) negEqSym p h = p (sym h) -- Proof that zero isn't equal to any number greater than zero total OnotS : Z = S n -> _|_ OnotS refl impossible instance DecEq Nat where decEq Z Z = Yes refl decEq Z (S _) = No OnotS decEq (S _) Z = No (negEqSym OnotS) -- recurse on the arguments together and modify the eventual -- decided proof so as to match the arguments actually passed. -- -- I.e. we might find that Yes (n = m) but we need Yes (S n = S m) -- decEq (S n) (S m) with (decEq n m) | Yes p = Yes $ cong p | No p = No $ \h : (S n = S m) => p $ succInjective n m h Finally, at compile time Idris will try to infer the concrete types instantiating variables throughout the program. If any of the variables are bounded by `DecEq` then it must be able to solve the typeclass prolog to establish decidable equality for that type. If it fails to fulfill that obligation then it'll fail at compile time. -- this fails since functions on naturals are -- far, far, far from decidable... Idris cannot achieve the -- obligation to find `DecEq (Nat -> Nat)`. decEq : (x : Nat -> Nat) -> y -> Dec (x = y)

tel 12y ago

It'd be more like decideValidity : (p : A -> Type) -> (a : A) -> Either (p a) (Not (p a)) and for some classes of propositions this is a really useful type, e.g. the notion of decidable equality[0]. For general propositions you're talking about unbounded proof search, however. Undecidable propositions will fail to terminate (thus causing problems in a total language). Decidable propositions may still be exponentially slow to decide. Some classes of propositions may be known to be decidable, but knowing generally whether or not a proposition is undecidable is undecidable (Halting). [0] https://github.com/agda/agda-stdlib/blob/master/src/Relation/Nullary/Core.agda https://github.com/agda/agda-stdlib/blob/master/src/Relation...