[ language, library, mit ] [ Propose Tags ]

TIP solver for simply typed lambda calculus to automatically infer the code from type definitions using TemplateHaskell.

Versions [faq] 0.0.0.1, 1.0.0.0 base (==4.9.*), template-haskell (==2.11.*) [details] MIT klntsky klntsky@gmail.com Language https://github.com/8084/haskell-holes-th head: git clone git://github.com/8084/haskell-holes-th.git by klntsky at Sun Dec 10 01:16:07 UTC 2017 NixOS:1.0.0.0 450 total (34 in the last 30 days) (no votes yet) [estimated by rule of succession] λ λ λ Docs available Last success reported on 2017-12-10

## Modules

[Index]

#### Maintainer's Corner

For package maintainers and hackage trustees

[back to package description]

TIP solver for simply typed lambda calculus to automatically infer the code from type definitions using TemplateHaskell. It may also be viewed as a prover for intuitionistic propositional logic with only implication allowed.

## Usage

The following example shows the basic usage of the macro.

{-# LANGUAGE TemplateHaskell #-}

-- \x -> x
i :: a -> a
i = $(hole [| I :: a -> a |]) -- \x y -> x y y w :: (a -> a -> b) -> a -> b w =$(hole [| W :: (a -> a -> b) -> a -> b |])

-- \x y z -> x (y z)
b :: (b -> c) -> (a -> b) -> (a -> c)
b = $(hole [| B :: (b -> c) -> (a -> b) -> (a -> c) |]) -- \x y z -> x z y c :: (a -> b -> c) -> (b -> a -> c) c =$(hole [| C :: (a -> b -> c) -> (b -> a -> c) |])


Also check out Test.hs.

## Limitations

• Only atomic types from the given context can be inferred. Use holeWith instead of hole to specify a non-default context. The default one contains Bool, Char, Double, Float, Int, Integer, Word and String.

• Haskell's type system is more rich than simply typed lambda calculus (it allows polymorphism), so some of the types that have corresponding definitions in Haskell can't be inferred. Also, in STLC every typed term is strongly normalizing, so the type of fixed-point combinator can't be inhabited.

## Custom context

Any atomic type can be added to the context by constructing a quoted expression of that type and a type itself (as an Exp from TemplateHaskell).

t3 :: Maybe Int
t3 = $(holeWith -- context = [Just 0 :: Maybe Int] [([| Just 0 |], AppT (ConT ''Maybe) (ConT ''Int))] [| mi :: Maybe Int |])  If the type do not correspond to the quoted value, the code containing the inferred term will not compile, but no warnings or errors will be shown if the quoted value is never used. Type definition in terms of Exp can be retrieved from ghci as follows: $ ghci -XTemplateHaskell

The part starting after (UnboundVarE _) is needed.