-
-
Save ericrasmussen/8173956196158e39c716 to your computer and use it in GitHub Desktop.
module main | |
{- | |
I assume you're coming here from | |
http://chromaticleaves.com/posts/idris-and-dependent-types.html | |
If not, please take a moment to read it. It's a very important white paper. | |
Completely serious, too. | |
Now that we have that out of the way, this gist is a contrived example that | |
shows how you might enforce a relationship in Idris at compile time instead | |
of having to enforce it with runtime checks and error handling. | |
The goal is to make a user history type that tracks user actions and ensures | |
that users cannot redeem more tokens than they've earned. At any given time, | |
you can't construct an instance of the History type without supplying a proof | |
that the number of redeemed tokens is <= the number of earned tokens, so this | |
particular case doesn't need to be tested. | |
-} | |
-- identify users by name only (YOLO) | |
data User = MkUser String | |
-- a data type representing the redemption of a token | |
data Redeem = MkRedeem Int | |
-- users can earn a token by recommending the app to a user | |
data Earn = Recommend User | |
-- user actions are either redeeming tokens or earning them | |
Action : Type | |
Action = Either Redeem Earn | |
-- a history type to keep track of user actions | |
-- the offset will be explained later, but notice how we use | |
-- `LTE (redeemed + offset) earned` in the type signature to show you can't | |
-- make an instance of History unless you can show there are fewer token | |
-- redemptions than recommendations to frineds | |
data History : Type where | |
MkHist : (user : User) -> | |
(redeemed : Nat) -> | |
(offset : Nat) -> | |
(earned : Nat) -> | |
LTE (redeemed + offset) earned -> | |
Vect (redeemed + earned) Action -> | |
History | |
-- we can make an empty history using lteZero, a relationship that says | |
-- 0 is less than or equal to any other natural number | |
emptyHistory : User -> History | |
emptyHistory user = MkHist user 0 0 0 lteZero [] | |
-- when the user recommends the app to a friend, we add it to their history. | |
-- thanks to @esmooov for the rewrite tip! | |
recommendApp : History -> User -> History | |
recommendApp (MkHist u r o e p v) friend = | |
MkHist u r (S o) (S e) ?recommendPrf v' | |
where a : Action | |
a = Right $ Recommend friend | |
v' : Vect (r + (S e)) Action | |
v' = rewrite (sym $ plusSuccRightSucc r e) in a :: v | |
-- if our offset is 0 then we can't redeem a token because all we can say for | |
-- sure is the number of redeemed tokens is <= the number of earned tokens, and | |
-- there's no way to increase the number of redeemed tokens while still proving | |
-- that relationship holds. If the offset is greater than 0, we can show that | |
-- redeemed + (1 + offset) can be rewritten as (redeemed + 1) + offset, without | |
-- changing the value of the lefthand side of redeemed + offset <= earned. | |
redeemToken : History -> Redeem -> Maybe History | |
redeemToken (MkHist _ _ Z _ _ _) _ = Nothing | |
redeemToken (MkHist u r (S o) e p v) token = | |
Just $ MkHist u (S r) o e ?redeemPrf (Left token :: v) | |
-- now we need a way to show that if the left hand side of the relation contains | |
-- the sum of two variables, we can increment one as long as we increment the | |
-- right side | |
total | |
ltePlusK : (k : Nat) -> LTE (n + k) m -> LTE (n + (S k)) (S m) | |
ltePlusK k p = ?plusK | |
-- next we'll have to show that we can rewrite the left side of the relation | |
-- n + (S k) as (S n) + k | |
total | |
lteShift : LTE (plus n (S k)) m -> LTE (plus (S n) k) m | |
lteShift p = ?lteShiftL | |
---------- Proofs ---------- | |
main.recommendPrf = proof | |
intros | |
rewrite (plusSuccRightSucc r o) | |
mrefine lteSucc | |
trivial | |
main.redeemPrf = proof | |
compute | |
intro | |
intro | |
intro | |
intro | |
rewrite plusSuccRightSucc r o | |
intros | |
trivial | |
main.lteShiftL = proof | |
intros | |
rewrite sym (plusSuccRightSucc n k) | |
trivial | |
main.plusK = proof | |
compute | |
intros | |
rewrite (plusSuccRightSucc n k) | |
mrefine lteSucc | |
trivial |
It might do to mention that LTE = "less than or equal to". I didn't realise it was an Idris thing and it took a while to click 😄
Can anyone help me out with how exactly the lteShiftL
and plusK
proofs come into play? They're not explicitly referenced anywhere. My guess would be that these were propositions that were needed during the course of proving redeemPrf
and were therefore proved separately in order to be used in redeemPrf
. But I'm really kind of baffled by these proofs as source code - how is one supposed to approach reading that? Is it not intended to be read like normal source code but only in the interactive context with the proof assistant?
That's my oversight that lteShiftL
and plusK
are still there. I added them initially to show what needed to be proved as part of redeemPrf
, but I ran into an issue where if I actually used them in redeemPrf
it'd work interactively and not typecheck.
I'll leave them there only because they prove the relationships we want to prove, but since I ended up proving redeemPrf
without them, you could remove them and everything would still work.
esmooov (https://github.com/esmooov) from #idris on freenode was kind enough to show me how to use rewrite on line 64