Gabriella439/grace

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.

loop (Value.List elements) =
apply arrayHandler (Value.List (fmap loop elements))
loop (Value.Record keyValues) =
apply objectHandler (Value.List (Seq.fromList (map adapt (HashMap.toList keyValues))))
where
adapt (key, value) =
Value.Record
[("key", Value.Scalar (Text key)), ("value", loop value)]

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.