Logic.Implicit

Documentation

class Fact p

A Fact p is an implicit proof of p, propagated by Haskell's constraint solver. Facts can be used to implicitly introduce or propagate proofs. However, there is a small run-time cost associated with using Facts: typeclass dictionaries for Facts are still passed around. In many cases they will be optimized away, but this is not guaranteed.

known :: Fact p => Proof p

Recall a known Fact from the implicit context.

note :: forall p t. Proof p -> (Fact p => t) -> t

Add a proof to the implicit context.

on :: Fact (p n) => (Proof (p n) -> Proof q) -> (a ~~ n) -> Proof q

Apply an implication to a predicate in the implicit context. The (a ~~ n) parameter is not actually used; it's type is used to help select a specific fact from the context.

@ -- A safe head function, using an implicitly-passed safety proof. head :: Fact (IsCons xs) => ([a] ~~ xs) -> a head xs = Prelude.head (the xs)

• - Reverse, and a lemma. reverse :: ([a] ~~ xs) -> ([a] ~~ Reverse xs) revConsLemma :: Proof (IsCons xs) -> Proof (IsCons (Reverse xs))
• - Implement a safe last function. last :: Fact (IsCons xs) => ([a] ~~ xs) -> a last xs = note (revConsLemma on xs) $ head (reverse xs)