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)


[Skip to Readme]
Versions [faq] 0.0.0.1, 1.0.0.0, 2.0.0.0
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 Sat Aug 24 07:44:26 UTC 2019
Distributions NixOS:2.0.0.0
Downloads 749 total (57 in the last 30 days)
Rating (no votes yet) [estimated by rule of succession]
Your Rating
  • λ
  • λ
  • λ
Status Hackage Matrix CI
Docs available [build log]
Last success reported on 2019-08-24 [all 1 reports]

Modules

[Index] [Quick Jump]

Downloads

Maintainer's Corner

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

  • 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.