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.
The error message is correct: you provided a value of type
Type
, but you need a value of typep '0'
. You are also correct thatp
is of typeChar -> Type
, and therefore thatp '0'
is of typeType
. However,p '0'
is not of typep '0'
.Perhaps the issue would be easier to see with simpler types:
3
has typeInt
, andInt
has typeType
, butInt
does not have typeInt
.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 typep '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 ofevery
, thep
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 ofp '0'
. We must instead change the type ofevery
.One possibility would be to write a more specialized version version of
every
, one which would only work for the particular predicateDigit
instead of working for an arbitraryp
:Instead of incorrectly using the value
p '0'
in a spot which needs a value of typep '0'
, I have used the valueZero
in a spot which now needs a value of typeDigit '0'
.Another possibility would be to modify
every
so that in addition to the predicatep
which gives a proof type for everyChar
, we would also receive a proof-making functionmkPrf
which would give the corresponding proof value for everyChar
, when possible.I am no longer pattern-matching on the
Char
, instead I am askingmkPrf
to examine theChar
. I then pattern-match on the result, to see if it found a proof. It is the implementation ofmkPrf
which pattern-matches on theChar
.In the implementation of
mkPrf
, we are again constructing a proof for the concrete typeDigit '0'
instead of the abstract typep '0'
, soZero
is an acceptable proof.