Infer haskell code by given type.

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

haskell-holes-th

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 #-}

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.

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.

See also

djinn - a program synthesizer with algebraic data and type class support.