aboutsummaryrefslogtreecommitdiff log msg author committer range

# `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 limited to type variables, product types `(a, b)`, sum types `Either a b` and function types `a -> b`.

Output terms are built using lambda abstraction, function application, `let` and `case` expressions, 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
```

muri currently doesn't have a build system, so you'll have to compile it yourself, or run it with `runhaskell` or similar.

## 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 -> b'
Impossible.
```