Add support for marshaling simple Dhall functions to Haskell functions (#88)
This commit is contained in:
parent
de80063698
commit
fae3232480
|
@ -1,6 +1,6 @@
|
|||
{ mkDerivation, ansi-wl-pprint, base, bytestring, case-insensitive
|
||||
, charset, containers, http-client, http-client-tls, lens
|
||||
, neat-interpolation, optparse-generic, parsers, stdenv
|
||||
, charset, containers, contravariant, http-client, http-client-tls
|
||||
, lens, neat-interpolation, optparse-generic, parsers, stdenv
|
||||
, system-fileio, system-filepath, tasty, tasty-hunit, text
|
||||
, text-format, transformers, trifecta, unordered-containers, vector
|
||||
}:
|
||||
|
@ -12,8 +12,8 @@ mkDerivation {
|
|||
isExecutable = true;
|
||||
libraryHaskellDepends = [
|
||||
ansi-wl-pprint base bytestring case-insensitive charset containers
|
||||
http-client http-client-tls lens neat-interpolation parsers
|
||||
system-fileio system-filepath text text-format transformers
|
||||
contravariant http-client http-client-tls lens neat-interpolation
|
||||
parsers system-fileio system-filepath text text-format transformers
|
||||
trifecta unordered-containers vector
|
||||
];
|
||||
executableHaskellDepends = [ base optparse-generic text trifecta ];
|
||||
|
|
|
@ -94,6 +94,7 @@ Library
|
|||
case-insensitive < 1.3 ,
|
||||
charset < 0.4 ,
|
||||
containers >= 0.5.0.0 && < 0.6 ,
|
||||
contravariant < 1.5 ,
|
||||
http-client >= 0.4.30 && < 0.6 ,
|
||||
http-client-tls >= 0.2.0 && < 0.4 ,
|
||||
lens >= 2.4 && < 4.16,
|
||||
|
|
248
src/Dhall.hs
248
src/Dhall.hs
|
@ -34,6 +34,10 @@ module Dhall
|
|||
, maybe
|
||||
, vector
|
||||
, GenericInterpret(..)
|
||||
|
||||
, Inject(..)
|
||||
, inject
|
||||
|
||||
-- * Miscellaneous
|
||||
, rawInput
|
||||
|
||||
|
@ -46,6 +50,7 @@ module Dhall
|
|||
|
||||
import Control.Applicative (empty, liftA2, (<|>), Alternative)
|
||||
import Control.Exception (Exception)
|
||||
import Data.Functor.Contravariant (Contravariant(..))
|
||||
import Data.Monoid ((<>))
|
||||
import Data.Text.Buildable (Buildable(..))
|
||||
import Data.Text.Lazy (Text)
|
||||
|
@ -298,7 +303,7 @@ detailed =
|
|||
> input :: Type a -> Text -> IO a
|
||||
-}
|
||||
data Type a = Type
|
||||
{ extract :: Expr X X -> Maybe a
|
||||
{ extract :: Expr Src X -> Maybe a
|
||||
-- ^ Extracts Haskell value from the Dhall expression
|
||||
, expected :: Expr Src X
|
||||
-- ^ Dhall type of the Haskell value
|
||||
|
@ -446,6 +451,19 @@ instance Interpret a => Interpret (Maybe a) where
|
|||
instance Interpret a => Interpret (Vector a) where
|
||||
autoWith opts = vector (autoWith opts)
|
||||
|
||||
instance (Inject a, Interpret b) => Interpret (a -> b) where
|
||||
autoWith opts = Type extractOut expectedOut
|
||||
where
|
||||
extractOut e = Just (\i -> case extractIn (Dhall.Core.normalize (App e (embed i))) of
|
||||
Just o -> o
|
||||
Nothing -> error "Interpret: You cannot decode a function if it does not have the correct type" )
|
||||
|
||||
expectedOut = Pi "_" declared expectedIn
|
||||
|
||||
InputType {..} = inject
|
||||
|
||||
Type extractIn expectedIn = autoWith opts
|
||||
|
||||
{-| Use the default options for interpreting a configuration file
|
||||
|
||||
> auto = autoWith defaultInterpretOptions
|
||||
|
@ -604,3 +622,231 @@ instance (Selector s, Interpret a) => GenericInterpret (M1 S s (K1 i a)) where
|
|||
key = fieldModifier (Data.Text.Lazy.pack (selName n))
|
||||
|
||||
Type extract' expected' = autoWith opts
|
||||
|
||||
{-| An @(InputType a)@ represents a way to marshal a value of type @\'a\'@ from
|
||||
Haskell into Dhall
|
||||
-}
|
||||
data InputType a = InputType
|
||||
{ embed :: a -> Expr Src X
|
||||
-- ^ Embeds a Haskell value as a Dhall expression
|
||||
, declared :: Expr Src X
|
||||
-- ^ Dhall type of the Haskell value
|
||||
}
|
||||
|
||||
instance Contravariant InputType where
|
||||
contramap f (InputType embed declared) = InputType embed' declared
|
||||
where
|
||||
embed' x = embed (f x)
|
||||
|
||||
{-| This class is used by `Interpret` instance for functions:
|
||||
|
||||
> instance (Inject a, Interpret b) => Interpret (a -> b)
|
||||
|
||||
You can convert Dhall functions with "simple" inputs (i.e. instances of this
|
||||
class) into Haskell functions. This works by:
|
||||
|
||||
* Marshaling the input to the Haskell function into a Dhall expression (i.e.
|
||||
@x :: Expr Src X@)
|
||||
* Applying the Dhall function (i.e. @f :: Expr Src X@) to the Dhall input
|
||||
(i.e. @App f x@)
|
||||
* Normalizing the syntax tree (i.e. @normalize (App f x)@)
|
||||
* Marshaling the resulting Dhall expression back into a Haskell value
|
||||
-}
|
||||
class Inject a where
|
||||
injectWith :: InterpretOptions -> InputType a
|
||||
default injectWith
|
||||
:: (Generic a, GenericInject (Rep a)) => InterpretOptions -> InputType a
|
||||
injectWith options = contramap GHC.Generics.from (genericInjectWith options)
|
||||
|
||||
{-| Use the default options for injecting a value
|
||||
|
||||
> inject = inject defaultInterpretOptions
|
||||
-}
|
||||
inject :: Inject a => InputType a
|
||||
inject = injectWith defaultInterpretOptions
|
||||
|
||||
instance Inject Bool where
|
||||
injectWith _ = InputType {..}
|
||||
where
|
||||
embed = BoolLit
|
||||
|
||||
declared = Bool
|
||||
|
||||
instance Inject Text where
|
||||
injectWith _ = InputType {..}
|
||||
where
|
||||
embed text = TextLit (Data.Text.Lazy.Builder.fromLazyText text)
|
||||
|
||||
declared = Text
|
||||
|
||||
instance Inject Data.Text.Text where
|
||||
injectWith _ = InputType {..}
|
||||
where
|
||||
embed text = TextLit (Data.Text.Lazy.Builder.fromText text)
|
||||
|
||||
declared = Text
|
||||
|
||||
instance Inject Natural where
|
||||
injectWith _ = InputType {..}
|
||||
where
|
||||
embed = NaturalLit
|
||||
|
||||
declared = Natural
|
||||
|
||||
instance Inject Integer where
|
||||
injectWith _ = InputType {..}
|
||||
where
|
||||
embed = IntegerLit
|
||||
|
||||
declared = Integer
|
||||
|
||||
instance Inject Double where
|
||||
injectWith _ = InputType {..}
|
||||
where
|
||||
embed = DoubleLit
|
||||
|
||||
declared = Double
|
||||
|
||||
instance Inject a => Inject (Maybe a) where
|
||||
injectWith options = InputType embedOut declaredOut
|
||||
where
|
||||
embedOut (Just x) =
|
||||
OptionalLit declaredIn (Data.Vector.singleton (embedIn x))
|
||||
embedOut Nothing =
|
||||
OptionalLit declaredIn Data.Vector.empty
|
||||
|
||||
InputType embedIn declaredIn = injectWith options
|
||||
|
||||
declaredOut = App Optional declaredIn
|
||||
|
||||
instance Inject a => Inject (Vector a) where
|
||||
injectWith options = InputType embedOut declaredOut
|
||||
where
|
||||
embedOut xs = ListLit (Just declaredIn) (fmap embedIn xs)
|
||||
|
||||
declaredOut = App List declaredIn
|
||||
|
||||
InputType embedIn declaredIn = injectWith options
|
||||
|
||||
{-| This is the underlying class that powers the `Interpret` class's support
|
||||
for automatically deriving a generic implementation
|
||||
-}
|
||||
class GenericInject f where
|
||||
genericInjectWith :: InterpretOptions -> InputType (f a)
|
||||
|
||||
instance GenericInject f => GenericInject (M1 D d f) where
|
||||
genericInjectWith = fmap (contramap unM1) genericInjectWith
|
||||
|
||||
instance GenericInject f => GenericInject (M1 C c f) where
|
||||
genericInjectWith = fmap (contramap unM1) genericInjectWith
|
||||
|
||||
instance (Constructor c1, Constructor c2, GenericInject f1, GenericInject f2) => GenericInject (M1 C c1 f1 :+: M1 C c2 f2) where
|
||||
genericInjectWith options@(InterpretOptions {..}) = InputType {..}
|
||||
where
|
||||
embed (L1 (M1 l)) = UnionLit keyL (embedL l) Data.Map.empty
|
||||
embed (R1 (M1 r)) = UnionLit keyR (embedR r) Data.Map.empty
|
||||
|
||||
declared =
|
||||
Union (Data.Map.fromList [(keyL, declaredL), (keyR, declaredR)])
|
||||
|
||||
nL :: M1 i c1 f1 a
|
||||
nL = undefined
|
||||
|
||||
nR :: M1 i c2 f2 a
|
||||
nR = undefined
|
||||
|
||||
keyL = constructorModifier (Data.Text.Lazy.pack (conName nL))
|
||||
keyR = constructorModifier (Data.Text.Lazy.pack (conName nR))
|
||||
|
||||
InputType embedL declaredL = genericInjectWith options
|
||||
InputType embedR declaredR = genericInjectWith options
|
||||
|
||||
instance (Constructor c, GenericInject (f :+: g), GenericInject h) => GenericInject ((f :+: g) :+: M1 C c h) where
|
||||
genericInjectWith options@(InterpretOptions {..}) = InputType {..}
|
||||
where
|
||||
embed (L1 l) = UnionLit keyL valL (Data.Map.insert keyR declaredR ktsL')
|
||||
where
|
||||
UnionLit keyL valL ktsL' = embedL l
|
||||
embed (R1 (M1 r)) = UnionLit keyR (embedR r) ktsL
|
||||
|
||||
nR :: M1 i c h a
|
||||
nR = undefined
|
||||
|
||||
keyR = constructorModifier (Data.Text.Lazy.pack (conName nR))
|
||||
|
||||
declared = Union (Data.Map.insert keyR declaredR ktsL)
|
||||
|
||||
InputType embedL (Union ktsL) = genericInjectWith options
|
||||
InputType embedR declaredR = genericInjectWith options
|
||||
|
||||
instance (Constructor c, GenericInject f, GenericInject (g :+: h)) => GenericInject (M1 C c f :+: (g :+: h)) where
|
||||
genericInjectWith options@(InterpretOptions {..}) = InputType {..}
|
||||
where
|
||||
embed (L1 (M1 l)) = UnionLit keyL (embedL l) ktsR
|
||||
embed (R1 r) = UnionLit keyR valR (Data.Map.insert keyL declaredL ktsR')
|
||||
where
|
||||
UnionLit keyR valR ktsR' = embedR r
|
||||
|
||||
nL :: M1 i c f a
|
||||
nL = undefined
|
||||
|
||||
keyL = constructorModifier (Data.Text.Lazy.pack (conName nL))
|
||||
|
||||
declared = Union (Data.Map.insert keyL declaredL ktsR)
|
||||
|
||||
InputType embedL declaredL = genericInjectWith options
|
||||
InputType embedR (Union ktsR) = genericInjectWith options
|
||||
|
||||
instance (GenericInject (f :+: g), GenericInject (h :+: i)) => GenericInject ((f :+: g) :+: (h :+: i)) where
|
||||
genericInjectWith options = InputType {..}
|
||||
where
|
||||
embed (L1 l) = UnionLit keyL valR (Data.Map.union ktsL' ktsR)
|
||||
where
|
||||
UnionLit keyL valR ktsL' = embedL l
|
||||
embed (R1 r) = UnionLit keyR valR (Data.Map.union ktsL ktsR')
|
||||
where
|
||||
UnionLit keyR valR ktsR' = embedR r
|
||||
|
||||
declared = Union (Data.Map.union ktsL ktsR)
|
||||
|
||||
InputType embedL (Union ktsL) = genericInjectWith options
|
||||
InputType embedR (Union ktsR) = genericInjectWith options
|
||||
|
||||
instance (GenericInject f, GenericInject g) => GenericInject (f :*: g) where
|
||||
genericInjectWith options = InputType embedOut declaredOut
|
||||
where
|
||||
embedOut (l :*: r) = RecordLit (Data.Map.union mapL mapR)
|
||||
where
|
||||
RecordLit mapL = embedInL l
|
||||
RecordLit mapR = embedInR r
|
||||
|
||||
declaredOut = Record (Data.Map.union mapL mapR)
|
||||
where
|
||||
Record mapL = declaredInL
|
||||
Record mapR = declaredInR
|
||||
|
||||
InputType embedInL declaredInL = genericInjectWith options
|
||||
|
||||
InputType embedInR declaredInR = genericInjectWith options
|
||||
|
||||
instance GenericInject U1 where
|
||||
genericInjectWith _ = InputType {..}
|
||||
where
|
||||
embed _ = RecordLit Data.Map.empty
|
||||
|
||||
declared = Record Data.Map.empty
|
||||
|
||||
instance (Selector s, Inject a) => GenericInject (M1 S s (K1 i a)) where
|
||||
genericInjectWith opts@(InterpretOptions {..}) =
|
||||
InputType embedOut declaredOut
|
||||
where
|
||||
n :: M1 i s f a
|
||||
n = undefined
|
||||
|
||||
name = fieldModifier (Data.Text.Lazy.pack (selName n))
|
||||
|
||||
embedOut (M1 (K1 x)) = RecordLit (Data.Map.singleton name (embedIn x))
|
||||
|
||||
declaredOut = Record (Data.Map.singleton name declaredIn)
|
||||
|
||||
InputType embedIn declaredIn = injectWith opts
|
||||
|
|
|
@ -26,6 +26,9 @@ module Dhall.Tutorial (
|
|||
-- * Functions
|
||||
-- $functions
|
||||
|
||||
-- * Compiler
|
||||
-- $compiler
|
||||
|
||||
-- * Strings
|
||||
-- $strings
|
||||
|
||||
|
@ -627,9 +630,56 @@ import Dhall
|
|||
-- functions in Haskell. The only difference is that Dhall requires you to
|
||||
-- annotate the type of the function's input.
|
||||
--
|
||||
-- We can test our @makeBools@ function directly from the command line. This
|
||||
-- library comes with a command-line executable program named @dhall@ that you
|
||||
-- can use to both type-check files and convert them to a normal form. Our
|
||||
-- You can import this function into Haskell, too:
|
||||
--
|
||||
-- >>> makeBools <- input auto "./makeBools" :: IO (Bool -> Vector Bool)
|
||||
-- >>> makeBools True
|
||||
-- [True,False,True,True]
|
||||
--
|
||||
-- The reason this works is that there is an `Interpret` instance for simple
|
||||
-- functions:
|
||||
--
|
||||
-- > instance (Inject a, Interpret b) => Interpret (a -> b)
|
||||
--
|
||||
-- Thanks to currying, this instance works for functions of multiple simple
|
||||
-- arguments:
|
||||
--
|
||||
-- >>> dhallAnd <- input auto "λ(x : Bool) → λ(y : Bool) → x && y" :: IO (Bool -> Bool -> Bool)
|
||||
-- >>> dhallAnd True False
|
||||
-- False
|
||||
--
|
||||
-- However, you can't convert anything more complex than that like a polymorphic
|
||||
-- or higher-order function). You will need to apply those functions to their
|
||||
-- arguments within Dhall before converting their result to a Haskell value.
|
||||
--
|
||||
-- Just like `Interpret`, you can derive `Inject` for user-defined data types:
|
||||
--
|
||||
-- > {-# LANGUAGE DeriveAnyClass #-}
|
||||
-- > {-# LANGUAGE DeriveGeneric #-}
|
||||
-- > {-# LANGUAGE OverloadedStrings #-}
|
||||
-- >
|
||||
-- > module Main where
|
||||
-- >
|
||||
-- > import Dhall
|
||||
-- >
|
||||
-- > data Example0 = Example0 { foo :: Bool, bar :: Bool }
|
||||
-- > deriving (Generic, Inject)
|
||||
-- >
|
||||
-- > main = do
|
||||
-- > f <- input auto "λ(r : { foo : Bool, bar : Bool }) → r.foo && r.bar"
|
||||
-- > print (f (Example0 { foo = True, bar = False }) :: Bool)
|
||||
-- > print (f (Example0 { foo = True, bar = True }) :: Bool)
|
||||
--
|
||||
-- The above program prints:
|
||||
--
|
||||
-- > False
|
||||
-- > True
|
||||
|
||||
-- $compiler
|
||||
--
|
||||
-- We can also test our @makeBools@ function directly from the command line.
|
||||
-- This library comes with a command-line executable program named @dhall@ that
|
||||
-- you can use to both type-check files and convert them to a normal form. Our
|
||||
-- compiler takes a program on standard input and then prints the program's type
|
||||
-- to standard error followed by the program's normal form to standard output:
|
||||
--
|
||||
|
@ -655,9 +705,9 @@ import Dhall
|
|||
--
|
||||
-- > forall x . b -- ... is the same as this Haskell type
|
||||
--
|
||||
-- The part where Dhall differs from Haskell is that you can also use @∀@/@forall@
|
||||
-- to give names to non-@Type@ arguments (such as the first argument to
|
||||
-- @makeBools@).
|
||||
-- The part where Dhall differs from Haskell is that you can also use
|
||||
-- @∀@/@forall@ to give names to non-@Type@ arguments (such as the first
|
||||
-- argument to @makeBools@).
|
||||
--
|
||||
-- The second line of Dhall's output is our program's normal form:
|
||||
--
|
||||
|
|
|
@ -1,14 +1,22 @@
|
|||
{-# LANGUAGE DeriveAnyClass #-}
|
||||
{-# LANGUAGE DeriveGeneric #-}
|
||||
{-# LANGUAGE OverloadedStrings #-}
|
||||
{-# LANGUAGE QuasiQuotes #-}
|
||||
|
||||
module Tutorial where
|
||||
|
||||
import qualified Data.Text.Lazy
|
||||
import qualified Data.Vector
|
||||
import qualified Dhall
|
||||
import qualified NeatInterpolation
|
||||
import qualified Test.Tasty
|
||||
import qualified Test.Tasty.HUnit
|
||||
import qualified Util
|
||||
|
||||
import Dhall (Inject)
|
||||
import GHC.Generics (Generic)
|
||||
import Test.Tasty (TestTree)
|
||||
import Test.Tasty.HUnit ((@?=))
|
||||
|
||||
tutorialTests :: TestTree
|
||||
tutorialTests =
|
||||
|
@ -17,6 +25,11 @@ tutorialTests =
|
|||
[ _Interpolation_0
|
||||
, _Interpolation_1
|
||||
]
|
||||
, Test.Tasty.testGroup "Functions"
|
||||
[ _Functions_0
|
||||
, _Functions_1
|
||||
, _Functions_2
|
||||
]
|
||||
]
|
||||
|
||||
_Interpolation_0 :: TestTree
|
||||
|
@ -29,7 +42,7 @@ in "My name is $${name} and my age is $${Integer/show age}"
|
|||
Util.assertNormalizesTo e "\"My name is John Doe and my age is 21\"" )
|
||||
|
||||
_Interpolation_1 :: TestTree
|
||||
_Interpolation_1 = Test.Tasty.HUnit.testCase "Example #0" (do
|
||||
_Interpolation_1 = Test.Tasty.HUnit.testCase "Example #1" (do
|
||||
e <- Util.code [NeatInterpolation.text|
|
||||
''
|
||||
for file in *; do
|
||||
|
@ -38,3 +51,29 @@ _Interpolation_1 = Test.Tasty.HUnit.testCase "Example #0" (do
|
|||
''
|
||||
|]
|
||||
Util.assertNormalized e )
|
||||
|
||||
_Functions_0 :: TestTree
|
||||
_Functions_0 = Test.Tasty.HUnit.testCase "Example #0" (do
|
||||
let text = Data.Text.Lazy.fromStrict [NeatInterpolation.text|
|
||||
\(n : Bool) ->
|
||||
[ n && True, n && False, n || True, n || False ]
|
||||
|]
|
||||
makeBools <- Dhall.input Dhall.auto text
|
||||
makeBools True @?= Data.Vector.fromList [True,False,True,True] )
|
||||
|
||||
_Functions_1 :: TestTree
|
||||
_Functions_1 = Test.Tasty.HUnit.testCase "Example #1" (do
|
||||
let text = Data.Text.Lazy.fromStrict [NeatInterpolation.text|
|
||||
λ(x : Bool) → λ(y : Bool) → x && y
|
||||
|]
|
||||
makeBools <- Dhall.input Dhall.auto text
|
||||
makeBools True False @?= False )
|
||||
|
||||
data Example0 = Example0 { foo :: Bool, bar :: Bool }
|
||||
deriving (Generic, Inject)
|
||||
|
||||
_Functions_2 :: TestTree
|
||||
_Functions_2 = Test.Tasty.HUnit.testCase "Example #2" (do
|
||||
f <- Dhall.input Dhall.auto "λ(r : { foo : Bool, bar : Bool }) → r.foo && r.bar"
|
||||
f (Example0 { foo = True, bar = False }) @?= False
|
||||
f (Example0 { foo = True, bar = True }) @?= True )
|
||||
|
|
Loading…
Reference in New Issue
Block a user