# haskell-holes-th

[TIP](https://en.wikipedia.org/wiki/Type_inhabitation_problem) solver for [simply typed lambda calculus](https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus) + sum & product types that can automatically infer code from type definitions (uses [TemplateHaskell](https://wiki.haskell.org/Template_Haskell)). It [may also be viewed](https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence) as a prover for intuitionistic propositional logic.

## Usage

The following code sample shows the usage of the macro.

```haskell
{-# LANGUAGE TemplateHaskell #-}

import Language.Haskell.Holes

b :: (b -> c) -> (a -> b) -> (a -> c)
b = $(hole [| b :: (b -> c) -> (a -> b) -> (a -> c) |])

dimap :: (a -> b) -> (c -> d) -> (b -> c) -> (a -> d)
dimap = $(hole [| dimap :: (a -> b) -> (c -> d) -> (b -> c) -> (a -> d) |])

-- Proving that (->) is an instance of Closed
closed :: (a -> b) -> (x -> a) -> (x -> b)
closed = $(hole [| closed :: (a -> b) -> (x -> a) -> (x -> b) |])

-- Proving that (->) is an instance of Strong
first :: (a -> b) -> (a, c) -> (b, c)
first = $(hole [| first :: (a -> b) -> (a, c) -> (b, c) |])

-- Proving that (->) is an instance of Choice
left :: (a -> b) -> Either a c -> Either b c
left = $(hole [| left :: (a -> b) -> Either a c -> Either b c |])
```

During compilation, the following output will be produced (so that you can check the synthesized terms):

```
hole: 'Main.b' := \c f g -> c (f g) :: (b_0 -> c_1) -> (a_2 -> b_0) -> a_2 -> c_1
hole: 'Main.dimap' := \c f i j -> f (i (c j)) :: (a_0 -> b_1) -> (c_2 -> d_3) -> (b_1 -> c_2) -> a_0 -> d_3
hole: 'Main.closed' := \c f g -> c (f g) :: (a_0 -> b_1) -> (x_2 -> a_0) -> x_2 -> b_1
hole: 'Main.first' := \c (e, d) -> (c e, d) :: (a_0 -> b_1) -> (a_0, c_2) -> (b_1, c_2)
hole: 'Main.left' := \c d -> case d of
            Data.Either.Left e -> (\f -> Data.Either.Left (c f)) e
            Data.Either.Right g -> (\h -> Data.Either.Right h) g :: (a_0 -> b_1) ->
Data.Either.Either a_0 c_2 -> Data.Either.Either b_1 c_2
```

Also check out [Test.hs](test/Test.hs).

## Limitations

- No ADT support

- No type synonym support

- in STLC every typed term is strongly normalizing, so the type of [fixed-point combinator](https://en.wikipedia.org/wiki/Fixed-point_combinator) can't be inhabited.

## See also

[djinn](https://github.com/augustss/djinn/) - a program synthesizer with algebraic data and type class support.