Last active
August 24, 2016 19:11
-
-
Save jonschoning/ec5eb31bf0668ce34feba937df6ccdd0 to your computer and use it in GitHub Desktop.
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
import Data.String | |
-- takes two integers, and a proof that x < y, and yields an integer | |
add : | |
(x : Integer) -> | |
(y : Integer) -> | |
(prf : x < y = True) -> -- require a proof that that x < y | |
Integer | |
add x y prf = x + y | |
main : IO () | |
main = do | |
sx <- getLine -- read string from input | |
sy <- getLine -- read string from input | |
let Just x = parseInteger sx -- assuming int parse is ok, else error | |
let Just y = parseInteger sy -- assuming int parse is ok, else error | |
case decEq (x < y) True of -- decEq constructs a proof if x < y is True | |
Yes prf => print (add x y prf) | |
No => putStrLn "no prf, x is not less than y" | |
-- lets say I mess up the sign of the comparison on the case line and write decEq (x > y) instead... then I'd get a type error | |
-- When checking argument prf to function Main.add: | |
-- Type mismatch between | |
-- x > y = True (Type of prf) | |
-- and | |
-- x < y = True (Expected type) | |
-- there's no way to construct the prf value artificially, or sneak in different parameters that are unrelated to the prf value. | |
-- it's either a compile error or it's valid. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment