Portability	non-portable (template-haskell)
Stability	experimental
Maintainer	claudiusmaximus@goto10.org

Language.Haskell.Djinn

Description

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

Synopsis

Documentation

djinn Source

Arguments

:: Q Type	type
-> Q Exp

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

djinns Source

Arguments

:: Q Type	type
-> Q Exp

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

djinnD Source

Arguments

:: String	name
-> Q Type	type
-> Q [Dec]

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"].

djinnsD Source

Arguments

:: String	name
-> Q Type	type
-> Q [Dec]

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"].