diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index b513e61f0..ca00fbee9 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://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/ + - 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 }}- diff --git a/examples/tutorial.dx b/examples/tutorial.dx index 48a10fb41..488e1e4f2 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 @@ -44,20 +48,22 @@ 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 :html matshow x +> ' 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 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 @@ include "plot.dx" 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 @@ -113,24 +124,34 @@ mean y lets consider how it works. Critically, one cannot simply index an table with an integer. -r = x.3 +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.(3 @ Height) +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.(3 @ 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 +> ' 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.(3 @ Height, 5 @ Width) +: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,26 +270,34 @@ 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. -'## Case Study: MNist +'## Case Study: Fashion MNist ' To run this section, move the following binary files to examples: -' `wget https://github.com/srush/learns-dex/raw/main/mnist.bin` +' `wget http://fashion-mnist.s3-website.eu-central-1.amazonaws.com/t10k-images-idx3-ubyte.gz; gunzip t10k-images-idx3-ubyte.gz` -' `wget https://github.com/srush/learns-dex/raw/main/labels.bin` +' `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 @@ -273,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:Full. 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 @@ -293,20 +342,25 @@ ims = for i : (Fin 100). all_ims.(ordinal i@_) im = ims.(0 @ _) :html matshow im +> :html matshow ims.(1 @ _) +> ' This show the mean pixel value aggregation over all images. :html matshow (sum ims) +> -' 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 :t imscolor +> ((Fin 28) => (Fin 28) => (Fin 3) => Float32) :html imshow (imscolor / 255.0) +> ' This one shows all the images on one channel over the base plot. @@ -316,6 +370,7 @@ imscolor2 = for b. for i. for j. for c:Channels. False -> ims.b.i.j :html imseqshow (imscolor2 / 255.0) +> ' 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 +386,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)) +> im2 : Fin 4 => Fin 4 => Fin 7 => Fin 7 => Float32 = imtile ims.(0@_) :html matshow (sum (sum im2)) +> '## Writing Loops @@ -371,7 +428,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 +444,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 +456,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 +471,7 @@ withState 10 $ \ state. state := 30 state := 10 get state +> 10 ' The element returned pair is the body function's result (`10`) @@ -421,6 +485,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,88 +500,103 @@ 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'` 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] +> 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 + 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 +'## 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: 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 @@ -524,10 +604,17 @@ 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) +hist = bincount $ for (i,j). (FToI (ims.(0 @ _).i.j) @Pixels) +> Ordinal index out of range:256 >= 256 +> Runtime error :t hist +> Error: variable not in scope: hist :html showPlot $ yPlot (for i. (IToF hist.i)) +> Error: variable not in scope: hist +> +> :html showPlot $ yPlot (for i. (IToF hist.i)) +> ^^^^ ' Find nearest images in the dataset: @@ -544,6 +631,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 +> '## Variable Length Lists @@ -562,46 +650,54 @@ 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) -AsList _ $ for i:Height. 0.0 +toList for i:Height. 0.0 +> (AsList 3 [0., 0., 0.]) -:t AsList _ $ for i:Height. 0.0 +:t toList for i:Height. 0.0 +> (List Float32) ' 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 +> (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. Here `mempty` is - synonymous with `AsList _ []`. + 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 -> 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. + 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 +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) +> '## Conclusion diff --git a/makefile b/makefile index c8a18e3f4..22f7b4ec1 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 fft vega-plotting + sgd chol fft tutorial vega-plotting test-names = uexpr-tests adt-tests type-tests eval-tests show-tests \ shadow-tests monad-tests io-tests exception-tests \