dhall-lang / dhall-haskell

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

implement shortcut for more data types in Natural/fold #2596

Closed winitzki closed 2 weeks ago

winitzki commented 2 weeks ago

This is a continuation of https://github.com/dhall-lang/dhall-haskell/pull/2585

This PR implements a shortcut for Natural/fold for more data types. When the accumulator stops changing, Natural/fold should return immediately.

First test: (This involves an accumulator of type Natural, which is already supported after the previous PR.)

let f : Natural → Natural = λ(x : Natural) → if Natural/isZero x then 1 else x
  in assert : 1 === Natural/fold 10000000000 Natural f 0

Second test shows a plausible use case: an integer division algorithm. Division proceeds by repeated subtraction, but we cannot know the required number of subtractions precisely. We know that to divide x / y we need no more than x subtractions.

The accumulator has a more complicated type than just Natural. The implementation now requires us to be able to compare Val a values of more complicated type.

-- unsafeDiv x y means x / y but it will return wrong results when y = 0.
let unsafeDiv : Natural → Natural → Natural =
  let Natural/lessThan = https://prelude.dhall-lang.org/Natural/lessThan
  let Accum = { result : Natural, sub : Natural, done : Bool }  -- Accumulator has this type.
  in λ(x : Natural) → λ(y : Natural) →
         let init : Accum = {result = 0, sub = x, done = False}
         let update : Accum → Accum = λ(acc : Accum) →
             if acc.done then acc
             else if Natural/lessThan acc.sub y then acc // {done = True}
             else acc // {result = acc.result + 1, sub = Natural/subtract y acc.sub}
         let r : Accum = Natural/fold x Accum update init
         in r.result
let x = 10000000000000000000
in  assert : unsafeDiv (3 * x) x === 3

Please let me know how I can improve this Haskell code. I am new to Haskell.

What I did:

What I would like to do in addition to that:

winitzki commented 2 weeks ago
/nix/store/l8j77jfvndani23bkp7kax82lsl4lh0c-binutils-2.35.2/bin/ranlib: dist/build/libHSdhall-1.42.1-C7GxurjhXWDFTD1LA7zHwI
-ghc8.10.7.a: No space left on device
Gabriella439 commented 2 weeks ago

I found one of the contributing factors to the disk issue: https://github.com/dhall-lang/dhall-lang/pull/1380