Proving properties of type-level natural numbers obtained from user input
Ranjit Jhala
jhala at cs.ucsd.edu
Mon Dec 8 18:45:55 UTC 2014
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>
More information about the Glasgow-haskell-users
mailing list