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]

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


[Skip to ReadMe]

Properties

Versions0.0.0.1, 1.0.0.0, 1.0.0.0
Change logNone available
Dependenciesbase (==4.9.*), template-haskell (==2.11.*) [details]
LicenseMIT
Authorklntsky
Maintainerklntsky@gmail.com
CategoryLanguage
Home pagehttps://github.com/8084/haskell-holes-th
Source repositoryhead: git clone git://github.com/8084/haskell-holes-th.git
UploadedSun Dec 10 01:15:04 UTC 2017 by klntsky

Modules

[Index]

Downloads

Maintainers' corner

For package maintainers and hackage trustees


Readme for haskell-holes-th-1.0.0.0

[back to package description]

haskell-holes-th

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

import Language.Haskell.Holes

-- \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

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
Prelude> :m + Language.Haskell.TH
Prelude Language.Haskell.TH> runQ [| _ :: Either (Maybe Int) String |] >>= print
SigE (UnboundVarE _) (AppT (AppT (ConT Data.Either.Either) (AppT (ConT GHC.Base.Maybe) (ConT GHC.Types.Int))) (ConT GHC.Base.String))

The part starting after (UnboundVarE _) is needed.

Notes

Type unification is not implemented, but it may be added in the future.