Example of dependent types and "proof-carrying code" in a simple, practical programming task.

TaxExample.idr

module TaxExample

import Data.So

-- Can't use `total` as a variable name! Boo :(
%default total


-- NOTE: Weird things happen when you use the same name in both a record
-- parameter and a record field name. Don't do it.


namespace ValidTotal
  public export
  record ValidTotal where
    constructor MkValidTotal
    value : Double
    0 prfValid : So (value >= 0.0)

  export
  fromDouble : (value : Double) -> {auto 0 prf : So (value >= 0.0)} -> ValidTotal
  fromDouble value = MkValidTotal value prf

  export
  parseTotal : (value : Double) -> Maybe ValidTotal
  parseTotal value =
    case choose (value >= 0.0) of
      Left _ => Just $ fromDouble value
      Right _ => Nothing


namespace ValidRate
  public export
  record ValidRate where
    constructor MkValidRate
    value : Double
    0 prfValid : So (value >= 0.0)

  export
  fromDouble : (value : Double) -> {auto 0 prf : So (value >= 0.0)} -> ValidRate
  fromDouble value = MkValidRate value prf

  export
  parseRate : (value : Double) -> Maybe ValidRate
  parseRate value =
    case choose (value >= 0.0) of
      Left _ => Just $ fromDouble value
      Right _ => Nothing


||| Tax calculation result.
-- Just a Double for now, but could itself be dependently-typed, e.g. asserting
-- that it is non-negative.
TaxResult : Type
TaxResult = Double


||| Calculate total with tax, with type-level enforcement of correct inputs.
calcTaxSafe : ValidRate -> ValidTotal -> TaxResult
calcTaxSafe rate qty = rate.value * qty.value


||| Calculate total with tax, with parsing of inputs.
calcTax : (rate : Double) -> (qty : Double) -> Maybe TaxResult
calcTax rate qty = do
  rate' <- parseRate rate
  qty' <- parseTotal qty
  Just $ calcTaxSafe rate' qty'