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 |
This comment has been minimized.
This comment has been minimized.
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 |
This comment has been minimized.
This comment has been minimized.
Can anyone help me out with how exactly the |
This comment has been minimized.
This comment has been minimized.
That's my oversight that I'll leave them there only because they prove the relationships we want to prove, but since I ended up proving |
This comment has been minimized.
esmooov (https://github.com/esmooov) from #idris on freenode was kind enough to show me how to use rewrite on line 64