Richard, Ranjit, Thanks for providing your solutions.
-- Alexander. On 8 December 2014 at 21:45, Ranjit Jhala <jh...@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 _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users