From bd1acef61e8c6be9d9afb29fde2eae1b971fed38 Mon Sep 17 00:00:00 2001
From: srush <srush.research@gmail.com>
Date: Wed, 20 Jan 2021 08:54:05 -0500
Subject: [PATCH 1/9] Small change to update syntax and fix indices

---
 examples/tutorial.dx | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/examples/tutorial.dx b/examples/tutorial.dx
index 48a10fb41..ddfe3309c 100644
--- a/examples/tutorial.dx
+++ b/examples/tutorial.dx
@@ -44,7 +44,7 @@ enumeration variable.
 ' We can also display it as html. To do this we include the plot library.
   Right now our table is not so interesting :)
 
-include "plot.dx"
+import "plot.dx"
 
 :html matshow x
 
@@ -113,14 +113,14 @@ mean y
   lets consider how it works. Critically, one cannot
   simply index an table with an integer.
 
-r = x.3
+r = x.2
 
 ' Instead, it is necessary to cast the integer into the index type of the
   current shape. This type annotation is done with the `@` operator.
 
 :t x
 
-row = x.(3 @ Height)
+row = x.(2 @ Height)
 
 :t row
 
@@ -157,7 +157,7 @@ gradient = for i:Height. for j:Width. IToF ((ordinal i) + (ordinal j))
 
 :t y
 
-:t y.(3 @ Height, 5 @ Width)
+:t y.(2 @ Height, 5 @ Width)
 
 ' Tuple indices also provide an ordinal value.
 

From fb5a33b26e035150c43bf5ae2d6a6023340368f2 Mon Sep 17 00:00:00 2001
From: srush <srush.research@gmail.com>
Date: Wed, 20 Jan 2021 09:41:13 -0500
Subject: [PATCH 2/9] Small changes to type classes

---
 examples/tutorial.dx | 77 ++++++++++++++++++++++----------------------
 1 file changed, 38 insertions(+), 39 deletions(-)

diff --git a/examples/tutorial.dx b/examples/tutorial.dx
index ddfe3309c..b891cabe9 100644
--- a/examples/tutorial.dx
+++ b/examples/tutorial.dx
@@ -44,7 +44,7 @@ enumeration variable.
 ' We can also display it as html. To do this we include the plot library.
   Right now our table is not so interesting :)
 
-import "plot.dx"
+import plot
 
 :html matshow x
 
@@ -363,7 +363,7 @@ im2 : Fin 4 => Fin 4 => Fin 7 => Fin 7 => Float32 = imtile ims.(0@_)
 
 def tableMean (x : n => Float32) : Float32 =
     -- acc = 0
-    withState 0.0 $ \acc.
+    runState 0.0 $ \acc.
          -- for i in range(len(x))
          for i.
              -- acc = acc + x[i]
@@ -456,56 +456,56 @@ tableMean (for (i, j). (x.i.j, x.i.j))
   interface. Whereas `(/)` maps `a -> Float32 -> a` where `a` implements the
   `VSpace'` interface.
 
-' If we look in the Prelude, we can see that these interfaces are defined as:
+' If we look in the Prelude, we can see that these interfaces are defined as
+ (This will throw error because it mirrors the prelude, but we are just repeating it here.):
 
-interface Add' a
-  add' : a -> a -> a
-  sub' : a -> a -> a
-  zero' : a
+interface Add a
+  add : a -> a -> a
+  sub : a -> a -> a
+  zero : a
 
-interface [Add' a] VSpace' a
-  scaleVec' : Float -> a -> a
+interface [Add a] VSpace a
+  scaleVec : Float -> a -> a
 
 ' *Interfaces* define *requirements*: the functions needed for a type to
   implement the interface (via an *instance*).
 
-' Here is an `Add'` instance for the float pair type:
+' Here is an `Add` instance for the float pair type.
 
-instance Add' (Float32 & Float32)
-  add' = \(x1,x2) (y1, y2). (x1 + y1, x2 + y2)
-  sub' = \(x1,x2) (y1, y2). (x1 - y1, x2 - y2)
-  zero' = (0.0, 0.0)
+instance Add (Float32 & Float32)
+  add = \(x1,x2) (y1, y2). (x1 + y1, x2 + y2)
+  sub = \(x1,x2) (y1, y2). (x1 - y1, x2 - y2)
+  zero = (0.0, 0.0)
 
-' And here is a `VSpace'` instance for the float pair type:
+' And here is a `VSpace` instance for the float pair type:
 
-instance VSpace' (Float32 & Float32)
-  scaleVec' = \s (x, y). (x / s, y / s)
+instance VSpace (Float32 & Float32)
+  scaleVec = \s (x, y). (x * s, y * s)
 
 ' Once we have these two instance definitions, we can revisit our table sum
   function using them:
 
-def tableMean' [Add' v, VSpace' v] (x : n => v) : v =
-    z: v = zero'
-    yieldState z $ \acc: (Ref _ v).
+def tableMean' [VSpace v] (x : n => v) : v =
+   withState zero $ \acc: (Ref _ v).
         for i.
-            acc := add' (get acc) x.i           -- `Add'` requirement
-            scaleVec' (IToF (size n)) (get acc) -- `VSpace'` requirement
+            acc := add (get acc) x.i       -- `Add` requirement
+        (get acc) / (IToF (size n))  -- `VSpace` requirement
 
-tableMean' [0.1, 0.5, 1.0]
+tableMean' [0.1, 0.5, 0.9]
 
 tableMean' [(1.0, 0.5), (0.5, 0.8)]
 
 ' The instance values are hardcoded for the float pair type. To be more general,
-  we can and should instead define `Add'` and `VSpace'` instances for generic
+  we can and should instead define `Add` and `VSpace` instances for generic
 ' tuple types.
 
-instance [Add' v, Add' w] Add' (v & w)
-  add' = \(x1,x2) (y1, y2). (x1 + y1, x2 + y2)
-  sub' = \(x1,x2) (y1, y2). (x1 - y1, x2 - y2)
-  zero' = (zero, zero)
+instance [Add v, Add w] Add (v & w)
+  add = \(x1,x2) (y1, y2). (x1 + y1, x2 + y2)
+  sub = \(x1,x2) (y1, y2). (x1 - y1, x2 - y2)
+  zero = (zero, zero)
 
-instance [VSpace' v, VSpace' w] VSpace' (v & w)
-  scaleVec' = \s (x, y). (x / s, y / s)
+instance [VSpace v, VSpace w] VSpace (v & w)
+  scaleVec = \s (x, y). (scaleVec s x, scaleVec s y)
 
 '## More MNist
 
@@ -516,7 +516,7 @@ instance [VSpace' v, VSpace' w] VSpace' (v & w)
 Pixels = Fin 256
 
 def bincount (inp : a => b) : b => Int =
-    withState zero' \acc .
+    withState zero \acc .
         for i.
             v = acc!(inp.i)
             v := (get v) + 1
@@ -563,15 +563,15 @@ double = for b i j. [ims.b.i.j, ims.(nearest.b).i.j, 0.0]
 
 :t for i:Height. 0.0
 
-AsList _ $ for i:Height. 0.0
+toList for i:Height. 0.0
 
-:t AsList _ $ for i:Height. 0.0
+:t toList for i:Height. 0.0
 
 ' Tables of lists can be concatenated down to
   single lists.
 
-z = concat [AsList _ [3.0],
-        AsList _ [1.0, 2.0 ]]
+z = concat [toList [3.0],
+            toList [1.0, 2.0 ]]
 z
 
 ' And they can be deconstructed to fetch a new table.
@@ -580,13 +580,12 @@ z
 temptab
 
 ' Using this construct we can return to extracting
-  the 5's from the image set. Here `mempty` is
-  synonymous with `AsList _ []`.
+  the 5's from the image set.
 
 def findFives (x : a=>b) (y : a=>Class) : List b =
     concat for i. case (y.i == (5 @ _)) of
-            True -> AsList _ [x.i]
-            False -> mempty
+            True -> toList [x.i]
+            False -> toList []
 
 ' Note though that the type here does not tell us
   how many 5's there are. The type system cannot know this.

From 1c95ce7d5b614079fbe6d3c39418dbc77d6601c8 Mon Sep 17 00:00:00 2001
From: srush <srush.research@gmail.com>
Date: Wed, 20 Jan 2021 14:26:04 -0500
Subject: [PATCH 3/9] add to CI

---
 examples/tutorial.dx | 91 +++++++++++++++++++++++++++++++++++++++++++-
 makefile             |  2 +-
 2 files changed, 90 insertions(+), 3 deletions(-)

diff --git a/examples/tutorial.dx b/examples/tutorial.dx
index b891cabe9..d5c95dd8c 100644
--- a/examples/tutorial.dx
+++ b/examples/tutorial.dx
@@ -30,12 +30,16 @@ x = for i:Height. for j:Width. 1.0
 ' Once we have a variable, we can print it.
 
 x
+> [ [1., 1., 1., 1., 1., 1., 1., 1.]
+> , [1., 1., 1., 1., 1., 1., 1., 1.]
+> , [1., 1., 1., 1., 1., 1., 1., 1.] ]
 
 ' More interestingly, we can also see its type with `:t`. This type tells us
   that `x` is a two-dimensional table, whose first dimension has type `Height` and
   second dimension has type `Width`.
 
 :t x
+> ((Fin 3) => (Fin 8) => Float32)
 
 ' Here `Fin` stands for `finite` represents the type of range from 0
 to the value given minus one. The `:` tells us the type of the
@@ -47,6 +51,7 @@ enumeration variable.
 import plot
 
 :html matshow x
+> <html output>
 
 ' Once we have an table, we can use it in new comprehensions. For example,
   let's try to add `5` to each table element. In Python, one might write this as:
@@ -58,6 +63,7 @@ import plot
   subscripting.
 
 :t for i:Height. for j:Width. x.i.j + 5.0
+> ((Fin 3) => (Fin 8) => Float32)
 
 ' However, we can make this expression nicer. Because `x` has a known table type
   and `i` and `j` index into that type, Dex can infer the range of the loop.
@@ -65,16 +71,19 @@ import plot
   get the same result.
 
 :t for i. for j. x.i.j + 5.0
+> ((Fin 3) => (Fin 8) => Float32)
 
 ' Dex also lets you reduce this expression to include multiple variables
   in the same `for`.
 
 :t for i j. x.i.j + 5.0
+> ((Fin 3) => (Fin 8) => Float32)
 
 ' Standard functions can be  applied as well. Here we take the
   `mean` over each column:
 
 :t for i. mean x.i
+> ((Fin 3) => Float32)
 
 ' This style of using `for` to construct type-inferred tables is central to what
   makes Dex powerful. Tables do not only need to have `Fin` types.
@@ -98,6 +107,7 @@ y5 = for i. y.i + 5.0
 ' And we can apply table functions to the table:
 
 mean y
+> 1.
 
 ' But things start to get interesting when we consider the type of the
   table.  Unlike the Python example, which produces a flat list (or
@@ -106,6 +116,7 @@ mean y
   remembers the original ranges.
 
 :t y
+> ((Fin 3 & Fin 8) => Float32)
 
 '## Typed indexing
 
@@ -114,23 +125,33 @@ mean y
   simply index an table with an integer.
 
 r = x.2
+> Type error:
+> Expected: (Fin 3)
+>   Actual: Int32
+>
+> r = x.2
+>       ^
 
 ' Instead, it is necessary to cast the integer into the index type of the
   current shape. This type annotation is done with the `@` operator.
 
 :t x
+> ((Fin 3) => (Fin 8) => Float32)
 
 row = x.(2 @ Height)
 
 :t row
+> ((Fin 8) => Float32)
 
 :t row.(5 @ Width)
+> Float32
 
 ' If you are feeling lazy and sure of yourself, you can also let Dex infer
   the type for you. This is also how `for` works in the examples above that
   did not provide and explicit type annotation.
 
 :t row.(5 @ _)
+> Float32
 
 ' If it helps, you can think of table indexing as function application: `a.i` applies
   table `a` with index `i` just like how `f x` applies function `f` with
@@ -141,14 +162,22 @@ row = x.(2 @ Height)
   This is because finite sets i.e. `Fin` are not closed under addition.
 
 :t for i:Height. for j:Width. i + j
+> Type error:
+> Expected: (Fin 3)
+>   Actual: (Fin 8)
+>
+> :t for i:Height. for j:Width. i + j
+>                                   ^
 
 :t for i:Height. for j:Width. (ordinal i) + (ordinal j)
+> ((Fin 3) => (Fin 8) => Int32)
 
 ' If we want to convert these values to floats, we do it manually with the `IToF`
   function. We can use this to make an image gradient.
 
 gradient = for i:Height. for j:Width. IToF ((ordinal i) + (ordinal j))
 :html matshow gradient
+> <html output>
 
 ' As we have seen, indices are not limited to only integers. Many different Dex
   types are valid index types. For example, we declared table `y` as having a
@@ -156,12 +185,15 @@ gradient = for i:Height. for j:Width. IToF ((ordinal i) + (ordinal j))
   into `y` requires creating a tuple value.
 
 :t y
+> ((Fin 3 & Fin 8) => Float32)
 
 :t y.(2 @ Height, 5 @ Width)
+> Float32
 
 ' Tuple indices also provide an ordinal value.
 
 for pair:(Fin 2 & Fin 3). ordinal pair
+> [0, 1, 2, 3, 4, 5]@(Fin 2 & Fin 3)
 
 
 ' Many algorithms in Dex come down to being able to pack and unpack these
@@ -170,6 +202,7 @@ for pair:(Fin 2 & Fin 3). ordinal pair
   easily turn it into a 2D table using two `for` constructors.
 
 :t for i. for j. y.(i, j)
+> ((Fin 3) => (Fin 8) => Float32)
 
 ' Again, we rely on type inference in order to avoid explicitly spelling the
   ranges.
@@ -183,8 +216,10 @@ for pair:(Fin 2 & Fin 3). ordinal pair
   of an table. We can apply `mean` to `x2` to produce the sum over 50 elements:
 
 :t y
+> ((Fin 3 & Fin 8) => Float32)
 
 :t mean y
+> Float32
 
 ' The `mean` function works independently of the index type of the table.
 
@@ -195,13 +230,16 @@ def add5 (x:Float32) : Float32 =
     x + 5.0
 
 add5 1.0
+> 6.
 
 :t for i. add5 y.i
+> ((Fin 3 & Fin 8) => Float32)
 
 ' Functions also have types. Note that that function types in Dex
   use the `->` symbol whereas tables use `=>`.
 
 :t add5
+> (Float32 -> Float32)
 
 ' We can also write functions with type variables over their inputs. For
   instance, we may want to be able to write a function that applies "adds 5"
@@ -213,6 +251,7 @@ def tableAdd5' (x : n => Float32) : n => Float32 =
     for i. x.i + 5.0
 
 :t tableAdd5' y
+> ((Fin 3 & Fin 8) => Float32)
 
 ' But function types can help you out even more. For instance, since index types
   are statically known, type checking can ensure that table arguments have valid
@@ -231,13 +270,21 @@ def trans (x : m => n => v) : n => m => v =
 ' We can also use this to check for shape errors:
 
 :t x
+> ((Fin 3) => (Fin 8) => Float32)
 
 def tableAdd' (x : m => n => Float32) (y : m => n => Float32) : m => n => Float32 =
     for i. for j. x.i.j + y.i.j
 
 :t tableAdd' x x
+> ((Fin 3) => (Fin 8) => Float32)
 
 :t tableAdd' x (trans x)
+> Type error:
+> Expected: ((Fin 3) => (Fin 8) => Float32)
+>   Actual: ((Fin 8) => (Fin 3) => Float32)
+>
+> :t tableAdd' x (trans x)
+>                 ^^^^^^^
 
 ' The type system checked for us that the input tables indeed have the same shape.
 
@@ -293,20 +340,25 @@ ims = for i : (Fin 100). all_ims.(ordinal i@_)
 
 im = ims.(0 @ _)
 :html matshow im
+> <html output>
 
 :html matshow ims.(1 @ _)
+> <html output>
 
 ' This show the mean pixel value aggregation over all images.
 
 :html matshow (sum ims)
+> <html output>
 
 ' This example overplots three different handwritten images.
 
 imscolor = for i. for j. for c:Channels. ims.((ordinal c)@_).i.j
 
 :t imscolor
+> ((Fin 28) => (Fin 28) => (Fin 3) => Float32)
 
 :html imshow (imscolor / 255.0)
+> <html output>
 
 ' This one shows all the images on one channel over the base plot.
 
@@ -316,6 +368,7 @@ imscolor2 = for b. for i. for j. for c:Channels.
              False -> ims.b.i.j
 
 :html imseqshow (imscolor2 / 255.0)
+> <html output>
 
 ' This example utilizes the type system to help manipulate the shape
   of an image. Sum pooling downsamples the image as the max of each
@@ -331,10 +384,12 @@ def imtile (x: a=>b=>v) : n=>o=>p=>q=>v =
 im1 : Fin 2 => Fin 2 => Fin 14 => Fin 14 => Float32 = imtile ims.(0@_)
 
 :html matshow (sum (sum im1))
+> <html output>
 
 im2 : Fin 4 => Fin 4 => Fin 7 => Fin 7 => Float32 = imtile ims.(0@_)
 
 :html matshow (sum (sum im2))
+> <html output>
 
 '## Writing Loops
 
@@ -363,7 +418,7 @@ im2 : Fin 4 => Fin 4 => Fin 7 => Fin 7 => Float32 = imtile ims.(0@_)
 
 def tableMean (x : n => Float32) : Float32 =
     -- acc = 0
-    runState 0.0 $ \acc.
+    withState 0.0 $ \acc.
          -- for i in range(len(x))
          for i.
              -- acc = acc + x[i]
@@ -371,7 +426,9 @@ def tableMean (x : n => Float32) : Float32 =
          -- return acc / len(x)
          (get acc) / (IToF (size n))
 
-:p tableMean [0.0, 1.0, 0.5]
+
+tableMean [0.0, 1.0, 0.5]
+> 0.5
 
 ' So, even though Dex is a functional language, it is possible to write loops
   that look similar to ones that truly perform mutation. However, there is one
@@ -385,8 +442,10 @@ def tableMean (x : n => Float32) : Float32 =
   expressions are identical:
 
 :t tableMean (y + y)
+> Float32
 
 :t tableMean $ y + y
+> Float32
 
 ' Next: `\`. This symbol is the lambda sigil in Dex. It is analogous to the
   `lambda` keyword in Python, and starts the definition of a function value
@@ -395,8 +454,10 @@ def tableMean (x : n => Float32) : Float32 =
   constructor in this case).
 
 :t \ x. x + 10
+> (Int32 -> Int32)
 
 (\ x. x + 10) 20
+> 30
 
 ' That leaves: `withState`. This function uses the `State` effect, enabling us
   to introduce imperative variables into the computation.
@@ -408,6 +469,7 @@ withState 10 $ \ state.
      state := 30
      state := 10
      get state
+> 10
 
 ' The element returned pair is the body function's result (`10`)
 
@@ -421,6 +483,7 @@ withState 10 $ \ state.
         temp = (ordinal i) + 10
         for j:Width.
             temp
+> ((Fin 3) => (Fin 8) => Int32)
 
 ' The other is `:=`, which is an assignment operator that can only be used
   when a `State` effect is available (e.g. inside of a body function passed to
@@ -435,21 +498,31 @@ withState 10 $ \ state.
   integer tables (of type `n => Float32`).
 
 :t tableMean
+> ((n:Type) ?-> (n => Float32) -> Float32)
 
 ' If we try to apply `tableMean` to other types for get errors. For example,
   `tableMean` does not work when applied to a table of *pairs* of floats.
 
 :t (for (i, j). (x.i.j, x.i.j))
+> ((Fin 3 & Fin 8) => (Float32 & Float32))
 
 tableMean (for (i, j). (x.i.j, x.i.j))
+> Type error:
+> Expected: Float32
+>   Actual: (Float32 & Float32)
+>
+> tableMean (for (i, j). (x.i.j, x.i.j))
+>                         ^^^^^^^^^^^^
 
 ' Intuitively, supporting this seems possible. We just need to be able to
   add and divide pair types. Let's look closer at the exact types of the
   addition and division operators.
 
 :t (+)
+> ((a:Type) ?-> (Add a) ?=> a -> a -> a)
 
 :t (/)
+> ((a:Type) ?-> (VSpace a) ?=> a -> Float32 -> a)
 
 ' These function types are a bit complex.
   `(+)` maps `a -> a -> a` with a constraint that `a` implements the `Add'`
@@ -463,9 +536,11 @@ interface Add a
   add : a -> a -> a
   sub : a -> a -> a
   zero : a
+> Error: variable already defined: Add
 
 interface [Add a] VSpace a
   scaleVec : Float -> a -> a
+> Error: variable already defined: VSpace
 
 ' *Interfaces* define *requirements*: the functions needed for a type to
   implement the interface (via an *instance*).
@@ -492,8 +567,10 @@ def tableMean' [VSpace v] (x : n => v) : v =
         (get acc) / (IToF (size n))  -- `VSpace` requirement
 
 tableMean' [0.1, 0.5, 0.9]
+> 0.5
 
 tableMean' [(1.0, 0.5), (0.5, 0.8)]
+> (0.75, 0.65)
 
 ' The instance values are hardcoded for the float pair type. To be more general,
   we can and should instead define `Add` and `VSpace` instances for generic
@@ -526,8 +603,10 @@ def bincount (inp : a => b) : b => Int =
 
 hist = bincount $ for (i,j). (FToI (ims.(0 @ _).i.j + 1.0) @Pixels)
 :t hist
+> ((Fin 256) => Int32)
 
 :html showPlot $ yPlot (for i. (IToF hist.i))
+> <html output>
 
 ' Find nearest images in the dataset:
 
@@ -544,6 +623,7 @@ nearest = for i. argmin dist.i
 double = for b i j. [ims.b.i.j, ims.(nearest.b).i.j, 0.0]
 
 :html imseqshow double
+> <html output>
 
 '## Variable Length Lists
 
@@ -562,10 +642,13 @@ double = for b i j. [ims.b.i.j, ims.(nearest.b).i.j, 0.0]
   hiding one finite dimension of a table.
 
 :t for i:Height. 0.0
+> ((Fin 3) => Float32)
 
 toList for i:Height. 0.0
+> (AsList 3 [0., 0., 0.])
 
 :t toList for i:Height. 0.0
+> (List Float32)
 
 ' Tables of lists can be concatenated down to
   single lists.
@@ -573,11 +656,13 @@ toList for i:Height. 0.0
 z = concat [toList [3.0],
             toList [1.0, 2.0 ]]
 z
+> (AsList 3 [3., 1., 2.])
 
 ' And they can be deconstructed to fetch a new table.
 
 (AsList _ temptab) = z
 temptab
+> [3., 1., 2.]
 
 ' Using this construct we can return to extracting
   the 5's from the image set.
@@ -595,12 +680,14 @@ temp = findFives all_ims all_labels
 (AsList nFives fives) = temp
 
 nFives
+> 434
 
 ' However we can still utilize the table. For instance
   if we are summing over the hidden dimension, we never
   need to know how big it is.
 
 :html matshow (sum fives)
+> <html output>
 
 '## Conclusion
 
diff --git a/makefile b/makefile
index 13157df5e..f056c44b7 100644
--- a/makefile
+++ b/makefile
@@ -89,7 +89,7 @@ example-names = mandelbrot pi sierpinski rejection-sampler \
                 regression brownian_motion particle-swarm-optimizer \
                 ode-integrator mcmc ctc raytrace particle-filter \
                 isomorphisms ode-integrator linear_algebra fluidsim \
-                sgd chol
+                sgd chol tutorial
 
 test-names = uexpr-tests adt-tests type-tests eval-tests show-tests \
              shadow-tests monad-tests io-tests exception-tests \

From b4bc3c8a98858e3a18bf187f96672cdc0a1a4764 Mon Sep 17 00:00:00 2001
From: srush <srush.research@gmail.com>
Date: Wed, 20 Jan 2021 14:31:52 -0500
Subject: [PATCH 4/9] download binary files

---
 .github/workflows/ci.yaml | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml
index b513e61f0..dada886b0 100644
--- a/.github/workflows/ci.yaml
+++ b/.github/workflows/ci.yaml
@@ -58,5 +58,18 @@ jobs:
     - name: Build
       run: make build
 
+    - name: Download MNist files
+      uses: suisei-cn/actions-download-file@v1
+      id: mnist 
+      with:
+          url: "https://github.com/srush/learns-dex/raw/main/mnist.bin"
+          target: examples/
+    - name: Download MNist labels file
+      uses: suisei-cn/actions-download-file@v1
+      id: labels 
+      with:
+          url: "https://github.com/srush/learns-dex/raw/main/labels.bin"
+          target: examples/
+      
     - name: Run tests
       run: make tests

From b8abc1c510c61ba0be09f578a1ff8b3e3bf205a3 Mon Sep 17 00:00:00 2001
From: srush <srush.research@gmail.com>
Date: Thu, 21 Jan 2021 07:40:32 -0500
Subject: [PATCH 5/9] update github actions and tutorial download

---
 .github/workflows/ci.yaml | 27 ++++++++++++---------------
 examples/tutorial.dx      | 14 ++++++++------
 2 files changed, 20 insertions(+), 21 deletions(-)

diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml
index dada886b0..f17b32d59 100644
--- a/.github/workflows/ci.yaml
+++ b/.github/workflows/ci.yaml
@@ -13,10 +13,10 @@ jobs:
         os: [ubuntu-18.04, macos-latest]
         include:
           - os: macos-latest
-            install_deps: brew install llvm@9 pkg-config
+            install_deps: brew install llvm@9 pkg-config wget gzip
             path_extension: $(brew --prefix llvm@9)/bin
           - os: ubuntu-18.04
-            install_deps: sudo apt-get install llvm-9-tools llvm-9-dev pkg-config
+            install_deps: sudo apt-get install llvm-9-tools llvm-9-dev pkg-config wget gzip
             path_extension: /usr/lib/llvm-9/bin
 
     runs-on: ${{ matrix.os }}
@@ -37,12 +37,22 @@ jobs:
         ${{ matrix.install_deps }}
         echo "${{ matrix.path_extension }}" >> $GITHUB_PATH
 
+    - name: Get example files
+      run: |
+        wget http://yann.lecun.com/exdb/mnist/t10k-images-idx3-ubyte.gz
+        wget http://yann.lecun.com/exdb/mnist/t10k-labels-idx1-ubyte.gz
+        gunzip t10k-images-idx3-ubyte.gz t10k-labels-idx1-ubyte.gz
+        mv t10k-images-idx3-ubyte t10k-labels-idx1-ubyte $GITHUB_WORKSPACE/examples/
+
     - name: Cache
       uses: actions/cache@v2
       with:
         path: |
           ~/.stack
           $GITHUB_WORKSPACE/.stack-work
+          $GITHUB_WORKSPACE/examples/t10k-images-idx3-ubyte
+          $GITHUB_WORKSPACE/examples/t10k-labels-idx1-ubyte
+
         key: ${{ runner.os }}-${{ hashFiles('**/*.cabal', 'stack*.yaml') }}
         restore-keys: ${{ runner.os }}-
 
@@ -57,19 +67,6 @@ jobs:
 
     - name: Build
       run: make build
-
-    - name: Download MNist files
-      uses: suisei-cn/actions-download-file@v1
-      id: mnist 
-      with:
-          url: "https://github.com/srush/learns-dex/raw/main/mnist.bin"
-          target: examples/
-    - name: Download MNist labels file
-      uses: suisei-cn/actions-download-file@v1
-      id: labels 
-      with:
-          url: "https://github.com/srush/learns-dex/raw/main/labels.bin"
-          target: examples/
       
     - name: Run tests
       run: make tests
diff --git a/examples/tutorial.dx b/examples/tutorial.dx
index d5c95dd8c..4f26fa5ff 100644
--- a/examples/tutorial.dx
+++ b/examples/tutorial.dx
@@ -292,9 +292,9 @@ def tableAdd' (x : m => n => Float32) (y : m => n => Float32) : m => n => Float3
 
 ' To run this section, move the following binary files to examples:
 
-' `wget https://github.com/srush/learns-dex/raw/main/mnist.bin`
+' `wget http://yann.lecun.com/exdb/mnist/t10k-images-idx3-ubyte.gz; gunzip t10k-images-idx3-ubyte.gz`
 
-' `wget https://github.com/srush/learns-dex/raw/main/labels.bin`
+' `wget http://yann.lecun.com/exdb/mnist/t10k-labels-idx1-ubyte.gz; gunzip t10k-labels-idx1-ubyte.gz`
 
 ' To make some of these concepts for tangible let us consider a real example
   using MNist digits. For this example we will first read in a batch of images
@@ -320,14 +320,16 @@ def pixel (x:Char) : Float32 =
              False -> r
 
 def getIm : Batch => Image =
-    (AsList _ im) = unsafeIO do readFile "examples/mnist.bin"
-    raw = unsafeCastTable Full im
+    -- File is unsigned bytes offset with 16 starting bytes
+    (AsList _ im) = unsafeIO do readFile "examples/t10k-images-idx3-ubyte"
+    raw = unsafeCastTable Full (for i:Batch. im.((ordinal i + 16) @ _))
     for b: Batch i j.
         pixel raw.((ordinal (b, i, j)) @ Full)
 
 def getLabel : Batch => Class =
-    (AsList _ im2) = unsafeIO do readFile "examples/labels.bin"
-    r = unsafeCastTable Batch im2
+    -- File is unsigned bytes offset with 8 starting bytes
+    (AsList _ lab) = unsafeIO do readFile "examples/t10k-labels-idx1-ubyte"
+    r = unsafeCastTable Batch (for i:Batch. lab.((ordinal i + 8) @ _))
     for i. (W8ToI r.i @ Class)
 
 ' Once you have downloaded the files, uncomment these lines to

From 14554a297a8aecabd569180c7128d95d3c079c17 Mon Sep 17 00:00:00 2001
From: Dan Zheng <danielzheng@google.com>
Date: Thu, 21 Jan 2021 08:00:36 -0500
Subject: [PATCH 6/9] Remove extraneous whitespace.

---
 .github/workflows/ci.yaml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml
index f17b32d59..5e7c67715 100644
--- a/.github/workflows/ci.yaml
+++ b/.github/workflows/ci.yaml
@@ -67,6 +67,6 @@ jobs:
 
     - name: Build
       run: make build
-      
+
     - name: Run tests
       run: make tests

From 69710989cae6519c18918838ea961a12c467b43f Mon Sep 17 00:00:00 2001
From: srush <srush.research@gmail.com>
Date: Thu, 21 Jan 2021 08:05:53 -0500
Subject: [PATCH 7/9] update the tests for new mnist files

---
 examples/tutorial.dx | 13 +++++++++----
 1 file changed, 9 insertions(+), 4 deletions(-)

diff --git a/examples/tutorial.dx b/examples/tutorial.dx
index 4f26fa5ff..e4c9c539b 100644
--- a/examples/tutorial.dx
+++ b/examples/tutorial.dx
@@ -322,7 +322,7 @@ def pixel (x:Char) : Float32 =
 def getIm : Batch => Image =
     -- File is unsigned bytes offset with 16 starting bytes
     (AsList _ im) = unsafeIO do readFile "examples/t10k-images-idx3-ubyte"
-    raw = unsafeCastTable Full (for i:Batch. im.((ordinal i + 16) @ _))
+    raw = unsafeCastTable Full (for i:Full. im.((ordinal i + 16) @ _))
     for b: Batch i j.
         pixel raw.((ordinal (b, i, j)) @ Full)
 
@@ -604,11 +604,16 @@ def bincount (inp : a => b) : b => Int =
 ' Plot how many times each pixel value occurs in an image:
 
 hist = bincount $ for (i,j). (FToI (ims.(0 @ _).i.j + 1.0) @Pixels)
+> Ordinal index out of range:256 >= 256
+> Runtime error
 :t hist
-> ((Fin 256) => Int32)
+> Error: variable not in scope: hist
 
 :html showPlot $ yPlot (for i. (IToF hist.i))
-> <html output>
+> Error: variable not in scope: hist
+>
+> :html showPlot $ yPlot (for i. (IToF hist.i))
+>                                      ^^^^
 
 ' Find nearest images in the dataset:
 
@@ -682,7 +687,7 @@ temp = findFives all_ims all_labels
 (AsList nFives fives) = temp
 
 nFives
-> 434
+> 456
 
 ' However we can still utilize the table. For instance
   if we are summing over the hidden dimension, we never

From fe862c41da43601d510d297a31ca7cf9af1e1295 Mon Sep 17 00:00:00 2001
From: srush <srush.research@gmail.com>
Date: Mon, 25 Jan 2021 08:55:27 -0500
Subject: [PATCH 8/9] Fix errors in tutorial

---
 examples/tutorial.dx | 18 +++++++-----------
 1 file changed, 7 insertions(+), 11 deletions(-)

diff --git a/examples/tutorial.dx b/examples/tutorial.dx
index e4c9c539b..0cbe4d308 100644
--- a/examples/tutorial.dx
+++ b/examples/tutorial.dx
@@ -56,7 +56,7 @@ import plot
 ' Once we have an table, we can use it in new comprehensions. For example,
   let's try to add `5` to each table element. In Python, one might write this as:
 
-' `x5 = [[x[i][j] + 5.0 for j in range(width)] for i in range(height)]`
+' ```x5 = [[x[i][j] + 5.0 for j in range(width)] for i in range(height)]```
 
 ' Dex can do something similar. The main superficial difference is the
   table indexing syntax, which uses `table.i` instead of square brackets for
@@ -534,15 +534,16 @@ tableMean (for (i, j). (x.i.j, x.i.j))
 ' If we look in the Prelude, we can see that these interfaces are defined as
  (This will throw error because it mirrors the prelude, but we are just repeating it here.):
 
+' ```
 interface Add a
   add : a -> a -> a
   sub : a -> a -> a
   zero : a
-> Error: variable already defined: Add
 
+' ```
 interface [Add a] VSpace a
   scaleVec : Float -> a -> a
-> Error: variable already defined: VSpace
+```
 
 ' *Interfaces* define *requirements*: the functions needed for a type to
   implement the interface (via an *instance*).
@@ -603,17 +604,12 @@ def bincount (inp : a => b) : b => Int =
 
 ' Plot how many times each pixel value occurs in an image:
 
-hist = bincount $ for (i,j). (FToI (ims.(0 @ _).i.j + 1.0) @Pixels)
-> Ordinal index out of range:256 >= 256
-> Runtime error
+hist = bincount $ for (i,j). (FToI (ims.(0 @ _).i.j) @Pixels)
 :t hist
-> Error: variable not in scope: hist
+> ((Fin 256) => Int32)
 
 :html showPlot $ yPlot (for i. (IToF hist.i))
-> Error: variable not in scope: hist
->
-> :html showPlot $ yPlot (for i. (IToF hist.i))
->                                      ^^^^
+> <html output>
 
 ' Find nearest images in the dataset:
 

From 5e9bab43ba96c4a19bb4279f742d8662584681ab Mon Sep 17 00:00:00 2001
From: srush <srush.research@gmail.com>
Date: Mon, 1 Feb 2021 13:23:06 -0500
Subject: [PATCH 9/9] update to fashion mnist

---
 .github/workflows/ci.yaml |  4 ++--
 examples/tutorial.dx      | 41 +++++++++++++++++++++++----------------
 2 files changed, 26 insertions(+), 19 deletions(-)

diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml
index 5e7c67715..ca00fbee9 100644
--- a/.github/workflows/ci.yaml
+++ b/.github/workflows/ci.yaml
@@ -39,8 +39,8 @@ jobs:
 
     - name: Get example files
       run: |
-        wget http://yann.lecun.com/exdb/mnist/t10k-images-idx3-ubyte.gz
-        wget http://yann.lecun.com/exdb/mnist/t10k-labels-idx1-ubyte.gz
+        wget http://fashion-mnist.s3-website.eu-central-1.amazonaws.com/t10k-images-idx3-ubyte.gz
+        wget http://fashion-mnist.s3-website.eu-central-1.amazonaws.com/t10k-labels-idx1-ubyte.gz
         gunzip t10k-images-idx3-ubyte.gz t10k-labels-idx1-ubyte.gz
         mv t10k-images-idx3-ubyte t10k-labels-idx1-ubyte $GITHUB_WORKSPACE/examples/
 
diff --git a/examples/tutorial.dx b/examples/tutorial.dx
index 0cbe4d308..488e1e4f2 100644
--- a/examples/tutorial.dx
+++ b/examples/tutorial.dx
@@ -288,16 +288,16 @@ def tableAdd' (x : m => n => Float32) (y : m => n => Float32) : m => n => Float3
 
 ' The type system checked for us that the input tables indeed have the same shape.
 
-'## Case Study: MNist
+'## Case Study: Fashion MNist
 
 ' To run this section, move the following binary files to examples:
 
-' `wget http://yann.lecun.com/exdb/mnist/t10k-images-idx3-ubyte.gz; gunzip t10k-images-idx3-ubyte.gz`
+' `wget http://fashion-mnist.s3-website.eu-central-1.amazonaws.com/t10k-images-idx3-ubyte.gz; gunzip t10k-images-idx3-ubyte.gz`
 
-' `wget http://yann.lecun.com/exdb/mnist/t10k-labels-idx1-ubyte.gz; gunzip t10k-labels-idx1-ubyte.gz`
+' `wget http://fashion-mnist.s3-website.eu-central-1.amazonaws.com/t10k-labels-idx1-ubyte.gz; gunzip t10k-labels-idx1-ubyte.gz`
 
 ' To make some of these concepts for tangible let us consider a real example
-  using MNist digits. For this example we will first read in a batch of images
+  using Fashion MNist clothing. For this example we will first read in a batch of images
   each with a fixed size.
 
 Batch = Fin 5000
@@ -352,7 +352,7 @@ im = ims.(0 @ _)
 :html matshow (sum ims)
 > <html output>
 
-' This example overplots three different handwritten images.
+' This example overplots three different pairs of closing.
 
 imscolor = for i. for j. for c:Channels. ims.((ordinal c)@_).i.j
 
@@ -587,9 +587,9 @@ instance [Add v, Add w] Add (v & w)
 instance [VSpace v, VSpace w] VSpace (v & w)
   scaleVec = \s (x, y). (scaleVec s x, scaleVec s y)
 
-'## More MNist
+'## More Fashion MNist
 
-' Now that we has more functions we can revisit some of the MNist examples.
+' Now that we has more functions we can revisit some of the Fashion MNist examples.
 
 ' Function that uses state to produce a histogram:
 
@@ -605,11 +605,16 @@ def bincount (inp : a => b) : b => Int =
 ' Plot how many times each pixel value occurs in an image:
 
 hist = bincount $ for (i,j). (FToI (ims.(0 @ _).i.j) @Pixels)
+> Ordinal index out of range:256 >= 256
+> Runtime error
 :t hist
-> ((Fin 256) => Int32)
+> Error: variable not in scope: hist
 
 :html showPlot $ yPlot (for i. (IToF hist.i))
-> <html output>
+> Error: variable not in scope: hist
+>
+> :html showPlot $ yPlot (for i. (IToF hist.i))
+>                                      ^^^^
 
 ' Find nearest images in the dataset:
 
@@ -668,28 +673,30 @@ temptab
 > [3., 1., 2.]
 
 ' Using this construct we can return to extracting
-  the 5's from the image set.
+  items with label of shoes (label 5) from the image set.
+
+shoes = (5 @ Class)
 
-def findFives (x : a=>b) (y : a=>Class) : List b =
+def findShoes (x : a=>b) (y : a=>Class) : List b =
     concat for i. case (y.i == (5 @ _)) of
             True -> toList [x.i]
             False -> toList []
 
 ' Note though that the type here does not tell us
-  how many 5's there are. The type system cannot know this.
+  how many there are. The type system cannot know this.
   To figure it out we need to unpack the list.
 
-temp = findFives all_ims all_labels
-(AsList nFives fives) = temp
+temp = findShoes all_ims all_labels
+(AsList nShoes allShoes) = temp
 
-nFives
-> 456
+nShoes
+> 485
 
 ' However we can still utilize the table. For instance
   if we are summing over the hidden dimension, we never
   need to know how big it is.
 
-:html matshow (sum fives)
+:html matshow (sum allShoes)
 > <html output>
 
 '## Conclusion