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

[Alexander V Vershilov]

Richard, Ranjit,

Thanks for providing your solutions.

--
Alexander.

On 8 December 2014 at 21:45, Ranjit Jhala <jhala at cs.ucsd.edu> wrote:
> 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
>



-- 
Alexander