Implement drop and take builtins #1287
Conversation
|
@Gabriella439 This is ready for a first pass review. I checked the hydra logs and it failed with Which I think means it's running Aside: I feel like the answer to these questions could go in the |
… as standardized in dhall-lang/dhall-lang#1287
There was a problem hiding this comment.
I have a matching PR for the Haskell implementation of Dhall: dhall-lang/dhall-haskell#2430
Also, I'll need you to merge ear7h#1 into your PR
| ```dhall | ||
| List/drop n a ([] : List a) = [] : List a | ||
|
|
||
| List/drop n a (xs # ys) = |
There was a problem hiding this comment.
The goal here is to be more declarative, so I'd suggest something like:
List/drop n a (xs # ys) =
List/drop n a xs # List/drop (Natural/subtract (List/length a xs) n) a ys| ```dhall | ||
| List/take n a ([] : List a) = [] : List a | ||
|
|
||
| List/take n a (xs # ys) = |
There was a problem hiding this comment.
Similarly, here I would suggest:
List/take n a (xs # ys) =
List/take n a xs # List/take (Natural/subtract (List/length a xs) n) a ys| f ⇥ List/drop 0 A₀ as ⇥ [ a, as… ] | ||
| ──────────────────────────────────── | ||
| f as ⇥ [ a, as… ] |
There was a problem hiding this comment.
Even though the previous judgment handles the empty list case, there's no need to explicitly require the list to be non-empty here, or to even be a list:
| f ⇥ List/drop 0 A₀ as ⇥ [ a, as… ] | |
| ──────────────────────────────────── | |
| f as ⇥ [ a, as… ] | |
| f ⇥ List/drop 0 A₀ as₀ ⇥ as₁ | |
| ──────────────────────────────────── | |
| f as₀ ⇥ as₁ |
If you omit the requirement that as₁ is a concrete list then the interpreter can do things like simplify λ(a : Type) → λ(xs : as) → List/drop 0 a xs to λ(a : Type) → λ(xs : as) → xs. In fact, that would be a useful property test to add for List/drop in the Prelude.
| f ⇥ List/drop n A₀ List/drop (n - 1) [ as… ] ⇥ bs | ||
| ─────────────────────────────────────────────────── | ||
| f [ a, as… ] ⇥ bs |
There was a problem hiding this comment.
The argument to f might not necessarily be a list until we β-reduce the list:
| f ⇥ List/drop n A₀ List/drop (n - 1) [ as… ] ⇥ bs | |
| ─────────────────────────────────────────────────── | |
| f [ a, as… ] ⇥ bs | |
| f ⇥ List/drop n A₀ as ⇥ [ a, as… ] List/drop (n - 1) [ as… ] ⇥ bs | |
| ───────────────────────────────────────────────────────────────────── | |
| f as ⇥ bs |
| f as ⇥ [] : A₁ | ||
|
|
||
|
|
||
| f ⇥ List/take 0 A₀ as ⇥ [ a, as… ] |
There was a problem hiding this comment.
Similar comments to List/drop
| ```haskell | ||
| betaNormalize (Application f as) | ||
| | Application | ||
| (Application (Builtin ListDrop) (NaturalLiteral _) |
There was a problem hiding this comment.
There's no need to require the argument to be a concrete Natural literal when the list is empty
| (Application (Builtin ListDrop) (NaturalLiteral _) | |
| (Application (Builtin ListDrop) n |
Per #1286
I can implement this for the Haskell, Rust, and Go implementations (although it might take a while)