Generating run time proofs with type predicates in Idris

decidable, idris, parsing, unification

Solution

The error message is correct: you provided a value of type `Type`, but you need a value of type `p '0'`. You are also correct that `p` is of type `Char -> Type`, and therefore that `p '0'` is of type `Type`. However, `p '0'` is not of type `p '0'`.

Perhaps the issue would be easier to see with simpler types: `3` has type `Int`, and `Int` has type `Type`, but `Int` does not have type `Int`.

Now, how do we fix the problem? Well, `p` is a predicate, meaning that it constructs types whose inhabitants are proofs of this predicate. So the value of type `p '0'` we need to provide would be a proof, in this case a proof that `'0'` is a digit. `Zero` happens to be such a proof. But in the signature of `every`, the `p` variable isn't talking about digits: it's an abstract predicate, about which we know nothing. For this reason, there are no values we could use instead of `p '0'`. We must instead change the type of `every`.

One possibility would be to write a more specialized version version of `every`, one which would only work for the particular predicate `Digit` instead of working for an arbitrary `p`:

everyDigit : (xs : List Char) -> Maybe $ Every Digit xs
everyDigit [] = Just []
everyDigit (x :: xs) with (decEq x '0')
  everyDigit ('0' :: xs) | (Yes Refl)  = Just $ Zero :: !(everyDigit xs)
  everyDigit (x   :: xs) | (No contra) = Nothing

Instead of incorrectly using the value `p '0'` in a spot which needs a value of type `p '0'`, I have used the value `Zero` in a spot which now needs a value of type `Digit '0'`.

Another possibility would be to modify `every` so that in addition to the predicate `p` which gives a proof type for every `Char`, we would also receive a proof-making function `mkPrf` which would give the corresponding proof value for every `Char`, when possible.

every : (p : Char -> Type)
     -> (mkPrf : (c : Char) -> Maybe $ p c)
     -> (xs : List Char)
     -> Maybe $ Every p xs
every p mkPrf [] = Just []
every p mkPrf (x :: xs) with (mkPrf x)
  every p mkPrf (x :: xs) | Just prf = Just $ prf :: !(every p mkPrf xs)
  every p mkPrf (x :: xs) | Nothing  = Nothing

I am no longer pattern-matching on the `Char`, instead I am asking `mkPrf` to examine the `Char`. I then pattern-match on the result, to see if it found a proof. It is the implementation of `mkPrf` which pattern-matches on the `Char`.

everyDigit' : (xs : List Char) -> Maybe $ Every Digit xs
everyDigit' = every Digit mkPrf
  where
    mkPrf : (c : Char) -> Maybe $ Digit c
    mkPrf '0' = Just Zero
    mkPrf _   = Nothing

In the implementation of `mkPrf`, we are again constructing a proof for the concrete type `Digit '0'` instead of the abstract type `p '0'`, so `Zero` is an acceptable proof.

Problem

I am using this type to reason about strings on which decidable parsing can be performed: ``` data Every : (a -> Type) -> List a -> Type where Nil : {P : a -> Type} -> Every P [] (::) : {P : a -> Type} -> P x -> Every P xs -> Every P (x::xs) ``` For example, defining the digits [0-9] like this: ``` data Digit : Char -> Type where Zero : Digit '0' One : Digit '1' Two : Digit '2' Three : Digit '3' Four : Digit '4' Five : Digit '5' Six : Digit '6' Seven : Digit '7' Eight : Digit '8' Nine : Digit '9' digitToNat : Digit a -> Nat digitToNat Zero = 0 digitToNat One = 1 digitToNat Two = 2 digitToNat Three = 3 digitToNat Four = 4 digitToNat Five = 5 digitToNat Six = 6 digitToNat Seven = 7 digitToNat Eight = 8 digitToNat Nine = 9 ``` then we can have the following functions: ``` fromDigits : Every Digit xs -> Nat -> Nat fromDigits [] k = 0 fromDigits (x :: xs) k = (digitToNat x) * (pow 10 k) + fromDigits xs (k-1) s2n : (s : String) -> {auto p : Every Digit (unpack s)} -> Nat s2n {p} s = fromDigits p (length s - 1) ``` This `s2n` function will now work fine at compile time, but then that isn't very useful in of itself. To use it at runtime we must construct the proof `Every Digit (unpack s)` before we can use the function. So I think I now want to write something like this function: ``` every : (p : a -> Type) -> (xs : List a) -> Maybe $ Every p xs ``` That or we want to return either a proof of membership or a proof of non-membership, but I'm not entirely sure how to do either of these things in a general way. So instead I tried doing the `Maybe` version for just characters: ``` every : (p : Char -> Type) -> (xs : List Char) -> Maybe $ Every p xs every p [] = Just [] every p (x :: xs) with (decEq x '0') every p ('0' :: xs) | (Yes Refl) = Just $ p '0' :: !(every p xs) every p (x :: xs) | (No contra) = Nothing ``` But then I get this unification error: ``` Can't unify Type with p '0' Specifically: Can't unify Type with p '0' ``` But `p` is of type `Char -> Type`. I'm not sure what is causing this unification failure, but think the problem may be related to my previous question. Is this a sensible approach to what I am trying to do? I feel like it is a little to much work at the moment, and more general versions of these functions should be possible. It would be nice if the `auto` keyword could be used to write a function gives you a `Maybe proof` or an `Either proof proofThatItIsNot`, in a similar way to how the `DecEq` class works.

Original source