I have the following code:
doSomething : (s : String) -> (not (s == "") = True) -> String
doSomething s = ?doSomething
validate : String -> String
validate s = case (not (s == "")) of
False => s
True => doSomething s
After checking the input is not empty I would like to pass it to a function which accepts only validated input (not empty Strings).
As far as I understand the validation is taking place during runtime but the types are calculated during compile time - thats way it doesn't work. Is there any workaround?
Also while playing with the code I noticed:
:t (("la" == "") == True)
"la" == "" == True : Bool
But
:t (("la" == "") = True)
"la" == "" = True : Type
Why the types are different?
This isn't about runtime vs. compile-time, since you are writing two branches in validate that take care, statically, of both the empty and the non-empty input cases; at runtime you merely choose between the two.
Your problem is Boolean blindness: if you have a value of type Bool, it is just that, a single bit that could have gone either way. This is what == gives you.
= on the other hand is for propositional equality: the only constructor of the type(-as-proposition) a = b is Refl : a = a, so by pattern-matching on a value of type a = b, you learn that a and b are truly equal.
I was able to get your example working by passing the non-equality as a proposition to doSomething:
doSomething : (s : String) -> Not (s = "") -> String
doSomething "" wtf = void $ wtf Refl
doSomething s nonEmpty = ?doSomething
validate : String -> String
validate "" = ""
validate s = doSomething s nonEmpty
where
nonEmpty : Not (s = "")
nonEmpty Refl impossible