Double arithmetic?

[michalrus]

I know it’s deliberately left out, but we have quite a few of these in config files:

, cookieMaxAge = 1209600.0 -- 14 * 24 * 60 * 60

As sometimes sub-second NominalDiffTimes are needed:

instance Dhall.Interpret NominalDiffTime where
  autoWith _ = fromRational . toRational <$> Dhall.double

What would be the best way to go here?

[Gabriella439]

How about adding a Natural/toDouble built-in? Then you could do:

cookieMaxAge = Natural/toDouble (14 * 24 * 60 * 60)

... or Integer/toDouble (since Natural/toInteger exists) or both

[ocharles]

I think just Integer/toDouble (or Double/fromInteger). Natural -> Double can be derived from primitives and be done in Dhall.

…

On Fri, Jun 1, 2018 at 3:29 PM Gabriel Gonzalez ***@***.***> wrote: How about adding a Natural/toDouble built-in? Then you could do: cookieMaxAge = Natural/toDouble (14 * 24 * 60 * 60) ... or Integer/toDouble (since Natural/toInteger exists) or both — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#166 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AABRjtSLxlJR_Zdrh-gYCPKVbGPg4fCGks5t4U_AgaJpZM4UWlbx> .

[Gabriella439]

Yeah, I'm also leaning towards only providing Integer/toDouble to keep the built-ins as orthogonal as possible

[michalrus]

Integer/toDouble would be wonderful! =)

[Gabriella439]

The proposed change to the standard is here: #168

[michalrus]

@Gabriel439 one more thought: this won’t allow Double calculations like 0.1 * 0.5, or this one (for which I have a use case):

{
  partOfInitialX = 0.00333333333333333333 -- = 5 / 1500
}

[Gabriella439]

@michalrus: That's correct. The proposed change still doesn't permit double arithmetic

[michalrus]

Yes, yes, I totally understand that from the diff and this discussion above.

But, now, after going through our Dhall files, I’m thinking that m-m-maaaybe being able to say 5/1500 instead of 0.00333333333333333333 -- = 5 / 1500 could also be seen as desirable. I don’t know. 🤷‍♂️

[michalrus]

I should have read all of the files when posting this issue, sorry. 😿

[Gabriella439]

@michalrus: No worries :)

I think I'll postpone adding Double arithmetic for now because that opens up a whole can of worms (like how Dhall should handle division by 0, for example)

[statusfailed]

I've ended up with another use-case for Double arithmetic- I wanted to have some user-supplied templates that are essentially "fragments" of SVG, and know how to draw themselves at supplied coordinates + dimensions.

Basically, the user-supplied Dhall expression is something like this:

\(dimensions: { x: Double, y: Double, width: Double, height: Double }) -> ''
<rect cx="${Double/show (x + w/4)}"
      cy="${Double/show (y + h/4)"
      width="${Double/show (width/2)}"
      height="${Double/show (height/2)}"
/>
''

Would there be an issue with adding division only for Doubles, and just allowing "Infinity" values when division by zero occurs? I see that division for other types might be a problem (because of exceptions) though.

[FintanH]

@statusfailed What if you made a new data type that represented ratios like { numerator : Natural, denominator : Natural } and then could define division and the likes for that type? I believe @sellout has described something similar to me before too.

[sellout]

@statusfailed I don’t know that it’ll provide what you want, but as @FintanH alluded to, I do have a nascent “dhall-numerics” library I’ve been working on. I can publish it later today, and you can take a look to see what’s there.

[statusfailed]

@FintanH I think I'd still need a function to get the decimal representation for my final output, right? Can this be done within Dhall?

To solve the immediate problem I might just add Double/div in this way

[statusfailed]

@sellout sure, I'll have a look, thanks!

[FintanH]

So the idea would be that you delay the computation until you interpret into your final language, e.g. Haskell, and then it will translate your Ratio into Double. The plus side of this is that you won't have the potential of precision errors until the very last moment :)

[Gabriella439]

@statusfailed: Yeah, I think you will probably want to add built-in Double operators for your use case

@FintanH: My understanding is that implementing the Double conversion logic in Haskell wouldn't work for this use because they want to use the resulting Double to template a string literal within Dhall

[FintanH]

My understanding is that implementing the Double conversion logic in Haskell wouldn't work for this use because they want to use the resulting Double to template a string literal within Dhall

Unless you can delay the show to Haskell as well? 🤔 But maybe I didn't understand the use case properly :)

[statusfailed]

@FintanH @Gabriel439 I threw together a little example of how this can be done here based on the Wiki guide.

Hopefully this helps anyone else who needs to do the same. Thanks everyone for your help!

[Gabriella439]

@statusfailed: Awesome! Thank you 🙂

[f-f]

Probably worth adding to the Wiki guide as a working example?

[statusfailed]

Hmm... seems like I've hit another problem: I'm not able to use (in Haskell-land) functions defined in terms of my newly-added Double arithmetic functions. For example, when I define a dhall file like this:

\(x : Double) -> \(y : Double) -> (Double/add x y)

I get this error in my Haskell program when trying to use it with Dhall.inputWithSettings doubleArithmeticSettings Dhall.auto text:

*** Exception: Interpret: You cannot decode a function if it does not have the correct type

Whereas if I only use "existing" Double functions (like the below Dhall function), everything works:

\(x : Double) -> \(y : Double) -> (Double/show x)

Is there a way I can solve this?

[ocharles]

Can you provide a full example?

[statusfailed]

I've created a full example on the branch example/cannot-decode-function of the double-dhall repo.

There are two Dhall files added. broken.dhall yields the below exception when run with cat broken.dhall | cabal run:

double-dhall: Interpret: You cannot decode a function if it does not have the correct type
CallStack (from HasCallStack):
  error, called at src/Dhall.hs:803:24 in dhall-1.19.1-CXfxNxFUhESEV34XV95wYt:Dhall

And working.dhall prints 1.0 as expected.

FWIW, I am using Nix, so running this with version 1.19.1 of Dhall - not sure if this would make a difference. Let me know if there's anything else I can provide - cheers!

[Gabriella439]

@statusfailed: I'll check this soon. Version 1.19.1 should be new enough since we haven't changed anything related to this since then

[Gabriella439]

@statusfailed: I found the problem. The issue is that the Interpret instance for functions isn't respecting your custom normalization setting:

instance (Inject a, Interpret b) => Interpret (a -> b) where
    autoWith opts = Type extractOut expectedOut
      where
        -- The `Dhall.Core.normalize` is ignoring your customizations
        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

This is why it works on built-in functions but not with your custom additions

I think fixing this properly requires adding a field to InterpretOptions to allow for a custom normalizer

[Gabriella439]

Alright, I have a fix up here: dhall-lang/dhall-haskell#777

I was able to verify it works using the following change to your double-dhall repository:

diff --git a/Main.hs b/Main.hs
index abe5afc..16b6c06 100644
--- a/Main.hs
+++ b/Main.hs
@@ -60,12 +60,15 @@ doubleNormalizer =
 
 main :: IO ()
 main = do
-  text <- Data.Text.IO.getContents
   let context     = doubleEnrichedContext
       normalizer  = ReifiedNormalizer $ pure . doubleNormalizer
       addSettings = Lens.set Dhall.normalizer normalizer
                   . Lens.set Dhall.startingContext context
       inputSettings = addSettings Dhall.defaultInputSettings 
 
-  x <- Dhall.inputWithSettings inputSettings Dhall.auto text
-  Data.Text.IO.putStrLn x
+      interpretOptions =
+          Dhall.defaultInterpretOptions
+              { Dhall.inputNormalizer = normalizer }
+
+  f <- Dhall.inputWithSettings inputSettings (Dhall.autoWith interpretOptions) "Double/add" :: IO (Double -> Double -> Double)
+  print (f 1 2)

[statusfailed]

Beautiful, works perfectly. I updated my branch on double-dhall to include your fix.

Thanks very much!

[Gabriella439]

@statusfailed: You're welcome! Thank you for reporting the issue 🙂