4 ms·
You won't see many examples of "traditional" languages taking advantage of Curry-Howard. Though you can, e.g. an `Admin` class whose constructor checks that the
by armchairhacker 3y ago
You won't see many examples of "traditional" languages taking advantage of Curry-Howard. Though you can, e.g. an `Admin` class whose constructor checks that the credentials are for an admin, and functions like `deleteDatabase` which take an `Admin` instance and don't check for admin credentials because they're already "proven".
loginAdmin(name: &str, password: &str) -> Result<Admin, AuthenticationError>
deleteDatabase(admin: Admin, dbConnection: &DbConnection, dbName: &str) -> Result<(), ConnectionError>
But 2) is correct: these aren't real proofs, because globals and errors can break Curry-Howard, not to mention unsafe coercions.
let evilAdmin: Admin = unsafe { std::mem::transmute([0; size_of<Admin>()]) };
deleteDatabase(evilAdmin, dbConnection, "important_data");
You can't even allow functions which infinitely loop: in theorem-proving languages, every function must be proved terminating. Otherwise you allow:
anything : a
anything = recurse 0
where recurse i = recurse (i + 1)
But in theorem-proving languages, the idea that "this type represents a logical statement, an instance only exists if it's true" is used very often. A classic example is fixed-size vectors
data Nat where
0 : Nat
S : Nat -> Nat -- n + 1, "S"uccessor
data Vec (n : Nat) a where
Nil : forall a, Vec 0 a
Cons : forall n a, a -> Vec n a -> Vec (S n) a
You will see declarations like:
-- Instances of `IsTrue b` only exist if `b = True`
data IsTrue (b : Boolean) where
Trivial : IsTrue True
-- Instances of `Every pred vec` only exist if every element in `vec` satisfies the predicate (so that `pred elem = True`)
data Every (pred : a -> Boolean) (vec: Vec n a) where
Every_nil : forall pred, Every pred Nil -- Every item of an empty vector satisfies an arbitrary predicate
-- Prepending an element which satisfies some predicate to a vector where every element satisfies the same predicate, produces a vector where every element satisfies the same predicate
Every_cons : forall pred x xs, IsTrue (pred x) -> Every pred xs Every pred (Cons x xs)
foosAreFoo : Every (\n -> n == "foo") (Cons "foo" (Cons "foo" (Cons "foo" Nil)))
foosAreFoo = Every_cons Trivial (Every_cons Trivial (Every_cons Trivial Every_nil))
On the other hand, the requirement that all functions must be "logical statements" is essential. Otherwise the programs will crash and the generated proofs will be illogical (and, notice that "crashing program" = "illogical proof"). For example, if one can define the following (impossible to prove) function, one can create programs which crash trying to extract the first element of an empty vector, and proofs which incorrectly assume that all vectors have a first element.
head : Vec n a -> a
head Nil = ???
head (Cons x _) = x
One can define this function though, taking advantage of the fact that there's no such instance `Nil : Vec (S n) a` so only the `Cons` case needs to be matched (which is why this typechecks even though we didn't handle the `Nil` case, while the above example doesn't. Sorry if it's confusing and/or sounds like a cop-out, that's just how it works and real languages accept this kind of pattern matching):
head : Vec (S n) a -> a
head (Cons x _) = x
And, to answer the second point, theorem-proving languages can represent and prove properties of programs with side-effects and even straight-line programs. The former is commonly done using Monads or Algebraic Effects, and the latter using Hoare Logic or another kind of logic
data Var a = String
-- Example IO monad which represents side-effects (stdin, stdout, and variables) through constructors
data IO a where
Pure : a -> IO a
ReadLine : IO String
PrintLine : String -> IO ()
ReadVar : Var a -> IO (Maybe a)
WriteVar : Var a -> Maybe a -> IO a
(>>=) : IO a -> (a -> b) -> IO b
-- "Pure" program which reads first and last name and prints full name.
-- The "interpreter" lazily computes the value of `main` and simultaneously evaluates `IO` actions to get their inner values:
-- When it encounters (x >>= y) it computes `x`, evaluates `x` to get the inner value at runtime,
-- then computes and evaluates `y`
main : IO ()
main =
PrintLine "What is your first name?" >>= \() ->
ReadLine >>= \firstName ->
PrintLine "What is your last name?" >>= \() ->
ReadLine >>= \lastName ->
Pure (firstName ++ " " ++ lastName) >>= \fullName ->
PrintLine ("Hello " ++ fullName ++ "!")
foo : Var Int
foo = Var "Foo"
-- Proving properties of programs is done with Hoare Logic.
-- This is a lot more complicated and full of boilerplate...
data Predicate where
True : Predicate
(!==) : forall a, Var a -> a -> Predicate
(/\) : Predicate -> Predicate -> Predicate
data HoareTriple (pre : Predicate) (stmt : IO ()) (post : Predicate) where
Obvious : forall pre stmt, HoareTriple pre stmt True
Merge : forall pre stmt post1 post2, HoareTriple pre stmt post1 -> HoareTriple pre stmt post2 -> HoareTriple pre stmt (post1 /\ post2)
WeakenL : forall pre1 pre2 stmt post, HoareTriple pre1 stmt post -> HoareTriple (pre1 /\ pre2) stmt post
WeakenR : forall pre1 pre2 stmt post, HoareTriple pre2 stmt post -> HoareTriple (pre1 /\ pre2) stmt post
Specific : forall varN n, HoareTriple (varN !== n) (ReadVar varN >>= \nValue - WriteVar (varN + 1)) (varN !== (n + 1))
example : HoareTriple
(foo !== 4 /\ foo !== 5) -- Precondition
(ReadVar foo >>= \fooValue -> WriteVar (fooValue + 1)) -- Statement
(foo !== 5 /\ foo !== 6) -- Postcondition
example = ... -- Some combination of Merge, WeakenL, WeakenR, and Specific, but I've written enough