Create a gist now

Instantly share code, notes, and snippets.

@jfdm /Nines.idr
Last active Aug 29, 2015

What would you like to do?
Types as Abstract Interpretations.
-- --------------------------------------------------------------- [ Nines.idr ]
-- Module : Nines.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License : GPL v3
-- see http://choosealicense.com/licenses/gpl-3.0/
-- --------------------------------------------------------------------- [ EOH ]
||| Example of using Dependent Types to implement 'Types as (Abstract)
||| Interpretations'.
|||
||| The concept of abstract interpretation is to model the runtime
||| behaviour (semantics) of a program using an existing formalism
||| whose execution costs are lightweight in comparison to the
||| original program.
|||
||| With dependent types we can encode such abstract interpretations
||| at the type-level to both model and reason on software execution.
|||
||| In this example we show how a 'casting out nines' interpretation
||| of arithmetic can be encoded within the types of an expression
||| language.
|||
||| This example, is taken from Chapter 1.1 of:
|||
||| Neil D. Jones and Flemming Nielson. 1995. Abstract interpretation:
||| a semantics-based tool for program analysis. In Handbook of logic
||| in computer science (vol. 4), S. Abramsky, Dov M. Gabbay, and
||| T. S. E. Maibaum (Eds.). Oxford University Press, Oxford, UK
||| 527-636.
module Nines
%access public
%default partial
||| Sum the digits in a number.
|||
||| probably not the most optimal way of doing it.
sumDigits : Int -> Int
sumDigits i = Foldable.foldr (\x,res => cast x + res) 0 (getDigits i)
where
getDigits : Int -> List String
getDigits i = map cast (unpack (cast i))
||| 'Cast out the Nines'
|||
||| Given a number reduce the number until the sum of its digits is
||| less than nine.
castNine : Int -> Int
castNine x =
if x < 9
then x
else castNine $ sumDigits x
||| Mod9 the Result
|||
||| Given a number find the sum of its digits mod nine.
sumMod9 : Int -> Int
sumMod9 i = mod (sumDigits i) 9
||| The expression language.
|||
||| For each expression the `castNine` value is represented within the
||| type.
data Expr : Int -> Type where
Val : (v : Int) -> Expr (castNine v)
Add : Expr a -> Expr b -> Expr (castNine (a + b))
Sub : Expr a -> Expr b -> Expr (castNine (a - b))
Mul : Expr a -> Expr b -> Expr (castNine (a * b))
||| Do the actual interpretation.
private
doInterp : Expr a -> Int
doInterp (Val x) = x
doInterp (Add x y) = doInterp x + doInterp y
doInterp (Sub x y) = doInterp x - doInterp y
doInterp (Mul x y) = doInterp x * doInterp y
||| Interp the expression and return the result if and only if the
||| sum of the digits in the result modulo nine is equal to the `castNine`
||| interpretation.
|||
||| It would be better if the check could also be brought to the type
||| level, and have some proof that the two values are equal, but that
||| is beyond my ability and experience in formal methods and dependent
||| types.
interp : Expr a -> Either String Int
interp {a} expr =
if sumMod9 (doInterp expr) == a
then Right (doInterp expr)
else Left "Err"
-- --------------------------------------------------------------------- [ EOF ]
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment