Declarative Graphing + JSON/DataFrames

examples/json.dx

@@ -0,0 +1,364 @@
+
+
+' # 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 ((Fin n) => v)
+  toJSON = \x . AsArray $ AsList _ $ for i. serialize x.i
+
+instance [ToJSON v] ToJSON (List v)
+  toJSON = \(AsList _ x) . toJSON x
+
+instance [ToJSON v] ToJSON ((Fin n) => (String & v))
+  toJSON = \x . AsObject $ AsList _ $ for i. (fst x.i, serialize $ snd x.i)
+
+instance [ToJSON v] ToJSON (List (String & v))
+  toJSON = \(AsList _ x) . toJSON x
+
+
+' ## 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 (https://vega.github.io/vega-lite/) specification for
+  graphing. Vega-Lite lets you make a large set of charts using a very small grammar. 
+
+
+' Our Dataframe will be Table that associates meta data with columns. 
+
+data DataFrame row col value meta =
+     AsDataFrame  (col => meta) (row => col => value) 
+
+
+' We will have two pieces of metadata. A header string and an encoding type that
+  describes the role of the column.
+
+Header = String
+
+
+data EncodingType =
+     Quantitative
+     Nominal
+     Ordinal
+
+instance Show EncodingType
+   show = (\ x.
+       case x of
+         Quantitative -> "quantitative"
+         Nominal -> "nominal"
+         Ordinal -> "ordinal")
+
+
+' The two main aspects of Vega-Lite are the Mark and the Channel.
+  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")
+
+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")
+
+' 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
+
+def VLDataFrame (row:Type) (col:Type) (value:Type): Type =
+    DataFrame row col value (Header & EncodingType) 
+
+
+def chart [ToJSON v, ToJSON o] (x: VLDataFrame n (Fin key) v)
+                     (mark: Opts Mark)
+                     (encs : (Fin key) => List (Opts Channel))
+                     (opts : o)
+             : Value =
+
+    -- Make the mark
+    (WithOpts mtype options) = mark
+    jmark = ("mark", mergeOpts options [("type", show mtype)])
+
+    -- Make the data
+    (AsDataFrame meta df) = x
+    finsize = Fin $ size n
+    jdf = toJSON $ castTable finsize $ for i. toJSON $ for k.
+                   ("field" <> (show $ ordinal k),
+                   toJSON df.i.k)
+    jdata = ("data", toJSON [("values", jdf)])
+
+    -- Make the encodings
+    jencodings = toJSON $ concat $ for i.
+        (AsList v encopts) = encs.i
+        AsList _ $ for c : (Fin v). 
+           (WithOpts channel encoptions) = encopts.c
+           (title, type):(String & EncodingType) = meta.i
+           (show channel,
+            mergeOpts encoptions 
+            [
+              ("field", "field" <> (show $ ordinal i)),
+              ("type", show type),
+              ("title", title)
+              ])           
+    jencode = ("encoding", jencodings)
+    mergeOpts opts [jdata, jmark, jencode]
+
+
+def showVega (x: Value) : String =
+    "<iframe width=\"100%\" frameborder=\"0\" scrolling=\"no\" onload=\"resizeIframe(this)\" srcdoc='<html> 
+    <head><script src=\"https://cdn.jsdelivr.net/npm/[email protected]\"></script>  
+          <script src=\"https://cdn.jsdelivr.net/npm/[email protected]\"></script>  
+          <script src=\"https://cdn.jsdelivr.net/npm/[email protected]\"></script> 
+    </head> 
+    <body> 
+           <div id=\"vis\"></div>
+           <script>vegaEmbed(\"#vis\"," <> (show x) <> ");</script>
+    </body>
+    </html>'>
+    </iframe>"
+
+' ## Example: Bar Chart
+
+a_data = ["A", "B", "C", "D", "E", "F", "G", "H", "I"]
+b_data = [28, 55, 43, 91, 81, 53, 19, 87, 52]
+
+df0 = (AsDataFrame [("a", Nominal), ("b", Quantitative)]
+                   (for i. [toJSON a_data.i, toJSON b_data.i]))
+
+
+c = (chart df0 (pure Bar)
+     [pureLs X, pureLs Y]
+     [("title", "Bar Graph")])
+
+:html showVega $ c
+
+
+' ## 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"
+
+' Then we will generate some random data. 
+
+keys : (Fin 5) => Key = splitKey $ newKey 1
+x1 : (Fin 100) => Float = arb $ keys.(0 @ _)
+x2 : (Fin 100) => Float = arb $ keys.(1 @ _)
+weight : (Fin 100) => Float = arb $ keys.(2 @ _)
+label : (Fin 100) => Class =
+      x = arb $ keys.(3 @ _)
+      for i. [A, B, C] (x.i)
+
+' The data frame has a mapping between the variable names and their encoding type.
+
+df = (AsDataFrame
+        [("X1", Quantitative), ("X2", Quantitative), ("Weight", Quantitative), ("Label", Nominal)]
+         (for i. [toJSON $ x1.i,
+                 toJSON $ x2.i,
+                 toJSON $ weight.i,
+                 toJSON $ show label.i]))
+
+
+' We use a different mark `Bar` and pass in multiple Channels for some variables.
+
+:html showVega (chart df (pure Point)
+         [pureLs X, pureLs Y, pureLs Size,
+          AsList _ [pure Color, pure Tooltip]]
+          [("title", "Scatter")])
+
+' ## 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 $ keys.(0 @ _)
+y = for i. cumSum . for j. select (y1.i.j > 0.0) (-1.0) 1.0 
+
+df2 = (AsDataFrame
+    [("density", Quantitative), ("Runs", Nominal), ("Round", Ordinal)]
+        (for (i,j). [toJSON $ y.i.j,
+                     toJSON $ ["Run 1", "Run 2", "Run 3"].i,
+                     toJSON $ ordinal j]))
+
+
+:html showVega (chart df2 (pure Area)
+                [pureLs Y,
+                 pureLs Row,
+                 pureLs X]
+                 [("title", "Area"), ("height", "75")])
+
+
+' ## Example: Heatmap
+
+words = ["the", "dog", "walked", "to", "the", "store"]
+
+z :  (Fin 6) => (Fin 6) => Float = arb $ keys.(0 @ _)
+
+df3 = (AsDataFrame
+        [("match", Quantitative) , ("words", Nominal), ("row", Ordinal), ("col", Ordinal)]
+        (for (i,j). [toJSON $ z.i.j,
+                     toJSON $ words.i <> " - " <> words.j,
+                     toJSON $ ordinal i,
+                     toJSON $ ordinal j
+                     ]))
+
+' Default heat map
+
+:html showVega (chart df3 (pure Rect)
+       [pureLs Color,
+        pureLs Tooltip,
+        pureLs X,
+        pureLs Y] AsNone)
+
+' Customization through JSON options.
+
+
+:html showVega (chart df3 (pure Rect)
+       [pureLs Color,
+        pureLs Tooltip,
+        pureLs X,
+        pureLs Y] $
+       mergeOpts [("title",  "HeatMap"), ("height",  "200"), ("width",  "200")]
+         [("config", toJSON [
+          ("axis", [("grid", toJSON  1), ("tickBand", toJSON  "extent")])
+          ])]
+       )

static/index.html

@@ -10,6 +10,12 @@
   <link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/[email protected]/dist/katex.min.css" integrity="sha384-AfEj0r4/OFrOo5t7NnNe46zW/tFgW6x/bCJG8FqQCEo3+Aro6EYUG4+cU+KJWu/X" crossorigin="anonymous">
   <script defer src="https://cdn.jsdelivr.net/npm/[email protected]/dist/katex.min.js" integrity="sha384-g7c+Jr9ZivxKLnZTDUhnkOnsh30B4H0rpLUpJ4jAIKs4fnJI+sEnkvrMWph2EDg4" crossorigin="anonymous"></script>
   <script defer src="https://cdn.jsdelivr.net/npm/[email protected]/dist/contrib/auto-render.min.js" integrity="sha384-mll67QQFJfxn0IYznZYonOWZ644AWYC+Pt2cHqMaRhXVrursRwvLnLaebdGIlYNa" crossorigin="anonymous"></script>
+
+<script>
+  function resizeIframe(obj) {
+    obj.style.height = obj.contentWindow.document.documentElement.scrollHeight + 'px';
+  }
+</script>
 </head>
 
 <body>