Dex: Typed Visualization

Declarative Graphing

This example shows how to use Dex to generate interactive graphs using a declarative graph library known as Vega-Lite. To do this we will first implement a small JSON serialization library and then a Dex interface to produce graph outputs.

JSON Implementation

def join (joiner: List a) (lists:n=>(List a)) : List a = -- Join together lists with an intermediary joiner concat $ for i. case ordinal i == (size n - 1) of True -> lists.i False -> lists.i <> joiner

A serialized JSON Value

-- TODO - once Dex supports recursive ADT JValue becomes Value.
data JValue = AsJValue String

Simple JSON Data Type

data Value = AsObject (List (String & JValue)) AsArray (List JValue) AsString String AsFloat Float AsInt Int AsNone
interface ToJSON a toJSON : a -> Value
instance Show JValue show = \ (AsJValue a). a

Serialization Methods

def toJValue (x:Value) : JValue = AsJValue $ case x of AsString y -> "\"" <> y <> "\"" AsFloat y -> show y AsInt y -> show y AsObject (AsList _ y) -> ("{" <> (join ", " $ for i. (k, v) = y.i "\"" <> k <> "\"" <> ":" <> (show v)) <> "}") AsArray (AsList _ y) -> ("[" <> (join ", " $ for i. show y.i) <> "]") AsNone -> ""
def serialize [ToJSON a] (x:a) : JValue = toJValue $ toJSON x
instance Show Value show = \x. show $ toJValue x

Type classes for JSON conversion

instance ToJSON String toJSON = AsString
instance ToJSON Int toJSON = AsInt
instance ToJSON Float toJSON = AsFloat
instance ToJSON Value toJSON = id
instance [ToJSON v] ToJSON (n => v) toJSON = \x . sizen = (size n) tab = castTable (Fin sizen) $ for i. serialize x.i AsArray $ AsList sizen tab
instance [ToJSON v] ToJSON (List v) toJSON = \(AsList _ x) . toJSON x
instance [ToJSON v] ToJSON (n => (String & v)) toJSON = \x . sizen = (size n) tab = castTable (Fin sizen) $ for i. (fst x.i, serialize $ snd x.i) AsObject $ AsList _ tab
instance [ToJSON v] ToJSON (List (String & v)) toJSON = \(AsList _ x) . toJSON x
def wrapCol [ToJSON d] (iso: Iso a (d & c)) (x:n=>a) : n=> Value = -- Helper function. Returns JSON of a column of a record for i. toJSON $ getAt iso x.i

Declarative Graph Grammars

Graph grammars are a style of graphing that aims to separate the data representation from the graph layout. The main idea is to represent the underlying data as a flat sequence of aligned rows (colloquially a dataframe) and separately describe the graph layout based on a grammar.

Here we implement a subset of the Vega-Lite ( specification for graphing. Vega-Lite lets you make a large set of charts using a very small grammar.

We will have several pieces of metadata. A header string, encoding type, and the channels that the data is displayed with.

Header = String
data EncodingType = Quantitative Nominal Ordinal
instance Show EncodingType show = (\ x. case x of Quantitative -> "quantitative" Nominal -> "nominal" Ordinal -> "ordinal")
data Channel = Y X Color Tooltip HREF Row Col Size
instance Show Channel show = (\ x. case x of Y -> "y" X -> "x" Color -> "color" Tooltip -> "tooltip" HREF -> "href" Size -> "size" Row -> "row" Col -> "col")

The final aspect of Vega-Lite is the Mark. The mark tells it what kind of graph to draw, and the channels allow us to assign different columns to different roles. We implement these as simple data types, ideally these would be derived from the spec.

data Mark = Area Bar Circle Line Point Rect Rule Square Text Tick
instance Show Mark show = (\ x. case x of Area -> "area" Bar -> "bar" Circle -> "circle" Line -> "line" Point -> "point" Rect -> "rect" Rule-> "rule" Square -> "square" Tick -> "tick")

Most things in VL can take in extra visual options. To avoid specifying these, we will take in as JSON.

data Opts a = WithOpts a Value
def pure (x:a) : Opts a = WithOpts x AsNone
def pureLs (x:a) : List (Opts a) = AsList 1 [WithOpts x AsNone]
def mergeOpts [ToJSON a, ToJSON b] (x : a) (y : b) : Value = case toJSON x of (AsObject x') -> case toJSON y of (AsObject y') -> AsObject $ x' <> y' (AsNone) -> AsObject x' (AsNone) -> toJSON y
data VLChart row col v = AsVLDescriptor (Opts Mark) v (col => ({title: Header & encType: EncodingType & encodings: List (Opts Channel) & rows: row => Value }))
instance [ToJSON v] ToJSON (VLChart r c v) toJSON = \ x. (AsVLDescriptor mark opts df) = x -- Make the mark (WithOpts mtype options) = mark jmark = ("mark", mergeOpts options [("type", show mtype)]) -- Make the data jdf = toJSON $ for row : r. toJSON $ for col : c. ("col" <> (show $ ordinal col), toJSON (getAt #rows df.col).row) jdata = ("data", toJSON [("values", jdf)]) -- Make the encodings jencodings = toJSON $ concat $ for col : c. (AsList v encopts) = getAt #encodings df.col AsList v $ for f. (WithOpts channel encoptions) = encopts.f (show channel, mergeOpts encoptions [ ("field", "col" <> (show $ ordinal col)), ("type", show $ getAt #encType df.col), ("title", getAt #title df.col) ]) jencode = ("encoding", jencodings) mergeOpts opts [jdata, jmark, jencode]
def showVega (x: Value) : String = "<iframe width=\"100%\" frameborder=\"0\" scrolling=\"no\" onload=\"'px'\"; srcdoc='<html> <head><script src=\"\"></script> <script src=\"\"></script> <script src=\"\"></script> </head> <body> <div id=\"vis\"></div> <script>vegaEmbed(\"#vis\"," <> (show x) <> ");</script> </body> </html>'> </iframe>"

Example: Bar Chart

Start with a well type and useful Dex record

df1 = for i. {a = ["A", "B", "C", "D", "E", "F", "G", "H", "I"].i, b = [28, 55, 43, 91, 81, 53, 19, 87, 52].i}
chart1 = (AsVLDescriptor (pure Bar) [("title", "Bar Graph")] [{title="a axis", encodings=pureLs X, encType=Nominal, rows=wrapCol #a df1}, {title="b axis", encodings=pureLs Y, encType=Quantitative, rows=wrapCol #b df1}] )
:html showVega $ toJSON chart1

Example: Scatter

This example constructs a scatter plot with several different variables.

First we will construct a Nominal variable for a class.

data Class = A B C
instance Show Class show = \x . case x of A -> "Apples" B -> "Bananas" C -> "Cucumbers"
instance Arbitrary Class arb = \key. [A, B, C].(arb key)
instance ToJSON Class toJSON = \x. AsString $ show x

Then we will generate some random data.

key : Key = newKey 1
df2 :(Fin 100) => {x1:Float & x2:Float & weight:Float & label:Class} = for i: (Fin 100). [k1, k2, k3, k4] = splitKey $ ixkey key i {x1=(arb k1), x2=arb k2, weight=arb k3, label=arb k4}

The descriptor has a mapping between the variable names and their encoding type.

We use a different mark Point and pass in multiple Channels for some variables.

chart2 = (AsVLDescriptor (pure Point) [("title", "Scatter")] [{title="X1", encodings=pureLs X, encType=Quantitative, rows=wrapCol #x1 df2}, {title="X2", encodings=pureLs Y, encType=Quantitative, rows=wrapCol #x2 df2}, {title="Weight", encodings=pureLs Size, encType=Quantitative, rows=wrapCol #weight df2}, {title="Label", encodings=toList [pure Color, pure Tooltip], encType=Nominal, rows=wrapCol #label df2}])
:html showVega $ toJSON chart2

Example: Faceted Area plot

This example show three different random walks. In particular in demonstrates how VL can auto-facet the chart based on Nominal variables.

y1 : (Fin 3) => (Fin 10) => Float = arb $ newKey 0
df3 = for i. cumSum . for j. select (y1.i.j > 0.0) (-1.0) 1.0
:t df3
((Fin 3) => (Fin 10) => Float32)
chart3 = (AsVLDescriptor (pure Area) [("title", "Area"), ("height", "75")] [{title="density", encodings=pureLs Y, encType=Quantitative, rows=for (i,j). toJSON df3.i.j}, {title="Runs", encodings=pureLs Row, encType=Nominal, rows= for (i,_). toJSON $ ["Run 1", "Run 2", "Run 3"].i}, {title="Round", encodings=pureLs X, encType=Ordinal, rows=for (_,j). toJSON $ ordinal j}] )
:html showVega $ toJSON chart3

Example: Heatmap

words = ["the", "dog", "walked", "to", "the", "store"]
z : (Fin 6) => (Fin 6) => Float = arb $ newKey 0
def showChart4 [ToJSON o] (opts:o) : Value = toJSON (AsVLDescriptor (pure Rect) opts [{title="match", encodings=pureLs Color, encType=Quantitative, rows=for (i,j). toJSON z.i.j}, {title="words", encodings=pureLs Tooltip, encType=Nominal, rows=for (i,j). toJSON (words.i <> " - " <> words.j)}, {title="row", encodings=pureLs X, encType=Ordinal, rows=for (i,_). toJSON (ordinal i)}, {title="col", encodings=pureLs Y, encType=Ordinal, rows=for (_,j). toJSON (ordinal j)}] )

Default heat map

:html showVega $ showChart4 AsNone

Customization through JSON options.

:html showVega $ showChart4 $ mergeOpts [("title", "HeatMap"), ("height", "200"), ("width", "200")] [("config", toJSON [ ("axis", [("grid", "1"), ("tickBand", "extent")]) ])]