Types and Abstract Interpretation

This post demonstrates how Dependent Types can be used to implement ‘Types as (Abstract) Interpretations’. The full code can be found on GIST.

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.

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))

Interpretation

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"