Portability | non-portable (template-haskell) |
---|---|

Stability | experimental |

Maintainer | claudiusmaximus@goto10.org |

Djinn uses a theorem prover for intuitionistic propositional logic to generate a Haskell expression when given a type. Djinn-TH uses Template Haskell to turn this expression into executable code.

Based mostly on http://hackage.haskell.org/package/djinn.

Using Language.Haskell.Djinn generally requires:

{-# LANGUAGE TemplateHaskell, ScopedTypeVariables #-}

# Documentation

Generate an anonymous expression of the given type (if it is realizable).

Generate a list of anonymous expressions of the given type (if it is realizable).

Generate a named declaration with an accompanying type signature. For example:

$(djinnD "maybeToEither" [t| forall a b . a -> Maybe b -> Either a b |]) main = print . map (maybeToEither "foo") $ [ Nothing, Just "bar" ]

might print `[Left "foo",Right "bar"]`

.

Generate a named declaration with an accompanying type signature for a list of possible realizations of a type.

$(djinnsD "picks" [t| forall a . (a, a) -> (a -> a) -> a |]) main = print [ p ("A","B") (++"C") | p <- picks ]

might print `["BC","AC","B","A"]`

.