muri :: Type -> Maybe Term

muri takes a Haskell type, and generates a Haskell term with that type (or a more general one), if possible.

Equivalently, under the propositions-as-types correspondence, muri is a theorem prover for intuitionistic propositional logic. It takes a proposition as input, and produces a proof of that proposition, if one exists.

Input types are restricted to type variables, the unit type (), product types (a, b), the empty type Void, sum types Either a b and function types a -> b.

Output terms are built using lambda abstraction, function application, let, absurd and case expressions, the empty tuple (), pair construction and the Left and Right type constructors.

muri was inspired by Lennart Augustsson's Djinn, and uses the LJT calculus from "Contraction-Free Sequent Calculi for Intuitionistic Logic" by Roy Dyckhoff to ensure termination.

Usage

muri TYPE

Examples

$ muri 'a -> (b, c) -> (b, (a, c))'
\a -> \(b, c) -> (b, (a, c))

$ muri '(a, b) -> Either a b'
\(a, b) -> Left a

$ muri 'Either (a, c) (b, c) -> (Either a b, c)'
\a -> case a of { Left (b, c) -> (Left b, c); Right (b, c) -> (Right b, c) }

$ muri '(Either (a -> f) a -> f) -> f'
\a -> a (Left (\c -> a (Right c)))

$ muri '(a -> b) -> (Either (a -> f) b -> f) -> f'
\a -> \b -> b (Left (\c -> b (Right (a c))))

$ muri '(Either (a -> f) (b -> f) -> f) -> ((a, b) -> f) -> f'
\a -> \b -> a (Left (\e -> a (Right (\f -> b (e, f)))))

$ muri '((a -> b) -> c) -> ((a, b -> c) -> b) -> c'
\a -> \b -> a (\f -> b (f, \e -> a (\_ -> e)))

$ muri '((((a -> Void) -> Void) -> a) -> a) -> (a -> Void) -> Void'
\a -> \b -> b (a (\d -> absurd (d b)))

$ muri 'a -> b'
Impossible.