Year 2015 Day 12
This day provides an introduction to our new
Parser.JSON module, as well as the use of DLists1
to collect values from an indexed type family into a single collection.
import Structures.Dependent.DList
import Parser
import Parser.JSON
Parsing
Parse a list of JSON values into a DList.
JSONValue's type constructor has the signature JSONType -> Type, forming
what is known as an "Indexed Type Family".
Each type of JSON value has a separate type, e.g. a Bool has type
JSONValue TBool, a String has type JSONValue TString, etc. While these are
all separate types, they all share the JSONValue component of the type
constructor, making them members of the same family.
Despite being members of the same type family, they still have different types,
so we can't just shove JSONValues of different types into, say, a
List JSONValue, we need a collection with some amount of heterogeneity. While
a List (type : JSONType ** JSONValue type) would work, that introduces
various ergonomic headaches, so instead we return a DList1, a List like
data structure specifically designed for collecting values from an indexed typed
family into a single collection.
The parsing logic is otherwise quite simple, we use the many combinator to
turn the value parser, which parses a single JSON value, into one that parses
a list of JSON values, and then use DList's fromList method to collect the
results into a DList.
parseJsons : Has (Except String) fs => Has IO fs => (input : String)
-> Eff fs (types : List JSONType ** DList JSONType JSONValue types)
parseJsons input = do
result <- runFirstIO (many value) input
case result of
Left err => throw $ show err
Right result => pure $ fromList result
Solving
A reducer for DList.dFoldL that sums all the numbers within the contained JSON
Value.
The outer function is meant to be called on a top level object, using
DList.dFoldL on a DList of JSONValues, where as the inner function
directly reduces a JSONValue using JSON.dFoldL.
sumNumbers : Double -> (type : JSONType) -> (value : JSONValue type) -> Double
sumNumbers dbl type value = dFoldL sumNumbers' dbl value
where
sumNumbers' : Double -> (type : JSONType) -> (value : JSONValue type) -> Double
sumNumbers' dbl TNumber (VNumber d) = dbl + d
sumNumbers' dbl _ value = dbl
Filter out objects containing a "red" key
noRed : (type : JSONType) -> (value : JSONValue type) -> Bool
noRed TObject value =
let (types ** vals) = getValues value
in case dFind (\t, v =>
case t of
TString => v == (VString "red")
_ => False
) vals of
Nothing => True
Just _ => False
noRed _ value = True
sumNumbersNoRed :
Double -> (type : JSONType) -> (value : JSONValue type) -> Double
sumNumbersNoRed dbl type value =
case dFilter noRed value of
Nothing => dbl
Just value => sumNumbers dbl type value
Part Functions
Part 1
Parse our JSONs, then fold our sumNumbers reducer over them.
part1 : Eff (PartEff String)
(Double, (types : List JSONType ** DList JSONType JSONValue types))
part1 = do
input <- askAt "input"
(types ** values) <- parseJsons input
let result = dFoldL sumNumbers 0.0 values
pure (result, (types ** values))
Part 2
part2 : (types : List JSONType ** DList JSONType JSONValue types)
-> Eff (PartEff String) Double
part2 (types ** values) = do
let result = dFoldL sumNumbersNoRed 0.0 values
pure result