Hackage :: [Package]

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

This is a package candidate release! Here you can preview how this package release will appear once published to the main package index (which can be accomplished via the 'maintain' link below). Please note that once a package has been published to the main package index it cannot be undone! Please consult the package uploading documentation for more information.

[maintain] [Publish]

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

[Skip to Readme]

Properties

Versions 0.0.0.1, 1.0.0.0, 2.0.0.0, 2.0.0.0
Change log None available
Dependencies base (>=4.0 && <5), template-haskell, transformers [details]
License MIT
Author klntsky
Maintainer klntsky@gmail.com
Category Language
Home page https://github.com/klntsky/haskell-holes-th
Source repo head: git clone git://github.com/klntsky/haskell-holes-th.git
Uploaded by klntsky at 2019-08-24T07:43:12Z

Modules

[Index] [Quick Jump]

Downloads

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Readme for haskell-holes-th-2.0.0.0

[back to package description]

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

See also

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