JSON.Value

The interfaces in this module abstract over how we
encode and decode values from and to JSON.

This allows us to use different (probably backend dependant)
intermediary data representations to be used by the actual
marshallers `ToJSON` and `FromJSON`.

Definitions

maxSafeInteger : Integer

  In Javascript, numbers are represented as IEEE 64bit
  floating point numbers. Integers can be represented exactly
  in the range [-(2^53-1), 2^53-1]. This library's default
  behavior is, that large integers will be encoded as
  `string` and smaller values use `number`

Visibility: public export

interface Encoder : Type -> Type

  Abstraction over JSON value encoding.

Parameters: v
Methods:

stringify : v -> String

  Converts the intermediary data representation
  to a JSON string.

string : String -> v

  Encodes a `String` value.

number : Double -> v

  Encodes a `Double` as a JSON `Number`.

boolean : Bool -> v

  Encodes a `Bool` as a JSON `Boolean`.

array : List v -> v

  Encodes a `List` of values as a JSON `Array`.

object : List (String, v) -> v

  Encodes a `List` key-value pairs as a JSON `Object`

null : v

Implementation: 

Encoder JSON

stringify : Encoder v => v -> String

  Converts the intermediary data representation
  to a JSON string.

Visibility: public export

string : Encoder v => String -> v

  Encodes a `String` value.

Visibility: public export

number : Encoder v => Double -> v

  Encodes a `Double` as a JSON `Number`.

Visibility: public export

boolean : Encoder v => Bool -> v

  Encodes a `Bool` as a JSON `Boolean`.

Visibility: public export

array : Encoder v => List v -> v

  Encodes a `List` of values as a JSON `Array`.

Visibility: public export

object : Encoder v => List (String, v) -> v

  Encodes a `List` key-value pairs as a JSON `Object`

Visibility: public export

null : Encoder v => v

Visibility: public export

smallInteger : Encoder v => Integer -> v

  Encode a small integer (less than or equal to `maxSafeInteger`)
  as a number.

Visibility: export

largeInteger : Encoder v => Integer -> v

  Encode an `Integer` (possibly larger than `masSafeInteger`)
  as a number or a string.
  
  The corresponding decoder for potentially large numbers
  will also try both types: Number and string.

Visibility: export

interface Object : Type -> Type -> Type

  Abstraction over JSON Object representation for decoding.
  It is important that `obj` is the type that guides interface
  resolution here, otherwise operators like `.:` cannot conveniently
  be used, since Idris needs additional guidance to resolve interfaces.

Parameters: obj, v
Methods:

lookup : String -> obj -> Maybe v

Implementation: 

Object (List (String, JSON)) JSON

lookup : Object obj v => String -> obj -> Maybe v

Visibility: public export

interface Value : Type -> Type -> Type

  Abstraction over JSON value representation for decoding.

Parameters: v, obj
Constraints: Object obj v
Methods:

typeOf : v -> String

  Returns the actual value. This should be one of
  "String", "Null", "Object", "Number", "Boolean", or "Array".
  However, other types are possible as well, as this is
  only used for error messages when something goes wrong.

parse : String -> Either ParseErr v

  Tries to convert a string to an intermediare value.

getObject : v -> Maybe obj

  Tries to convert a value to an `Object`.

getArray : v -> Maybe (List v)

  Tries to convert a value to an `Array` of values.

getBoolean : v -> Maybe Bool

  Tries to convert a value to a `Boolean`.

getNumber : v -> Maybe Double

  Tries to convert a value to a `Number`.

getString : v -> Maybe String

  Tries to convert a value to a `String`.

isNull : v -> Bool

  `True`, if the value in question is `null`.

Implementation: 

Value JSON (List (String, JSON))

typeOf : Value v obj => v -> String

  Returns the actual value. This should be one of
  "String", "Null", "Object", "Number", "Boolean", or "Array".
  However, other types are possible as well, as this is
  only used for error messages when something goes wrong.

Visibility: public export

parse : Value v obj => String -> Either ParseErr v

  Tries to convert a string to an intermediare value.

Visibility: public export

getObject : Value v obj => v -> Maybe obj

  Tries to convert a value to an `Object`.

Visibility: public export

getArray : Value v obj => v -> Maybe (List v)

  Tries to convert a value to an `Array` of values.

Visibility: public export

getBoolean : Value v obj => v -> Maybe Bool

  Tries to convert a value to a `Boolean`.

Visibility: public export

getNumber : Value v obj => v -> Maybe Double

  Tries to convert a value to a `Number`.

Visibility: public export

getString : Value v obj => v -> Maybe String

  Tries to convert a value to a `String`.

Visibility: public export

isNull : Value v obj => v -> Bool

  `True`, if the value in question is `null`.

Visibility: public export