The following interactive session is an example of JSON program that reads a list of records written in JSON.

# val J = "[{n̈ame:̈J̈oe,̈ äge:̈21, g̈rade:̈1.1},"
            ^ "{n̈ame:̈S̈ue,̈ äge:̈31, g̈rade:̈2.0},"
            ^ "{n̈ame:̈B̈ob,̈ äge:̈41, g̈rade:̈3.9}]";
val J =
  "[{"name":"Joe", "age":21, "grade":1.1},
    {"name":"Sue", "age":31, "grade":2.0},
    {"name":"Bob", "age":41, "grade":3.9}]" : string
# fun getNames l = map #name l;
val getNames = fn : [’a#{name: ’b}, ’b. ’a list -> ’b list]
# val j = Dynamic.fromJson J;
val j = _ : Dynamic.void Dynamic.dyn
# val vl = _dynamic j as {name:string, age:int, grade:real} list;
val vl =
  [
   {age = 21,grade = 1.1,name = "Joe"},
   {age = 31,grade = 2.0,name = "Sue"},
   {age = 41,grade = 3.9,name = "Bob"}
  ] : {age: int, grade: real, name: string} list
# val nl = getNames vl;
val nl = ["Joe","Sue","Bob"] : string list

Let us look at a more practical example. Suppose that we intend to deal with the following JSON.

[
  {"name":"Alice", "age":10, "nickname":"Allie"},
  {"name":"Dinah", "age":3, "grade":2.0},
  {"name":"Puppy", "age":7}
]

Let J be the JSON string of this. This is a heterogeneous list. While it is not able to cast such a list to an ML list, we can see that every element in this list has at least name and age field of string and int type, respectively. According to this view, we read this JSON as follows:

val j = Dynamic.fromJson J
val vl = _dynamic j as {name:string, age:int} Dynamic.dyn list

The type of vl is {name:string, age:int} JSON.dyn list, which means a list of partially dynamic records. The static view of this list can be obtained by

val l = map Dynamic.view vl

Then, to obtain name values from the elements, for example, do the following:

val names = map #name l

We usually want to check whether or not a certain field exists in a partially dynamic record in the list. We do this by performing the dynamic type check against each element in the list. For example, suppose we want to get nickname if it exists, or get name otherwise. The following code achieve this:

fun getFriendlyName x =
    _dynamiccase x of
      {nickname = y:string, ...} => y
    | _ : Dynamic.void Dynamic.dyn => #name (Dynamic.view x) val friendlyNames = map getFriendlyName vl

The type of getFriendlyName is [’a#reify#{name : string}. ’a Dynamic.dyn -> string]. Note that the combination of a polymorphic record type and partially dynamic type constitutes this type. What does this type mean? Intuitively, from the perspective of JSON manipulation, one would say that this seems similar to {name : string} Dynamic.dyn -> string. Strictly speaking, the meaning of these two types are different. Latter one can take a JSON object only if exactly its name field is known and thus any other fields must be unknown without further dynamic type checking. In contrast, first one accepts JSON objects if at least its name field is known in spite of determination of any other fields.