Proving properties of type-level natural numbers obtained from user input
Alexander V Vershilov
alexander.vershilov at gmail.com
Fri Dec 19 22:53:16 UTC 2014
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
More information about the Glasgow-haskell-users
mailing list