Create a gist now

Instantly share code, notes, and snippets.

Contrived user history example to show off dependent types
module main
I assume you're coming here from
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 ->
-- 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
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
lteShift : LTE (plus n (S k)) m -> LTE (plus (S n) k) m
lteShift p = ?lteShiftL
---------- Proofs ----------
main.recommendPrf = proof
rewrite (plusSuccRightSucc r o)
mrefine lteSucc
main.redeemPrf = proof
rewrite plusSuccRightSucc r o
main.lteShiftL = proof
rewrite sym (plusSuccRightSucc n k)
main.plusK = proof
rewrite (plusSuccRightSucc n k)
mrefine lteSucc

esmooov ( from #idris on freenode was kind enough to show me how to use rewrite on line 64

japgolly commented May 4, 2014

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment