5 ms·
So the way it works when your data comes from somewhere and you don't know if it is "clean" is that you write a decision procedure to "find out". So the simple
by jonsterling 12y ago
So the way it works when your data comes from somewhere and you don't know if it is "clean" is that you write a decision procedure to "find out".
So the simplest use case is you've got a type like `{x : String | x.length < 10}`: that is, the type of strings which have length less than ten. A value of that type is going to be a pair `<str, proof>` where `proof` is an object which witnesses the fact that `str` has a length less than ten.
Now, it is a decidable property whether or not a string is shorter than 10 chars long. You can easily construct a function with the following type:
decideValidity : (str : string) -> Either (str.length < 10) (Not (str.length < 10))
This function is defined by induction on the string.
Now you want to receive such a string from user input. Crucially, the logic of your program is going to operate on data that's already been validated: so your program will only deal with `{x:String | x.length < 10}`; we just need to shore up the boundaries between your program and user input.
yourComputation :: {x:String | x.length < 10} -> Something
main : IO ()
main = do
userInput <- getLine
case (decideValidity userInput) of
Left prf -> do
print (yourComputation <userInput, prf>)
Right nope ->
print "The input was invalid"
- munro 12y agoIs 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 agoNo—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 agoWouldn'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 agoYou 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 agoIt'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...
- mamcx 12y agoBut then, I don't see what I gain with this. Is like have Eiffel contracts.