JSON/fold example in the README doesn't work
cjsauer opened this issue ยท 5 comments
Hi there ๐
When I attempt to paste the following snippet from the README into the Grace browser:
JSON/fold
{ "bool": \b -> if b then 1 else 0
, "natural": \x -> x
, "integer": Integer/abs
, "real": \_ -> 1
, "string": \_ -> 2
, "null": 3
, "object": List/length
, "array": \vs -> List/fold vs (\x -> \y -> x + y : Natural) 0
}
[ true, 1, [ -2, false, "" ], null, { foo: { } } ]
I get:
Not a subtype
The following type:
List a?
(input):1:1:
โ
1 โ JSON/fold
โ โ
โฆ cannot be a subtype of:
{ cons: b? -> c? -> c?, nil: c? }
(input):9:21:
โ
9 โ , "array": \vs -> List/fold vs (\x -> \y -> x + y : Natural) 0
โ โ
I can't understand how I might fix this given that Grace doesn't support recursion, which seems like it'd be necessary in order to get the result that the README suggests: 10
. In fact I'm having trouble understanding the usefulness of JSON/fold
at all given that recursion isn't supported...
Actually, the issue isn't that Grace doesn't support. Rather the issue is that the type of List/fold
changed to improve its ergonomics. The type used to be:
forall (a : Type) . forall (b : Type) . List a -> (a -> b -> b) -> b -> b
โฆ but now the type is:
forall (a : Type) . forall (b : Type) . { cons: a -> b -> b, nil: b } -> List a -> b
Ah that works now! Thanks for the quick change.
What I was failing to understand was that the JSON/fold
built-in maps the handlers over the array before passing it to the reducing function. For whatever reason I had it in my head that I needed to recurse with the handler manually over the array, which is obviously not possible. The same is true for records, for anyone reading this in the future.
Lines 402 to 409 in 44d4b48
Also, this blog post of mine might help for others who want to improve their intuition of how folds in general work:
https://www.haskellforall.com/2021/02/folds-are-constructor-substitution.html
There is also a useful Dhall-specific guide to recursion that is relevant, too (since Dhall has the same limitations as Grace):
https://docs.dhall-lang.org/howtos/How-to-translate-recursive-code-to-Dhall.html
Very helpful, thank you. So in the JSON/fold
case, the handlers you're passing in can be thought of as the "constructor replacing functions", where the constructors in this case are the JSON sub-types (bool, object, array, etc). That's a great insight.
Looking at the recursive Dhall link, is it fair to say then that Dhall/Grace's strategy to recursion is modeling it as a fold where function application is the constructor, with additional parameters for replacing said constructor and the zero. Once those parameters are given, the computation can "collapse".
Right. The idea is that a JSON value like this:
[ true, 1, [ -2, false, "" ], null, { "foo": { } } ]
โฆ is modeled as:
\constructors ->
constructors.array
[ constructors.bool true
, constructors.natural 1
, constructors.array [ constructors.integer -2, constructors.bool false, constructors.string "" ]
, constructors.null
, constructors.object [ { key = "foo", value = constructors.object [ ] } ]
]
โฆ and the "handlers" that you're passing to JSON/fold
become the constructors
argument to that function.