# haskell-holes-th: Infer haskell code by given type.

[ language, library, mit ] [ Propose Tags ]

TIP solver for simply typed lambda calculus. Can automatically infer code from type definitions. (TemplateHaskell)

## Modules

[Index] [Quick Jump]

#### Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

Versions [RSS] 0.0.0.1, 1.0.0.0, 2.0.0.0 base (>=4.0 && <5), template-haskell, transformers [details] MIT klntsky klntsky@gmail.com Language https://github.com/klntsky/haskell-holes-th head: git clone git://github.com/klntsky/haskell-holes-th.git by klntsky at 2019-08-24T07:44:26Z 1 direct, 0 indirect [details] 1806 total (4 in the last 30 days) 2.0 (votes: 1) [estimated by Bayesian average] λ λ λ Docs available Last success reported on 2019-08-24

[back to package description]

TIP solver for simply typed lambda calculus + sum & product types that can automatically infer code from type definitions (uses TemplateHaskell). It may also be viewed as a prover for intuitionistic propositional logic.

## Usage

The following code sample shows the usage of the macro.

{-# LANGUAGE TemplateHaskell #-}

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.

## Limitations

• No ADT support

• No type synonym support

• in STLC every typed term is strongly normalizing, so the type of fixed-point combinator can't be inhabited.