Proving properties of type-level natural numbers obtained from user input

[Ranjit Jhala]

Dear Alexander,

FWIW, this sort of thing is quite straightforward with LiquidHaskell:

http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1418064183.hs

or, the code below:

-----

{-@ LIQUID "--no-termination" @-}

module Nat255 where

-- | Define a predicate for valid integers

{-@ predicate IsValid X = 0 <= X && X < 255 @-}

-- | Use the predicate to define a refinement type (subset) of valid
integers

{-@ type Valid = {v:Int | IsValid v}        @-}

-- | A function that checks whether a given Int is indeed valid

{-@ isValid   :: n:Int -> {v:Bool | Prop v <=> IsValid n} @-}
isValid n     = 0 <= n && n < (255 :: Int)

-- | A function that can only be called with Valid Ints.

{-@ workWithValidNumber :: Valid -> IO () @-}
workWithValidNumber n = putStrLn $ "This is a valid number" ++ show (n ::
Int)

-- | This is fine...
ok    = workWithValidNumber 12

-- | ... But this is not.
notOk = workWithValidNumber 257

-- | Finally the top level loop that inputs a number, tests it
--   and calls `workWithValidNumber` if the number is valid.

loop = do putStrLn "Enter Number between 0 and 255"
          n <- readLn :: IO Int
          if isValid n
             then workWithValidNumber n
             else putStrLn "Humph, bad input, try again!" >> loop

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20141208/d1570dcf/attachment.html>