Last active
December 15, 2020 22:27
-
-
Save erdeszt/f592c16112c8a49c412e257c831e2e00 to your computer and use it in GitHub Desktop.
Idris datatype invariant
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Main | |
import Data.String | |
data CorrectSize : Nat -> Nat -> Nat -> Type where | |
SmallerThan150 : (x : Nat) -> (y : Nat) -> (z : Nat) -> {auto prf : x + y + z <= 150 = True} -> CorrectSize x y z | |
Show (CorrectSize x y z) where | |
show (SmallerThan150 x y z) = "CorrectSize " ++ show (x, y, z) | |
showPrec _ size = show size | |
mkCorrectSize : (x : Nat) -> (y : Nat) -> (z : Nat) -> Maybe (CorrectSize x y z) | |
mkCorrectSize x y z = | |
case decEq (x + y + z <= 150) True of | |
Yes prf => Just (SmallerThan150 x y z) | |
No => Nothing | |
main : IO () | |
main = do | |
Just dynX <- map (parsePositive {a=Nat}) getLine | Nothing => idris_crash "X is not a number" | |
Just dynY <- map (parsePositive {a=Nat}) getLine | Nothing => idris_crash "Y is not a number" | |
Just dynZ <- map (parsePositive {a=Nat}) getLine | Nothing => idris_crash "Z is not a number" | |
let static1 = SmallerThan150 120 20 10 -- Ok, value is known at compile time | |
let static2 = SmallerThan150 50 90 10 -- Ok, value is known at compile time | |
let static3 = SmallerThan150 50 50 50 -- Ok, value is known at compile time | |
-- let static4 = SmallerThan150 120 120 10 -- Not ok, doesn't compile, value is known at compile time | |
-- let static5 = SmallerThan150 80 80 50 -- Not ok, doesn't compile value is known at compile time | |
let correctOrNothing = mkCorrectSize dynX dynY dynZ -- Ok if dynamic data is ok, value is checked by smart constructor | |
-- let surelyCorrect = SmallerThan150 dynX dynY dynZ -- Not ok, doesn't compile | |
putStrLn (show correctOrNothing) | |
pure () |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- Alternative version with `So` | |
module Main | |
import Data.String | |
import Data.So | |
data CorrectSize : Nat -> Nat -> Nat -> Type where | |
SmallerThan150 : (x : Nat) -> (y : Nat) -> (z : Nat) -> {auto prf : So (x + y + z <= 150)} -> CorrectSize x y z | |
Show (CorrectSize x y z) where | |
show (SmallerThan150 x y z) = "CorrectSize " ++ show (x, y, z) | |
showPrec _ size = show size | |
mkCorrectSize : (x : Nat) -> (y : Nat) -> (z : Nat) -> Maybe (CorrectSize x y z) | |
mkCorrectSize x y z = | |
case choose (x + y + z <= 150) of | |
Left oh => Just (SmallerThan150 x y z) | |
_ => Nothing | |
main : IO () | |
main = do | |
Just dynX <- map (parsePositive {a=Nat}) getLine | Nothing => idris_crash "X is not a number" | |
Just dynY <- map (parsePositive {a=Nat}) getLine | Nothing => idris_crash "Y is not a number" | |
Just dynZ <- map (parsePositive {a=Nat}) getLine | Nothing => idris_crash "Z is not a number" | |
let static1 = SmallerThan150 120 20 10 -- Ok, value is known at compile time | |
let static2 = SmallerThan150 50 90 10 -- Ok, value is known at compile time | |
let static3 = SmallerThan150 50 50 50 -- Ok, value is known at compile time | |
-- let static4 = SmallerThan150 120 120 10 -- Not ok, doesn't compile, value is known at compile time | |
-- let static5 = SmallerThan150 80 80 50 -- Not ok, doesn't compile value is known at compile time | |
let correctOrNothing = mkCorrectSize dynX dynY dynZ -- Ok if dynamic data is ok, value is checked by smart constructor | |
-- let surelyCorrect = SmallerThan150 dynX dynY dynZ -- Not ok, doesn't compile | |
putStrLn (show correctOrNothing) | |
pure () |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment