Types as Abstract Interpretations.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- --------------------------------------------------------------- [ 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