Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Merged
merged 3 commits into from
Jun 16, 2024

Conversation

winitzki
Copy link
Collaborator

@winitzki winitzki commented Jun 12, 2024

This is a continuation of #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:

  • implement valEq to compare two Val a values in case we can easily compare them (natural literals, record literals, Some(), etc.)
  • do a shortcut for Natural/fold: return immediately when the accumulator stops changing

What I would like to do in addition to that:

  • figure out how to make this code more elegant by deriving some typeclass instances
  • figure out how to compare more subtypes of Val

@winitzki
Copy link
Collaborator Author

winitzki commented Jun 12, 2024

/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
Copy link
Collaborator

I found one of the contributing factors to the disk issue: dhall-lang/dhall-lang#1380

@Gabriella439 Gabriella439 merged commit e615993 into main Jun 16, 2024
7 checks passed
@Gabriella439 Gabriella439 deleted the feature/shortcut-natural-fold branch June 16, 2024 21:44
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants