dhall-lang / dhall-haskell

Maintainable configuration files
https://dhall-lang.org/
BSD 3-Clause "New" or "Revised" License
912 stars 213 forks source link

Failure to Decode Expression with extended Builtin Function #2526

Closed julmue closed 10 months ago

julmue commented 1 year ago

I'm trying to extend the Dhall language with an equality operation and then decode functions using the extended interface to haskell functions. Unfortunately that doesn't work.

For the implementation I follow the section Extending the language of the official tutorial.

naturalEqualType :: Dhall.Expr s a
naturalEqualType = Dhall.Pi Nothing "_" Dhall.Natural (Dhall.Pi Nothing "_" Dhall.Natural Dhall.Bool)

startingContext :: Dhall.Context.Context (Dhall.Expr s a)
startingContext = transform Dhall.Context.empty
  where
    transform :: Dhall.Context.Context (Dhall.Expr s a) -> Dhall.Context.Context (Dhall.Expr s a)
    transform =
      Dhall.Context.insert "Natural/equal" naturalEqualType

normalizer :: Dhall.Expr s1 a1 -> Maybe (Dhall.Expr s2 a2)
normalizer (Dhall.App (Dhall.App (Dhall.Var "Natural/equal") (Dhall.NaturalLit x)) (Dhall.NaturalLit y)) = Just (Dhall.BoolLit (x == y))
normalizer _ = Nothing

inputSettings :: Dhall.InputSettings
inputSettings = transform Dhall.defaultInputSettings
  where
    transform =
        set Dhall.normalizer      (Just (Dhall.ReifiedNormalizer (pure . normalizer)))
      . set Dhall.startingContext startingContext

input :: FromDhall a => Text -> IO a
input = Dhall.inputWithSettings inputSettings Dhall.auto

It works if the function is fully applied within the Dhall expression:

testNaturalEqSource1 :: Text
testNaturalEqSource1 = [NeatInterpolation.text|
let x = Natural/equal 1 1
in x : Bool

testNaturalEq1 :: Bool
testNaturalEq1 = unsafePerformIO $ input testNaturalEqSource1
|]

Executing testNaturalSource1 in ghci returns True as expected.

It fails if I try to decode the function without applying it to arguments:

testNaturalEqSource2 :: Text
testNaturalEqSource2 = [NeatInterpolation.text|
let x : Natural -> Natural -> Bool = \ (n1 : Natural) -> \ (n2 : Natural) -> Natural/equal n1 n2
in x
|]

testNaturalEq2 :: Natural -> Natural -> Bool
testNaturalEq2 = unsafePerformIO $ input testNaturalEqSource2

Running it in ghci results in an error

>>> testNaturalEq2 1 1

 *** Exception: FromDhall: You cannot decode a function if it does not have the correct type
CallStack (from HasCallStack):
  error, called at src/Dhall/Marshal/Decode.hs:1134:23 in dhall-1.41.2-DSv9eZfnsTVGwdH0GPi336:Dhall.Marshal.Decod

Decoding functions works for "real" builtins like Natural/subtract with no problem. Am I missing something?

Many thanks in advance

julmue commented 10 months ago

Works using the functionWith combinator.