From f814a6c0f670e3501c93e5eb0075e7c823486264 Mon Sep 17 00:00:00 2001 From: Sasha Rush Date: Fri, 8 Jan 2021 20:21:26 -0500 Subject: [PATCH 01/14] tutorial --- examples/tutorial.dx | 494 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 494 insertions(+) create mode 100644 examples/tutorial.dx diff --git a/examples/tutorial.dx b/examples/tutorial.dx new file mode 100644 index 000000000..06622370d --- /dev/null +++ b/examples/tutorial.dx @@ -0,0 +1,494 @@ +'# Dex Tutorial + + +'Dex is a functional, statically typed language for array processing. +There are many tools for array processing from high-level libraries +like NumPy / MATLAB to low-level languages like CUDA. Dex gives you +many benefit of the safety and simplicity benefits of high-level array +processing languages, without requiring that you give up low-level +control. + +'## Array Comprehensions + + +' Before getting into the details of the language, let us begin with +the most useful component of dex, the `for` builder. The best analogy +for this construct is list comprehensions in Python. For instance, in +Python we might write a list comprehension like: + +' `x = [[1 for j in range(10)] for i in range(5)]` + +' In Dex, this construct would be written as, + +x = for i:(Fin 5). for j:(Fin 10). 1 + + +' Once we have an variable we can print it `:p` + +:p x + +' More interestingly, we can also see its type with `:t`. This type +signature tells us that `x` is a two-dimensional array, with first +dimension of size 5 and the second of size 10. + +:t x + +' Once we have an array we can use it in new comprehensions. For example, + if say we want to add `5` to each element of the array. In Python, + you might write this as, + +' `y = [[x[i][j] for j in range(10)] for i in range(5)]` + +' Dex can do something similar. The main superficial difference is the + indexing syntax which uses `.` instead of brackets. + +y = for i:(Fin 5). for j:(Fin 10). x.i.j + 5 + +:p y + +' However, we can make this expression nicer. Because `x` has a known type + and `i` and `j` index into that type, Dex can infer the range of the loop. + That means that we can safely remove `Fin` statements and get the same result. + +y' = for i. for j. x.i.j + 5 + + +' We can further reduce this array by applying array functions such as `sum`. + +z = for i. sum x.i + +' This style of using the `for` construct to infer the loop range is + central to what makes Dex powerful. Let's consider another example. + This one produces a list of length 50 in Python. + +' `x = [1 for j in range(10) for i in range(5)]` + +' The analogous array construct in Dex is written in + the following form. This produces a one dimension + array of 50 elements. + +x2 = for (i, j): (Fin 5 & Fin 10). 1 + + +' As before, we can modify this array through another `for` constructor, + which enumerates over each element of `x2`. Or by applying a function. + + +y2 = for i. x2.i + 5 + +:p sum x2 + +' But things start to get interesting when we consider the type of this array. + Unlike the Python example that produces a list of length 50. The + Dex array maintains the index type of its construction. In particular + the type of `x2` remembers the original ranges. + +:t x2 + + +'## Typed Indexing + +' The use of typed indices lets you do some really neat things, but it + also breaks some things in counterintuitive ways. Dex use the `.` + syntax for indexing. Critically though, cannot simply index with a + raw integer. + +r = x.3 + +' Instead you need to cast your integer into the index type of the current + shape. This is done with the `@` operator. (If it helps, you can think of `a.i` + as passing index `i` to array `a` the same way `f x` passes arg `x` to function + `f`.) + +:t x + +row = x.(3 @ Fin 5) + +:t row + +:t row.(5 @ Fin 10) + +' This is bit verbose, but you rarely need to do it in practice. Most of the + time, you index with the `for` construct which is able to infer the right indices. + That's why we didn't have to use any `@` symbols when constructing `y2` above. + +' Similarly you can't use indices as integers as you might be used to. You need to + cast them out explicitly. + + +x4 = for i:(Fin 5). for j:(Fin 10). i + j + + +x4 = for i:(Fin 5). for j:(Fin 10). (ordinal i) + (ordinal j) + + +' As we have seen though, indices do not need to just be integers. We can index with + many different Dex type. For instance `x2` was indexed with a pair of integers (`&` means tuple) + so we need to build a tuple in order to index. + +:t x2 + +:t x2.(3@Fin 5, 5@Fin 10) + +' A lot of algorithms in Dex come down to being able to pack and + unpack these indices. For example, we have seen that it is easy to + sum over one dimension of a 2D array. However, if we have a 1D + array indexed by a pair, we can easily turn it into a 2D array by + constructing it. + +x3 = for i. for j. x2.(i, j) + +:t x3 + +' Again we rely on type inference in order to avoid explicitly giving +the ranges. + +' ## Functions over Arrays + +' One use case of packing and unpacking array indices is that + it allows us to change the order of the axes. This is useful for + applying functions on arrays. + +' For instance, we saw the `sum` function above which sums over an + axes. We can apply `sum` to `x2` to produce the sum over 50 elements. + +:t x2 +:p sum x2 + +' Alternatively we can apply sum over `x3` to produce the sum over rows. + +:t x3 +:p sum x3 + +' How do we sum over the columns? In systems like NumPy you would + do this by passing an axis argument to `sum`. Dex doesn't work this + way. To sum over columns, you need to move columns to the front + of the line. Luckily, you already know how to do this. + + +:t x3 + +trans = for j. for i. x3.i.j + +:t trans + +:p sum trans + +' The `sum` function seems to work independently of the index type of the + array. + +' Let's see how we can do this with our own functions. To define a function in + Dex we use the following syntax (there are other ways to do it, but this + one looks pretty close to Python.) + +def add5 (x:Int32) : Int32 = x + 5 + +:p add5 1 + +:t for i. add5 x2.i + + +' We can also write functions with type variables over their inputs. For instance + we if we want to be able to `Add5` to any array. This function binds the type + variable `n` to the index type of the array. + + +def arrAdd5 (x : n => Int32) : n => Int32 = for i. x.i + 5 + +:t arrAdd5 x2 + + +' But the function types can help you out even more. + For instance, because index types are sized, you + can use type inference to ensure the arguments passed in + are valid. + +' For instance, let's say we want to add two array together. + +:t x +:t y + + +def arrAdd (x : m => n => Int32) (y : m => n => Int32) : m => n => Int32 = + for i. for j. x.i.j + y.i.j + +:t arrAdd x y + +:t arrAdd x (trans y) + +' Here the system type checked for us that they are the same size. + + +'## Writing Loops + +' Dex is a functional language, but when writing mathematical algorithm + it is often convenient to ignore that fact and write imperative code. + +' For example, lets say we now want to actually write the `sum` function + ourselves by accumulating summed values. In Python, We can't do this directly + with list comprehensions, so we would write a loop. + +' `acc = 0` + +' `for i in range(10):` + +' `acc = acc + x[i]` + +' Variables are immutable in Dex, so we cannot do this directly. But we can + write very similar code using the `state` effect. Here's what it looks like + with the corresponding Python code. + + +def arrSum (x : a => Int32) : Int32 = + -- acc = 0 + initAcc = 0 + + -- (ignore for now) + snd $ withState initAcc $ \acc. + + -- for i in range + for i. + -- acc = acc + x[i] + acc := (get acc) + x.i + +:p arrSum x2 + + +' So even though we are functional, the loop looks quite + similar to the imperative style. However there is one + line which is quite new and a bit scary. Let us look + into that line in a bit more detail. + +' First `$`. This symbol is used in Dex the same way it is + used in Haskell, but if you have haven't seen it before it + is a bit strange. It basically takes the place of parens `( )` + when you are too lazy to write them. For example, these two are the same: + +:t arrSum (x2 + x2) + +:t arrSum $ x2 + x2 + +' Next `\`. This symbol is the lambda operator in Dex. It makes a function + that you can use right away, and behaves like `lambda` in python. + Here the function takes an argument `acc` and returns the expression below (a `for` constructor). + +' Finally, the function `snd` is from the prelude. It returns the second of a pair, nothing fancy. + +:p fst (1, 2) +:p snd (1, 2) + + +' That leaves `withState`. This function allows you to introduce imperative variables into the computation. + It takes a intial values `initAcc` and a function of a reference to that value `\acc.` It then returns + a pair of the result of that function and the final value. Here's a simple example + +:p withState 10 $ \ state. + state := 30 + 20 + +' The first element in the pair is the function return (`20`) and the second is the final value of the variable (`30`). + +' Finally this is a good point to talk a bit about some of the other operators in Dex. + Here we see two types of equal signs `=` and `:=`. The first is the `let` operator that makes an + immutable assignment. This one is built into the language and can be used anywhere you want. + + +q = for i:(Fin 10). + -- Bind a temp variable for some reason + temp = (ordinal i) + 10 + for j:(Fin 5). temp + +' The other is `:=` which can only be used inside of a `withState` block. It assigns + a value to a mutable reference. To read that value you need to use the `get` function. + or wait until the `withState` returns. + + +'## Type Classes + +' Our arrSum function is pretty neat. It lets us work with any type index + to compute the sum. However, it annoyingly only works for integers. + +:t arrSum + +' If we apply it to floats we get the following error. + +arrSum for i : (Fin 5). 10.0 + +' We can compare the type of our sum to the built-in Dex `sum`. + +:t sum + +' It has another type variable `v` for the output. It also has the extra annotation + `(Add v) ?=>`. This is a constraint that tells us that `v` can be any type in the + `Add` type class. + +' If we wanted to, we could look in the Dex prelude to see what this looks like. But we can + probably guess what it means. `v` needs to be something where `add` works on it. + We can do that! Let's define our own type class. + +interface MyAdd a:Type where + myAdd : a -> a -> a + myZero : a + +' This tells us that to be in the `MyAdd` type class, a type `a` needs to have + a function `myAdd` and `myZero`. A type can then join the class like this. + + +instance int32MyAdd : MyAdd Int32 where + myAdd = \x y. x + y + myZero = 0 + +instance float32MyAdd : MyAdd Float32 where + myAdd = \x y. (x + y) + myZero = 0.0 + +' Once we have these two definitions, we can revisit our sum function. Here is how we modify + the type. + +def arrSum2 (_:MyAdd v) ?=> (x : a => v) : v = + snd $ withState myZero $ \acc. + for i. + acc := myAdd (get acc) x.i + +arrSum2 for i : (Fin 5). 10 +arrSum2 for i : (Fin 5). 10.0 + +arrSum2 $ for i : (Fin 5). + for j : (Fin 10). 10.0 + +' So it works for ints and it works for floats. But it failed when we tried to + pass in a 2D array. What went wrong? The error tells us that it can't produce + a class dictionary for `MyAdd ((Fin 10) => Float32)`. This makes sense as + we have have not written one. We need to tell the system how to add columns. + +' If we want, we can take the type checker literally and make this instance :). + + +instance specMyAdd : MyAdd ((Fin 10) => Float32) where + myAdd = \x y. for i: (Fin 10). (x.i + y.i) + myZero = for i: (Fin 10). 0.0 + +arrSum2 $ for i : (Fin 5). + for j : (Fin 10). 10.0 + + +' Or we can treat it a more generally and extend to all 1D arrays. + +instance arrMyAdd : (MyAdd v) ?=> MyAdd (a => v) where + myAdd = \x y. for i. (myAdd x.i y.i) + myZero = for i. myZero + +arrSum2 $ for i : (Fin 5). + for j : (Fin 9). 10.0 + + +' This now works for 3D arrays too. + +arrSum2 $ for i : (Fin 5). + for j : (Fin 9). + for k : (Fin 9). 10.0 + + +' ## Prelude Practice + + +' There are a bunch of goodies implemented in the prelude + that are worth knowing. It's good practice just to + infer what these functions do from their type. + +' Here are a couple that come up a lot. + + +' * `select` for filtering + +:t select + +select True 1 2 +select False 1 2 + +' * `zero` for creating empty arrays + +:t zero + +myzero1 : (Fin 20 & Fin 10) => Float32 = zero +myzero2 : (Fin 20) => (Fin 10) => Float32 = zero + +' * `zip` for creating tables of pairs + +:t zip + +:t zip x x +:t for i. zip x.i x.i + + +' * `iota` for create aranges + +:t iota + +:p (iota (Fin 10)) +:p for i. for j. (iota (Fin 4 & Fin 4)).(i, j) + + +' * Random numbers + +:t newKey +:t splitKey +:t randn + +key = newKey 0 +(key1, key2, key3) = splitKey3 key + +:p randn key1 + +' * `randVec` creates a random vector + + +randv = randVec 20 randn key2 +:t randv + +randv2 = randVec 20 randInt key3 +:t randv2 + + +'## Worked Examples: Project Euler + +' To demonstrate Dex in practice, here are some example + functions solving problems on https://projecteuler.net/ + + +def ignore (y:a) (x : Maybe a) : a = + case x of + Just x -> x + Nothing -> y + +instance maybeAdd : (Add v) ?=> Add (Maybe v) where + add = \x y. Just $ ignore zero x + ignore zero y + sub = \x y. Just $ ignore zero x - ignore zero y + zero = Just zero + + +' ### Problem 1: Find the sum of all the multiples of 3 or 5 below 1000. + + + +prob1 = for i : (Fin 1000). + i' = ordinal i + case ((i' `mod` 3) == 0 || (i' `mod` 5) == 0) of + True -> Just i' + False -> Nothing + +:p fromJust $ sum prob1 + +' ### Problem 2: By considering the terms in the Fibonacci sequence whose values do not exceed four million, find the sum of the even-valued terms. + + +... + + +-- def maybeList (x : Maybe a) : List a = +-- case x of +-- Just a -> AsList 1 $ for i : (Fin 1). a +-- Nothing -> mempty + +-- def remMaybe (x: n => Maybe a) : List a = +-- concat $ for i. maybeList x.i From a4299a8b4c6a0ea440b95d25f3124cb8c0f98883 Mon Sep 17 00:00:00 2001 From: Dan Zheng Date: Sat, 9 Jan 2021 00:01:41 -0500 Subject: [PATCH 02/14] Remove extra CSS bottom padding in HTML-rendered Dex. (#445) The bottom padding adds unnecessary empty bottom scrolling, which slightly hurts UX. --- static/style.css | 1 - 1 file changed, 1 deletion(-) diff --git a/static/style.css b/static/style.css index 77a7ce208..f978675d4 100644 --- a/static/style.css +++ b/static/style.css @@ -11,7 +11,6 @@ body { font-family: Helvetica, sans-serif; font-size: 100%; color: #333; - padding-bottom: 500px; } .cell { From 87cf010284ca31b8897bf587a91dcbf956799b83 Mon Sep 17 00:00:00 2001 From: Dan Zheng Date: Sat, 9 Jan 2021 00:02:58 -0500 Subject: [PATCH 03/14] Add LaTeX rendering for HTML-rendered Dex via KaTeX. (#444) This involves only web frontend changes via KaTeX CSS and JS: https://katex.org. I chose KaTeX over MathJax because KaTeX seems more modern, performant, and prettier. --- examples/latex.dx | 41 +++++++++++++++++++++++++++++++++++++++++ examples/pi.dx | 12 ++++++++++++ static/dynamic.js | 14 ++++++++++++++ static/index.html | 5 +++++ 4 files changed, 72 insertions(+) create mode 100644 examples/latex.dx diff --git a/examples/latex.dx b/examples/latex.dx new file mode 100644 index 000000000..fcb0dc07b --- /dev/null +++ b/examples/latex.dx @@ -0,0 +1,41 @@ +'# $\href{https://katex.org/}{\KaTeX}$ rendering examples + +'This document demonstrates $\KaTeX$ rendering in literate Dex programs. + +'## Random examples + +'$$\text{This is a multiline equation:} \\\\ \textbf{A}\textbf{x} = \textbf{b}$$ + +'$$f(\relax{x}) = \int_{-\infty}^\infty \hat{f}(\xi)\,e^{2 \pi i \xi x} \,d\xi$$ + +'## [Environments](https://katex.org/docs/supported.html#environments) + +'$$\begin{matrix} a & b \\\\ c & d \end{matrix}$$ + +'$$\begin{pmatrix} a & b \\\\ c & d \end{pmatrix}$$ + +'$$\begin{bmatrix} a & b \\\\ c & d \end{bmatrix}$$ + +'$$\def\arraystretch{1.5} \begin{array}{c:c:c} a & b & c \\\\ \hline d & e & f \\\\ \hdashline g & h & i \end{array}$$ + +'$$\begin{aligned} a&=b+c \\\\ d+e&=f \end{aligned}$$ + +'$$\begin{alignedat}{2} 10&x+ &3&y = 2 \\\\ 3&x+&13&y = 4 \end{alignedat}$$ + +'$$\begin{gathered} a=b \\\\ e=b+c \end{gathered}$$ + +'$$x = \begin{cases} a &\text{if } b \\\\ c &\text{if } d \end{cases}$$ + +'$$\begin{rcases} a &\text{if } b \\\\ c &\text{if } d \end{rcases} \Rightarrow \dots$$ + +'## [Layout annotation](https://katex.org/docs/supported.html#annotation) + +'$$\overbrace{a+b+c}^{\text{note}}$$ + +'$$\underbrace{a+b+c}_{\text{note}}$$ + +'$$\xcancel{\text{second-order array combinators}}$$ + +'## [Logic and Set Theory](https://katex.org/docs/supported.html#logic-and-set-theory) + +'$$\begin{aligned} \forall \\; & \texttt{\textbackslash forall} & \complement \\; & \texttt{\textbackslash complement} & \therefore \\; & \texttt{\textbackslash therefore} & \emptyset \\; & \texttt{\textbackslash emptyset} \\\\ \exists \\; & \texttt{\textbackslash exists} & \subset \\; & \texttt{\textbackslash subset} & \because \\; & \texttt{\textbackslash because} & \empty \\; & \texttt{\textbackslash empty} \\\\ \exist \\; & \texttt{\textbackslash exist} & \supset \\; & \texttt{\textbackslash supset} & \mapsto \\; & \texttt{\textbackslash mapsto} & \varnothing \\; & \texttt{\textbackslash varnothing} \\\\ \nexists \\; & \texttt{\textbackslash nexists} & \mid \\; & \texttt{\textbackslash mid} & \to \\; & \texttt{\textbackslash to} & \implies \\; & \texttt{\textbackslash implies} \\\\ \in \\; & \texttt{\textbackslash in} & \land \\; & \texttt{\textbackslash land} & \gets \\; & \texttt{\textbackslash gets} & \impliedby \\; & \texttt{\textbackslash impliedby} \\\\ \isin \\; & \texttt{\textbackslash isin} & \lor \\; & \texttt{\textbackslash lor} & \leftrightarrow \\; & \texttt{\textbackslash leftrightarrow} & \iff \\; & \texttt{\textbackslash iff} \\\\ \notin \\; & \texttt{\textbackslash notin} & \ni \\; & \texttt{\textbackslash ni} & \notni \\; & \texttt{\textbackslash notni} & \neg \\; & \texttt{\textbackslash neg} \\\\ \lnot \\; & \texttt{\textbackslash lnot} \\\\ \end{aligned}$$ diff --git a/examples/pi.dx b/examples/pi.dx index c8cc314e7..ef8175b34 100644 --- a/examples/pi.dx +++ b/examples/pi.dx @@ -1,5 +1,17 @@ '# Monte Carlo estimates of pi +'Consider the unit circle centered at the origin. + +'Consider the first quadrant: the unit circle quadrant and its $1 \times 1$ bounding unit square. + +'$$\text{Area of unit circle quadrant: } \\\\ A_{quadrant} = \frac{\pi r^2}{4} = \frac{\pi}{4}$$ + +'$$\text{Area of unit square: } \\\\ A_{square} = 1$$ + +'$$\text{Compute } \pi \text{ via ratios: } \\\\ \frac{A_{quadrant}}{A_{square}} = \frac{\pi}{4}, \\; \pi = 4 \thinspace \frac{A_{quadrant}}{A_{square}} $$ + +'To compute $\pi$, randomly sample points in the first quadrant unit square to estimate the $\frac{A_{quadrant}}{A_{square}}$ ratio. Then, multiply by $4$. + def estimatePiArea (key:Key) : Float = [k1, k2] = splitKey key x = rand k1 diff --git a/static/dynamic.js b/static/dynamic.js index 41f5a8634..6e6efcb13 100644 --- a/static/dynamic.js +++ b/static/dynamic.js @@ -4,6 +4,18 @@ // license that can be found in the LICENSE file or at // https://developers.google.com/open-source/licenses/bsd +var katexOptions = { + delimiters: [ + {left: "$$", right: "$$", display: true}, + {left: "\\[", right: "\\]", display: true}, + {left: "$", right: "$", display: false}, + {left: "\\(", right: "\\)", display: false} + ], + // Enable commands that load resources or change HTML attributes + // (e.g. hyperlinks): https://katex.org/docs/security.html. + trust: true +}; + var cells = {}; function append_contents(key, contents) { @@ -65,4 +77,6 @@ source.onmessage = function(event) { } Object.assign(cells, new_cells); } + // Render LaTeX equations via KaTeX. + renderMathInElement(body, katexOptions); }; diff --git a/static/index.html b/static/index.html index 5084094db..d1774f2ec 100644 --- a/static/index.html +++ b/static/index.html @@ -4,7 +4,12 @@ Dex Output + + + + + From 3b8b9e794c6b8b3944e168f36e05c1e259f2ea9b Mon Sep 17 00:00:00 2001 From: Dan Zheng Date: Sat, 9 Jan 2021 01:07:47 -0500 Subject: [PATCH 04/14] Fix stack build warning for dex executable target. (#446) Remove `-threaded` option to fix warning: ``` Warning: 'ghc-options: -threaded' has no effect for libraries. It should only be used for executables. ``` --- dex.cabal | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/dex.cabal b/dex.cabal index 5a639a818..8c4f5acd7 100644 --- a/dex.cabal +++ b/dex.cabal @@ -85,7 +85,7 @@ executable dex default-language: Haskell2010 hs-source-dirs: src default-extensions: CPP, LambdaCase, BlockArguments - ghc-options: -threaded -optP-Wno-nonportable-include-path + ghc-options: -optP-Wno-nonportable-include-path if flag(optimized) ghc-options: -O3 else From 6932d3e8b3a3aeeb91d5d3239a83c558ec63115d Mon Sep 17 00:00:00 2001 From: Dan Zheng Date: Sat, 9 Jan 2021 03:38:23 -0500 Subject: [PATCH 05/14] Edit tutorial by @srush. - Rebase on top of main branch. - Some code snippets do not yet compile due to syntax changes. This should be straightforward to fix. - Stylistic edits: use consistent terminology and voice. - Remove some second person "you" references. - Use consistent Dex and programming languages terminology and spellings. - Consistently use "array" everywhere: no mentions of "table" - Consistently use "`for` comprehension" - Consistent formatting, punctuation, heading casing (first word uppercase). --- examples/tutorial.dx | 424 +++++++++++++++++++++---------------------- 1 file changed, 208 insertions(+), 216 deletions(-) diff --git a/examples/tutorial.dx b/examples/tutorial.dx index 06622370d..2e73be438 100644 --- a/examples/tutorial.dx +++ b/examples/tutorial.dx @@ -1,104 +1,100 @@ '# Dex Tutorial +' Dex is a functional, statically typed language for array processing. There are + many tools for array processing, from high-level libraries like NumPy and + MATLAB to low-level languages like CUDA. Dex gives you many of the safety and + simplicity benefits of high-level array processing languages, without + requiring that users give up low-level control. -'Dex is a functional, statically typed language for array processing. -There are many tools for array processing from high-level libraries -like NumPy / MATLAB to low-level languages like CUDA. Dex gives you -many benefit of the safety and simplicity benefits of high-level array -processing languages, without requiring that you give up low-level -control. +'## Array comprehensions -'## Array Comprehensions - - -' Before getting into the details of the language, let us begin with -the most useful component of dex, the `for` builder. The best analogy -for this construct is list comprehensions in Python. For instance, in -Python we might write a list comprehension like: +' Before getting into language details, let us begin with the most useful + component of Dex, the `for` builder. The best analogy for this construct is + list comprehensions in Python. For instance, in Python, we might write a + list comprehension like: ' `x = [[1 for j in range(10)] for i in range(5)]` -' In Dex, this construct would be written as, +' In Dex, this construct would be written as: x = for i:(Fin 5). for j:(Fin 10). 1 - -' Once we have an variable we can print it `:p` +' Once we have an variable, we can print it `:p` :p x -' More interestingly, we can also see its type with `:t`. This type -signature tells us that `x` is a two-dimensional array, with first -dimension of size 5 and the second of size 10. +' More interestingly, we can also see its type with `:t`. This type tells us + that `x` is a two-dimensional array, whose first dimension has size 5 and + second dimension has size 10. :t x -' Once we have an array we can use it in new comprehensions. For example, - if say we want to add `5` to each element of the array. In Python, - you might write this as, +' Once we have an array, we can use it in new comprehensions. For example, + let's try to add `5` to each array element. In Python, one might write this as: ' `y = [[x[i][j] for j in range(10)] for i in range(5)]` ' Dex can do something similar. The main superficial difference is the - indexing syntax which uses `.` instead of brackets. + array indexing syntax, which uses `array.i` instead of square brackets for + subscripting. -y = for i:(Fin 5). for j:(Fin 10). x.i.j + 5 +y = for i:(Fin 5). for j:(Fin 10). x.i.j + 5 :p y -' However, we can make this expression nicer. Because `x` has a known type +' However, we can make this expression nicer. Because `x` has a known array type and `i` and `j` index into that type, Dex can infer the range of the loop. - That means that we can safely remove `Fin` statements and get the same result. + That means that we can safely remove the explicit `Fin` type annotations and + get the same result. -y' = for i. for j. x.i.j + 5 +y' = for i. for j. x.i.j + 5 +' We can further reduce this array by applying array reduction functions like + `sum`: -' We can further reduce this array by applying array functions such as `sum`. +z = for i. sum x.i -z = for i. sum x.i +' This style of using `for` to construct type-inferred arrays is central to what + makes Dex powerful. Let's consider another example. This one produces a list of + length 50 in Python. -' This style of using the `for` construct to infer the loop range is - central to what makes Dex powerful. Let's consider another example. - This one produces a list of length 50 in Python. - ' `x = [1 for j in range(10) for i in range(5)]` -' The analogous array construct in Dex is written in - the following form. This produces a one dimension - array of 50 elements. +' The analogous array construct in Dex is written in the following form. It + produces a one-dimensional array of 50 elements. -x2 = for (i, j): (Fin 5 & Fin 10). 1 +x2 = for (i, j): (Fin 5 & Fin 10). 1 +' As before, we can implement "adding 5" to this array using a `for` constructor, + enumerating over each of its elements: -' As before, we can modify this array through another `for` constructor, - which enumerates over each element of `x2`. Or by applying a function. - +y2 = for i. x2.i + 5 -y2 = for i. x2.i + 5 +' And we can apply array functions to the array: :p sum x2 -' But things start to get interesting when we consider the type of this array. - Unlike the Python example that produces a list of length 50. The - Dex array maintains the index type of its construction. In particular - the type of `x2` remembers the original ranges. +' But things start to get interesting when we consider the type of the array. + Unlike the Python example, which produces a list of length 50, the Dex array + Jmaintains the index type of its construction. In particular, the type of the + array remembers the original ranges. :t x2 +'## Typed indexing -'## Typed Indexing - -' The use of typed indices lets you do some really neat things, but it - also breaks some things in counterintuitive ways. Dex use the `.` - syntax for indexing. Critically though, cannot simply index with a - raw integer. +' The use of typed indices lets you do really neat things, but it also breaks + other things in counterintuitive ways. Dex uses the `.` syntax for array + indexing. Critically though, one cannot simply index an array with an integer + literal. r = x.3 -' Instead you need to cast your integer into the index type of the current - shape. This is done with the `@` operator. (If it helps, you can think of `a.i` - as passing index `i` to array `a` the same way `f x` passes arg `x` to function - `f`.) +' Instead, it is necessary to cast the integer into the index type of the + current shape. This type annotation is done with the `@` operator. (If it + helps, you can think of array indexing as function application: `a.i` applies + array `a` with index `i` just like how `f x` applies function `f` with + argument `x`.) :t x @@ -108,63 +104,58 @@ row = x.(3 @ Fin 5) :t row.(5 @ Fin 10) -' This is bit verbose, but you rarely need to do it in practice. Most of the - time, you index with the `for` construct which is able to infer the right indices. +' This explicit annotation is a bit verbose, but it is rarely necessary in + practice. Most of the time, the `for` construct can infer index types. That's why we didn't have to use any `@` symbols when constructing `y2` above. -' Similarly you can't use indices as integers as you might be used to. You need to - cast them out explicitly. - +' Similarly, you cannot use indices as integers as you might be used to. It is + necessary to explicitly annotate index types. x4 = for i:(Fin 5). for j:(Fin 10). i + j +x4 = for i:(Fin 5). for j:(Fin 10). (ordinal i) + (ordinal j) -x4 = for i:(Fin 5). for j:(Fin 10). (ordinal i) + (ordinal j) - - -' As we have seen though, indices do not need to just be integers. We can index with - many different Dex type. For instance `x2` was indexed with a pair of integers (`&` means tuple) - so we need to build a tuple in order to index. +' As we have seen, indices are not limited to only integers. Many different Dex + types are valid index types. For example, we declared array `x2` as having a + pair of integers as its index type (`a & b` means tuple type), so indexing + into `x2` requires creating a tuple value (via `(x, y)`). :t x2 :t x2.(3@Fin 5, 5@Fin 10) -' A lot of algorithms in Dex come down to being able to pack and - unpack these indices. For example, we have seen that it is easy to - sum over one dimension of a 2D array. However, if we have a 1D - array indexed by a pair, we can easily turn it into a 2D array by - constructing it. +' Many algorithms in Dex come down to being able to pack and unpack these + indices. For example, we have seen that it is easy to sum over one dimension + of a 2-D array. However, if we have a 1D array indexed by a pair, we can + easily turn it into a 2D array using two `for` constructors. x3 = for i. for j. x2.(i, j) :t x3 -' Again we rely on type inference in order to avoid explicitly giving -the ranges. +' Again, we rely on type inference in order to avoid explicitly spelling the + ranges. -' ## Functions over Arrays +' ## Defining functions over arrays -' One use case of packing and unpacking array indices is that - it allows us to change the order of the axes. This is useful for - applying functions on arrays. +' One use case of packing and unpacking array indices is that it allows us to + change the order of the axes. This is useful for applying functions on arrays. -' For instance, we saw the `sum` function above which sums over an - axes. We can apply `sum` to `x2` to produce the sum over 50 elements. +' For instance, we saw the `sum` function above which sums over the first axis + of an array. We can apply `sum` to `x2` to produce the sum over 50 elements: :t x2 :p sum x2 -' Alternatively we can apply sum over `x3` to produce the sum over rows. +' Alternatively, we can apply sum over `x3` to produce the sum over rows: :t x3 :p sum x3 -' How do we sum over the columns? In systems like NumPy you would - do this by passing an axis argument to `sum`. Dex doesn't work this - way. To sum over columns, you need to move columns to the front - of the line. Luckily, you already know how to do this. - +' How do we sum over the columns of `x3`? In systems like NumPy, you would do + this by passing an axis argument to `sum`. Dex doesn't work this way. To sum + over columns, you need to move columns to the front of the line. Luckily, we + already know how to do this: using `for` constructors! :t x3 @@ -174,12 +165,11 @@ trans = for j. for i. x3.i.j :p sum trans -' The `sum` function seems to work independently of the index type of the - array. +' The `sum` function works independently of the index type of the array. -' Let's see how we can do this with our own functions. To define a function in - Dex we use the following syntax (there are other ways to do it, but this - one looks pretty close to Python.) +' Let's see how we can define our own array functions. Defining a function in + Dex uses the following syntax. (There are other ways to do it, but this one + looks closest to Python.) def add5 (x:Int32) : Int32 = x + 5 @@ -187,28 +177,25 @@ def add5 (x:Int32) : Int32 = x + 5 :t for i. add5 x2.i - -' We can also write functions with type variables over their inputs. For instance - we if we want to be able to `Add5` to any array. This function binds the type - variable `n` to the index type of the array. - +' 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" + to arrays with _any_ index type. This is possible by declaring an `n => Int32` + array argument type: this declares the type variable `n` as the index type of + the array argument. def arrAdd5 (x : n => Int32) : n => Int32 = for i. x.i + 5 - -:t arrAdd5 x2 +:t arrAdd5 x2 -' But the function types can help you out even more. - For instance, because index types are sized, you - can use type inference to ensure the arguments passed in - are valid. +' But function types can help you out even more. For instance, since index types + are statically known, type checking can ensure that array arguments have valid + dimensions. This is "shape safety". -' For instance, let's say we want to add two array together. +' For instance, let's write a function adding two 2D arrays with the same shape: :t x :t y - def arrAdd (x : m => n => Int32) (y : m => n => Int32) : m => n => Int32 = for i. for j. x.i.j + y.i.j @@ -216,192 +203,207 @@ def arrAdd (x : m => n => Int32) (y : m => n => Int32) : m => n => Int32 = :t arrAdd x (trans y) -' Here the system type checked for us that they are the same size. +' The type system checked for us that input arrays indeed have the same shape. +'## Writing loops -'## Writing Loops +' Dex is a functional language - but when writing mathematical algorithms, + it is often convenient to temporarily put aside immutability and write + imperative code using mutation. -' Dex is a functional language, but when writing mathematical algorithm - it is often convenient to ignore that fact and write imperative code. +' For example, let's say we want to actually implement the `sum` function + ourselves by accumulating summed values in-place. In Python, implementing this + is not directly possible solely via list comprehensions, so we would write a + loop. -' For example, lets say we now want to actually write the `sum` function - ourselves by accumulating summed values. In Python, We can't do this directly - with list comprehensions, so we would write a loop. - ' `acc = 0` ' `for i in range(10):` -' `acc = acc + x[i]` +' `acc = acc + x[i]` -' Variables are immutable in Dex, so we cannot do this directly. But we can - write very similar code using the `state` effect. Here's what it looks like - with the corresponding Python code. - +' In Dex, values are immutable, so we cannot directly perform mutation. But Dex + includes algebraic effects, which are a purely-functional way to modeling + side-effects like mutation. We can write code that looks like mutation using + the `State` effect, which provides getter and setter functionality (via `get` + and `:=` assignment). Here's what it looks like: -def arrSum (x : a => Int32) : Int32 = +def arrSum (x : n => Int32) : Int32 = -- acc = 0 - initAcc = 0 + init = 0 -- (ignore for now) - snd $ withState initAcc $ \acc. + snd $ withState init $ \acc. -- for i in range for i. -- acc = acc + x[i] acc := (get acc) + x.i - -:p arrSum x2 +:p arrSum x2 -' So even though we are functional, the loop looks quite - similar to the imperative style. However there is one - line which is quite new and a bit scary. Let us look - into that line in a bit more detail. +' 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 + line which is quite new and a bit scary. Let us look into that line in a bit + more detail. -' First `$`. This symbol is used in Dex the same way it is - used in Haskell, but if you have haven't seen it before it - is a bit strange. It basically takes the place of parens `( )` - when you are too lazy to write them. For example, these two are the same: +' First: `$`. This symbol is used in Dex just like it is used in Haskell, but + if you haven't seen it before, it seems a bit strange. `$` is the function + application operator: it basically replaces of expression-grouping parentheses + `(f x)` when it is inconvenient to write them. For example, the following two + expressions are identical: :t arrSum (x2 + x2) :t arrSum $ x2 + x2 -' Next `\`. This symbol is the lambda operator in Dex. It makes a function - that you can use right away, and behaves like `lambda` in python. - Here the function takes an argument `acc` and returns the expression below (a `for` constructor). +' 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 + (i.e. closure). In `arrSum` above: the lambda takes an argument named `acc` + and returns the body, which is the expression following the `.` (a `for` + constructor in this case). -' Finally, the function `snd` is from the prelude. It returns the second of a pair, nothing fancy. +' Finally, the function `snd` is from the Dex Prelude. It simply returns the + second element of a pair - there is also `fst` for extracting the first + element. :p fst (1, 2) :p snd (1, 2) - -' That leaves `withState`. This function allows you to introduce imperative variables into the computation. - It takes a intial values `initAcc` and a function of a reference to that value `\acc.` It then returns - a pair of the result of that function and the final value. Here's a simple example +' That leaves: `withState`. This function uses the `State` effect, enabling us + to introduce imperative variables into the computation. + `withState` takes an initial value `init` and a body function taking a + "mutable value" reference (`acc` here), and returns a pair of the body + function's result and the final value. Here's a simple example: :p withState 10 $ \ state. state := 30 20 -' The first element in the pair is the function return (`20`) and the second is the final value of the variable (`30`). - -' Finally this is a good point to talk a bit about some of the other operators in Dex. - Here we see two types of equal signs `=` and `:=`. The first is the `let` operator that makes an - immutable assignment. This one is built into the language and can be used anywhere you want. +' The first element of the returned pair is the body function's result (`20`). + The second element is the final value of the variable (`30`). +' Finally: this is a good point to talk a bit about some other operators in Dex. + In the examples above, we see two types of equal sign operators: `=` and `:=`. + The first is the `let` operator that creates an immutable assignment (a + "let-binding"). This one is built into the language and can be used anywhere. q = for i:(Fin 10). - -- Bind a temp variable for some reason + -- Bind a temporary variable `temp`, as an example. temp = (ordinal i) + 10 for j:(Fin 5). temp - -' The other is `:=` which can only be used inside of a `withState` block. It assigns - a value to a mutable reference. To read that value you need to use the `get` function. - or wait until the `withState` returns. +' 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 + `withState`. `ref := x` assigns the value `x` to the mutable reference `ref`. + Reading the value in `ref` is possible via the `get` function. or via using + the final result returned by `withState`. -'## Type Classes +'## Typeclasses -' Our arrSum function is pretty neat. It lets us work with any type index - to compute the sum. However, it annoyingly only works for integers. +' Our `arrSum` function is pretty neat. It lets us work with arrays with any + index type and computes the sum. However, `arrSum` explicitly takes only + integer arrays (of type `n => Int32`). :t arrSum -' If we apply it to floats we get the following error. +' If we try to apply `arrSum` to float arrays, we get the following error: arrSum for i : (Fin 5). 10.0 -' We can compare the type of our sum to the built-in Dex `sum`. +' We can compare the type of our `arrSum` function to the `sum` function found + in the Dex Prelude. :t sum -' It has another type variable `v` for the output. It also has the extra annotation - `(Add v) ?=>`. This is a constraint that tells us that `v` can be any type in the - `Add` type class. +' The Prelude-defined `sum` function also has an additional argument, spelled + like: `(Add v) ?=> ...`. This is a constraint telling us that the function + expects an `Add v` typeclass instance, where `v` is any type that implements + the `Add` typeclass. -' If we wanted to, we could look in the Dex prelude to see what this looks like. But we can - probably guess what it means. `v` needs to be something where `add` works on it. - We can do that! Let's define our own type class. +' We could look in the Dex Prelude to see exactly how `sum` is defined and what + `Add v` means. But we can guess what the `Add v` constraint means: `v` needs + to be a type that works with `add`. We can do that! Let's define our own + typeclass. interface MyAdd a:Type where myAdd : a -> a -> a myZero : a -' This tells us that to be in the `MyAdd` type class, a type `a` needs to have - a function `myAdd` and `myZero`. A type can then join the class like this. - +' This declares a typeclass (i.e. interface or trait) called `MyAdd` with some + typeclass methods (interface requirements). To implement the `MyAdd` + typeclass, a type `a` needs to define functions `myAdd` and `myZero` in a + "typeclass instance", like so: instance int32MyAdd : MyAdd Int32 where myAdd = \x y. x + y myZero = 0 instance float32MyAdd : MyAdd Float32 where - myAdd = \x y. (x + y) + myAdd = \x y. (x + y) myZero = 0.0 -' Once we have these two definitions, we can revisit our sum function. Here is how we modify - the type. +' Once we have these two instance definitions (`MyAdd Int32` and + `MyAdd Float32`), we can revisit our array sum function and add a typeclass + constraint: -def arrSum2 (_:MyAdd v) ?=> (x : a => v) : v = +def arrSumGeneric (_:MyAdd v) ?=> (x : a => v) : v = snd $ withState myZero $ \acc. for i. acc := myAdd (get acc) x.i -arrSum2 for i : (Fin 5). 10 -arrSum2 for i : (Fin 5). 10.0 +arrSumGeneric for i : (Fin 5). 10 +arrSumGeneric for i : (Fin 5). 10.0 -arrSum2 $ for i : (Fin 5). - for j : (Fin 10). 10.0 +arrSumGeneric $ for i : (Fin 5). + for j : (Fin 10). 10.0 -' So it works for ints and it works for floats. But it failed when we tried to - pass in a 2D array. What went wrong? The error tells us that it can't produce - a class dictionary for `MyAdd ((Fin 10) => Float32)`. This makes sense as - we have have not written one. We need to tell the system how to add columns. - -' If we want, we can take the type checker literally and make this instance :). +' This sum function works for any type that implements `MyAdd`, like `Int32` and + `Float32`. But it failed when we tried to pass in a 2D array. What went wrong? + The error tells us that the function could not find a `MyAdd` instance for + `MyAdd ((Fin 10) => Float32)`. This makes sense because we have have not + written one. We need to tell the system "how to add array columns". +' One option is to directly satisfy the type checker and provide a specific + `MyAdd ((Fin 10) => Float32)` instance: instance specMyAdd : MyAdd ((Fin 10) => Float32) where - myAdd = \x y. for i: (Fin 10). (x.i + y.i) + myAdd = \x y. for i: (Fin 10). (x.i + y.i) myZero = for i: (Fin 10). 0.0 -arrSum2 $ for i : (Fin 5). - for j : (Fin 10). 10.0 - +arrSumGeneric $ for i : (Fin 5). + for j : (Fin 10). 10.0 -' Or we can treat it a more generally and extend to all 1D arrays. +' To be more general, we can instead define a `MyAdd` instance for all array + types. This instance requires that the array element type `v` also has an + `MyAdd` instance; this requirement is represented as a `(MyAdd v) ?=> ...` + constraint. instance arrMyAdd : (MyAdd v) ?=> MyAdd (a => v) where - myAdd = \x y. for i. (myAdd x.i y.i) + myAdd = \x y. for i. (myAdd x.i y.i) myZero = for i. myZero -arrSum2 $ for i : (Fin 5). - for j : (Fin 9). 10.0 +arrSumGeneric $ for i : (Fin 5). + for j : (Fin 9). 10.0 +' This instance not only works for 2D arrays, but also 3D and higher-dimensional + arrays: -' This now works for 3D arrays too. - -arrSum2 $ for i : (Fin 5). +arrSumGeneric $ for i : (Fin 5). for j : (Fin 9). for k : (Fin 9). 10.0 - - -' ## Prelude Practice +' ## Learn the Prelude -' There are a bunch of goodies implemented in the prelude - that are worth knowing. It's good practice just to - infer what these functions do from their type. - -' Here are a couple that come up a lot. +' The Prelude contains many handy functions. Since Dex types contain so much + information, it is possible to infer what many of these functions do just by + reading and understanding their type. +' Here are a few used, commonly-used Prelude functions. ' * `select` for filtering -:t select +:t select select True 1 2 select False 1 2 @@ -413,23 +415,21 @@ select False 1 2 myzero1 : (Fin 20 & Fin 10) => Float32 = zero myzero2 : (Fin 20) => (Fin 10) => Float32 = zero -' * `zip` for creating tables of pairs +' * `zip` for creating arrays of pairs :t zip :t zip x x :t for i. zip x.i x.i - -' * `iota` for create aranges +' * `iota` for creating "aranges" :t iota :p (iota (Fin 10)) :p for i. for j. (iota (Fin 4 & Fin 4)).(i, j) - -' * Random numbers +' * Pseudorandom number generation :t newKey :t splitKey @@ -440,55 +440,47 @@ key = newKey 0 :p randn key1 -' * `randVec` creates a random vector +' * `randVec` for creating a vector of random numbers - -randv = randVec 20 randn key2 +randv = randVec 20 randn key2 :t randv randv2 = randVec 20 randInt key3 :t randv2 +'## Worked examples: Project Euler -'## Worked Examples: Project Euler - -' To demonstrate Dex in practice, here are some example - functions solving problems on https://projecteuler.net/ +' To demonstrate Dex in practice, below are some examples of solving problems + from [Project Euler](https://projecteuler.net). - def ignore (y:a) (x : Maybe a) : a = case x of Just x -> x Nothing -> y - + instance maybeAdd : (Add v) ?=> Add (Maybe v) where add = \x y. Just $ ignore zero x + ignore zero y sub = \x y. Just $ ignore zero x - ignore zero y zero = Just zero - ' ### Problem 1: Find the sum of all the multiples of 3 or 5 below 1000. - - prob1 = for i : (Fin 1000). i' = ordinal i case ((i' `mod` 3) == 0 || (i' `mod` 5) == 0) of True -> Just i' False -> Nothing - + :p fromJust $ sum prob1 ' ### Problem 2: By considering the terms in the Fibonacci sequence whose values do not exceed four million, find the sum of the even-valued terms. - ... - -- def maybeList (x : Maybe a) : List a = -- case x of -- Just a -> AsList 1 $ for i : (Fin 1). a -- Nothing -> mempty -- def remMaybe (x: n => Maybe a) : List a = --- concat $ for i. maybeList x.i +-- concat $ for i. maybeList x.i \ No newline at end of file From 2c99e4812d3f5cc1958bb014f0ab8c98cce31c7f Mon Sep 17 00:00:00 2001 From: Dan Zheng Date: Sat, 9 Jan 2021 09:25:58 -0500 Subject: [PATCH 06/14] Consistently spell "n-D" as "nD". --- examples/tutorial.dx | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/examples/tutorial.dx b/examples/tutorial.dx index 2e73be438..2c5b54042 100644 --- a/examples/tutorial.dx +++ b/examples/tutorial.dx @@ -126,7 +126,7 @@ x4 = for i:(Fin 5). for j:(Fin 10). (ordinal i) + (ordinal j) ' Many algorithms in Dex come down to being able to pack and unpack these indices. For example, we have seen that it is easy to sum over one dimension - of a 2-D array. However, if we have a 1D array indexed by a pair, we can + of a 2D array. However, if we have a 1D array indexed by a pair, we can easily turn it into a 2D array using two `for` constructors. x3 = for i. for j. x2.(i, j) @@ -483,4 +483,4 @@ prob1 = for i : (Fin 1000). -- Nothing -> mempty -- def remMaybe (x: n => Maybe a) : List a = --- concat $ for i. maybeList x.i \ No newline at end of file +-- concat $ for i. maybeList x.i From e9368b1cc668f347c981f636d9b8f1887bb534bf Mon Sep 17 00:00:00 2001 From: Sasha Rush Date: Sat, 9 Jan 2021 10:51:53 -0500 Subject: [PATCH 07/14] Update tutorial to use the latest syntax for typeclasses --- examples/tutorial.dx | 49 +++++++++++++++++++++----------------------- 1 file changed, 23 insertions(+), 26 deletions(-) diff --git a/examples/tutorial.dx b/examples/tutorial.dx index 2c5b54042..ef2f1dd2c 100644 --- a/examples/tutorial.dx +++ b/examples/tutorial.dx @@ -6,6 +6,10 @@ simplicity benefits of high-level array processing languages, without requiring that users give up low-level control. + +include "plot.dx" + + '## Array comprehensions ' Before getting into language details, let us begin with the most useful @@ -222,6 +226,8 @@ def arrAdd (x : m => n => Int32) (y : m => n => Int32) : m => n => Int32 = ' `acc = acc + x[i]` +' `return acc` + ' In Dex, values are immutable, so we cannot directly perform mutation. But Dex includes algebraic effects, which are a purely-functional way to modeling side-effects like mutation. We can write code that looks like mutation using @@ -233,13 +239,14 @@ def arrSum (x : n => Int32) : Int32 = init = 0 -- (ignore for now) - snd $ withState init $ \acc. - + withState init $ \acc. -- for i in range for i. -- acc = acc + x[i] acc := (get acc) + x.i - + -- return acc + get acc + :p arrSum x2 ' So, even though Dex is a functional language, it is possible to write loops @@ -263,12 +270,6 @@ def arrSum (x : n => Int32) : Int32 = and returns the body, which is the expression following the `.` (a `for` constructor in this case). -' Finally, the function `snd` is from the Dex Prelude. It simply returns the - second element of a pair - there is also `fst` for extracting the first - element. - -:p fst (1, 2) -:p snd (1, 2) ' That leaves: `withState`. This function uses the `State` effect, enabling us to introduce imperative variables into the computation. @@ -278,7 +279,7 @@ def arrSum (x : n => Int32) : Int32 = :p withState 10 $ \ state. state := 30 - 20 + get state ' The first element of the returned pair is the body function's result (`20`). The second element is the final value of the variable (`30`). @@ -326,7 +327,7 @@ arrSum for i : (Fin 5). 10.0 to be a type that works with `add`. We can do that! Let's define our own typeclass. -interface MyAdd a:Type where +interface MyAdd a:Type myAdd : a -> a -> a myZero : a @@ -335,11 +336,11 @@ interface MyAdd a:Type where typeclass, a type `a` needs to define functions `myAdd` and `myZero` in a "typeclass instance", like so: -instance int32MyAdd : MyAdd Int32 where +instance MyAdd Int32 myAdd = \x y. x + y myZero = 0 -instance float32MyAdd : MyAdd Float32 where +instance MyAdd Float32 myAdd = \x y. (x + y) myZero = 0.0 @@ -347,10 +348,11 @@ instance float32MyAdd : MyAdd Float32 where `MyAdd Float32`), we can revisit our array sum function and add a typeclass constraint: -def arrSumGeneric (_:MyAdd v) ?=> (x : a => v) : v = - snd $ withState myZero $ \acc. +def arrSumGeneric [MyAdd v] (x : a => v) : v = + withState myZero $ \acc. for i. acc := myAdd (get acc) x.i + get acc arrSumGeneric for i : (Fin 5). 10 arrSumGeneric for i : (Fin 5). 10.0 @@ -367,7 +369,7 @@ arrSumGeneric $ for i : (Fin 5). ' One option is to directly satisfy the type checker and provide a specific `MyAdd ((Fin 10) => Float32)` instance: -instance specMyAdd : MyAdd ((Fin 10) => Float32) where +instance MyAdd ((Fin 10) => Float32) myAdd = \x y. for i: (Fin 10). (x.i + y.i) myZero = for i: (Fin 10). 0.0 @@ -379,7 +381,7 @@ arrSumGeneric $ for i : (Fin 5). `MyAdd` instance; this requirement is represented as a `(MyAdd v) ?=> ...` constraint. -instance arrMyAdd : (MyAdd v) ?=> MyAdd (a => v) where +instance [MyAdd v] MyAdd (a => v) myAdd = \x y. for i. (myAdd x.i y.i) myZero = for i. myZero @@ -436,7 +438,8 @@ myzero2 : (Fin 20) => (Fin 10) => Float32 = zero :t randn key = newKey 0 -(key1, key2, key3) = splitKey3 key +[key1, key2, key3] = splitKey key + :p randn key1 @@ -458,7 +461,7 @@ def ignore (y:a) (x : Maybe a) : a = Just x -> x Nothing -> y -instance maybeAdd : (Add v) ?=> Add (Maybe v) where +instance [Add v] Add (Maybe v) add = \x y. Just $ ignore zero x + ignore zero y sub = \x y. Just $ ignore zero x - ignore zero y zero = Just zero @@ -475,12 +478,6 @@ prob1 = for i : (Fin 1000). ' ### Problem 2: By considering the terms in the Fibonacci sequence whose values do not exceed four million, find the sum of the even-valued terms. -... --- def maybeList (x : Maybe a) : List a = --- case x of --- Just a -> AsList 1 $ for i : (Fin 1). a --- Nothing -> mempty --- def remMaybe (x: n => Maybe a) : List a = --- concat $ for i. maybeList x.i +' TODO: Finish this part with some more examples \ No newline at end of file From 5576121809ffde47a69a385c407caf2628eda351 Mon Sep 17 00:00:00 2001 From: Sasha Rush Date: Sat, 9 Jan 2021 19:53:14 -0500 Subject: [PATCH 08/14] update with mnist --- examples/cmn | Bin 0 -> 78400 bytes examples/tutorial.dx | 487 +++++++++++++++++++++++-------------------- 2 files changed, 258 insertions(+), 229 deletions(-) create mode 100644 examples/cmn diff --git a/examples/cmn b/examples/cmn new file mode 100644 index 0000000000000000000000000000000000000000..7fe2667ff1e32ab58ac6c4869fa648a603752c6f GIT binary patch literal 78400 zcmeHw2V50L*Y`vP5yXOE0~C9Sy+n;sv6qq@gZ4Ap*9=b6QQx_G4Q!jXGu=;OgKK$ek>DjYsH4TKE9?MwRiOdu&Tk&__ zG!El%2lVMi9z#Vw*@y=U_zG(&KAX=7bU2GU7-6VVO4QczpBTVBk};lE#sIASC&ues z4ZvbUB>a~FhEO)n_7sA3=AOj(hA1V~*2F;0<(%NvN_#z}dHVO)98{{!J&J_&;0!wL zlkdZY?uA&TCPC3uCw;yHiy*WJfV&HQi}6Sv=U>f%^3~@gB>X0lZny3&fee1YW1Ida zgruw+X~#h&Hj<>Py{eVt0AQ@ZD+`PG$bQbVueN6^dU$3|35tygq37o3twevl~~ zgrZH+fsm2Hl=p?K5A-ugHXDIF`k%`IA0PT?n>=}o3P3>)^Q2sG!9G45CUZSGHu3~f z0h=FDxNCK|Hk|XCShLwc*h(RQ0h=C@==RI*nKE@FOJwarBf*~N9 znS5lFNYZ5R@dU2ycr65RF!=2`RtKyM+mq!9W8|02N1qdEw=rsB^8SRf$}UYf{!0ffqLy^ilM z8!t*Xh}%{cbPz;l@_7Gx4&-yHvuIJeDdjs(rRdNd@I2!;kFHhXuz3`DeOXkM2fV|X z<6GC}R44;pome3N%*|N%D9PdjaE>S_GnQ#&5)Hur9_A94UD42J6pp)hZ-)384Wjvi z&$bdN=bPGT<}Hl5mX<18<}to**oheP4%?`L-1VL@RyNug^ToFe!}}Vm4L~lm{|v_W zF=T-_rVeWe&YoLP2-b$uHOq%Dk*P4n4t5l(A&(;j4-iAZeLuG6J$h;NjKHNBZ?rW4 zKYf9*y8(t;5HiRJ`vT)5|1@^a*ygm^_^r4LPxA~5tB88b?;SDWEKx1z;hPH;>Okek0KVj zaig&U(LC0FEeGnh{&wdqfr?|B)sN}@ddFg)??3RI-l#v8cheX61-?6#g;OFQ&8%En zH=tf%?PAw*IC)P;!62st#+!?HiC+c4R_LEDYgBCZWMceqn86D+GAkRj+WudvSx zoM?XVH9+|`GEwpxUZdeE-lxmuYm)@ri^ItIvSpo0jZDN_`6_NbhHSov zcO~i31aVWTrl+Sshqsc)`G<3$O#KZJngiAmr6-M@|iuoHJ+6 z#7?8RvY(gC@6roiN24?@|S6T6y;f=n$!-}T6~Uy&>@mIw=B3;f0LB*47d;`&=n`~jaKIs z+4N0Hz9gJhZ0ZS4{I)ZJd~9T~;E)MyMw|1%<+y~U7ZIBp@p)40xC9vd$2DZZPlACz z{uRa9l^4YTN@^)9)MRf)70}9D(3yRXWMPMn4>G~t*-mU&3O!`}Su7i@-%q5Y zikIdqi(yRjq+75F<6u?6eEsA$+`G=9sc;{Ta&<`g>&pF$7{pa&(7Cun@9iGOULN^R zvJT0!9ZbM#ovbuHGKNW_>5gSi2(mNzoICiZeFq*tI+ z{?Ruxym_|F8G(u6K-VR_NZj&9sK_>AO4z}*^kkFHb;mEbjdQP#<%1kT!?LS9?pg#F z%@N03WqFrJv$*My3v&Ca@t||KIcM`CIkcC+luXu-9E1vQ$bbRwFzoHQmPqCe=xH% z`)Zo?E^y5=h(rRG?k<>IUeM)4=q64rX>|8Km9Vc7h9={fx<+8pRrr((DN}||d6jXSH+P(K1~Qhz#zJFAcCW%& zYi5pG!(|sW> zxdHC1mP%JKk>jeLUYBXQ^TopPF)c>ItWTHi3A{s#t%*-rrIzk6%lCyALz7~0(m;9K zw{A2(&b%#6&cg!v^XJcBc&T(Fbei@H=%frZJX87$vdnegU-u6y;Gd(>FcYm_`xstTy-iw1kATpADkvda zAcVYNv{ZKC8Ycm?(B|4T&^Z`fj1sfWKV@aVdaf+5X zPeftS`*5*WZ|>glVSm`1!otP~Dp;aKiG?|YOS>boYppcTxvoX2WwTEyP1~sLjGo{j+Z$yw?_(Js(m zsb>~5UtD)W;+B3h_jwj!x(^_b|64$1r|(%Py7{a9`iziWHM!n{0^1cXY=D@9{zxy* z-rnAxkoMu;cknn}9(X6G(lO9v@5k9v;ym5-=yVwV4B0XOM&+Ju`9j}5@BU6&R1L=W zmOYxGjGAa{4wa-ZN|q7S(`7D5Z~AFub>6ZUq_=%^91T(CqLkWGL+iYyE=ljyM^Oh* zqQq56>d0};jFA|d_~x|&<{K{IOhGGAM)QrhCLQxMTj4IfvZPRMsHj;V<#isHA-&Oe zs?f;PQ)U|z(xrpiw+wYjm$t5~QKJSeC#FkMpf;>(&*0vHySi=b)-#f%??ViD^X|n6J zYO+|9B!aJh-;!lhy3s4??Etn$F$+GIq*t?NH`9&Gs5VY3(Kx}qw;-@^HMq-?bY2yv z*M5^Vb~>In4bzYz5!#}?Hja>6{fhQUDc+hM+c3OK)1@x*bLK_Mki!BgN?EIwdQRP9 z$u&J@yELMxO_(lyMiQ`Bq){aPjD-K*6ZyiWOt3qm8&jmAg5&^!e^EK6j)1n$JCsx%Gv`7v6i9dOS5X7q2g?wWtJDV9+MW(GC6B)n(R* zM;Fj%R32F6usSAk@7Tz$UC|(R0JUI)bYgI10IHXPi69(m zy#%cBA-TKCav=euK_osL@CNT?g0hmmPQDqgQ>?VLorSKKpx@By)65xBd z%`)^=KQptw9>a;pMp8~y?{pk&4VlN969VjX^>eRJSqegvm=$3?!eX5IzhVXuYbG?W2%Mj( zuYhZ2Mf(|J28UV53VrEu7tQ+iZ6*lP-4yKwM^JzhoKFEs2n+1%?geS&RQsw&dA#rB z4&?Q|^t>0-jRon`EuY?@XQ`C?du#^sXL`7sLun>D|3o>gq*=7cWM6u8M__cc@NT(# z!PycZVCnSZGFY%qph%DL4~)AF-R7f~&=v zYyevKL|u1Ou)zh`aL1ItX7vi76~Wn3z^;H@YojeTEn&8aljHal=4sj6UR+seBI7wv zs#{d3r?|{jf2MO-!ba*~=O@-4eOoI1WDSvLKqon%`e~cP)cZSWVx7+l-$q= zM6+^I4HrM5%Xqq@k!BezEoZQ*lU2qBZVh%H+*JX~68ya?X1?~3;+j=O&6*8M!}s+A zB2b;CVJRV$PBEnSVANoCXxZ7b$$(uknqc8H@)(*NC}2Bz3isgWuT?8QYQFv%^aRgn zWM%JBa;iYt%e0diz`RSPH%l>49Q*sYy1FvA&}Ius|BAJw&~5&B^_Qm@DhUyIn{cOZ zaa$g*lp5}BUzAsUHr=-jT*p7Rb)Q}mtX&z2u4vcFvEtrsg`rv>n>Hi1KMnam3dN}#M z^YZelWy2WcjN~zx9DuW~d>EEW%BNb1!C<*rZc-(+SE}WS#D|0d<_RZ=32h3GH8UFy zrfLT6J?D7Axs&fvghRfJtwJIU!jn(!GS*a*Z=mb>KC=J@3-pvYf>|FPgnLI}9}z|) zVhVJ24Q{huKbFNf}wjQ*&D+?*9`+{GULbVz;xETBdAQdeq*`_mR)|8Wjxq_Z4YnD%;}KU+6Z%tjWUAJ8hXlC`7d1s z0xeDVbL5fEljT^{;Ud8y-`B2P`{%chSgiG%fCfr=+#R!+mELHK+1!b<$}v8FqI5v4 z>;hwy2?D#NxxcYBU{MT>&rjS3hGy_*uG!ta`1A2lINhd()t1HA;6A}8ephQV3p>wa z&Vd53o*P^~K0_)Mm_>VD7;odSx;aN=RY$vkf z2RKJUKQ?dCb%V3Y)>I$**vZ#6&v5Gb(VfAC;WRyjP_<)n z7DE~`R_L@SVcQ%A3c&e$a8MrOznKFrl`B`)H-}Y&rKdcB*6YdDDs8zIFOF8pEnBk1 z!ZUk{o}7Zt5^}M7-MadAG~lbr1k}piT`;tfe`zjmh1fz+HtDdKkU!W^%=AE5aI&qY zs0ILmc^AS>Bzl(MO{d!S&DR~y3TbaP#9s#DoG-Q9UoL5=9HQ&Rhdr?-skuZ}X(Ul9 zc{SBpVU#^ZUhBG4P45%(d{^Uo;GU68>mCYO+`i*)X-XcGC_z2^Y2#gw2#MJ@TpO6x z?_8-;UVqt|9si>~`|2HfS8qAEdUa+n79!@~D44 z2a2~@0u!A0@7cWRhA$=QWfF|$#q!uTNm}Glt9|?StvIaEd1(PxWtgRoOJ|HAWWtL} zmoCjbWoA7(rYPa0ulY9*HO5l>$p^45S~PC8tzQM?Qf8sFm5Zgy7$sd13{1&r{y=Q_ zB9)e;+NufmI$nye!1B!Wr}2`m#?gvB!MBAKC%j@?@zI)EQLDdPfD~r{)qg3yFzClY zG%mPXjp%$&7XMgG$M`sj{I<4A7m`W7L#;LI&!?X^E^XdE3Sj_I{2ZY>P z*uu3GVmk}P1EBIhHbU@H6zCsJF7*`OCEFW>JgRQThNIBGq{62An~TLybxpg^mfj+F z^s0{5=gw|O!b{!r6cjSl5=^B8;$tDe)1AcMm}L&9QbPI&EtYSOKzt;1`@?XbzdNOSuCAJeK z+EjvOOyri6`uG?2PS3toy=eFDzirvl!Q25gOB8>E6PdQPMfVauV3`%LFcr@*lGc-9 zSxDI9opVkYLl9{)B`lL%Fl>ob4ka@zhFDKIvYTb8bkoCRwd&VhyAODV%xQR!XOR zeSPO|l|_nZ6>YwJC2giHf`aa&4j(>juf>W|ahcF#06m||LhJ)#j(BN0At>$&tUnTZ zH5gEYJj&^O4F~WFGRNf>xn%%#f`w^*D_0H`wUdv_ z6%oO=1OZM2EaS@6T>QJW<*x=Y2tEN+12%ys>rbYa;lU>I8}+~jIaSHoe{Wm2jk?U@Y+seo8Wj z2IOEYFLH`dO01W*qc=I5C7gEf?^}>Q%r^@DxQ+@n3>JC#yX+$P+PnZ>~ zn31(a98HjE`H~zmG+X`~LAhhbPZGlr(fs#d`-E7vYpoF~ zoqSYq|4>8eZOGa%>lC6jg5djdOIq5N_uLDe@P8U{0={?b>+9&~NSh}Px@NeWazF!A zw{a_1u6%u63$~F`r(KFOH;E+a4{cGhSAw~r%DsCJyLRo3l(bp7_q1$}`xFk?%3OT%NncuRQ^%|z)^(N#+RgNn&N<`zA1`vGg zIqFlf7D9e_j}e66jLU0t+}+(p0`@`5+)3cDW*!{w*tF?hI7$YFXJRgi-rj<4U;8aP zf=S|`L!7Re;dLg9gzzQ08Etc$1ZndOp-cNMa{+J$to|9khR>UYt45Rc`ZC|~Cb=e0 z@62k?4g|yon70&E<#5L4BiNx-B?qUpezSjJNRNlObu44 z=)7h%YtDX1Ue4zW>?;JmZgKZoFCIZC@Zz>9_3|EBHaq`c(Km#qe&(I#1Z2>bkY`L3x3+eLg+m!U~|i+ z+1+@1a5Pg2T^wp6cWUWXWNP-JMT>rDeMEb_3nTS8PGLA!($7fG!FdwN7S$_`j-Q@| z5?QwrT(-CS!Gq`*Fx^j9J6Y|UeVfhs_(-rYiaX>2d>2Iep4-eI^Kr(B0f_o_HegoVj zF>7h5d}cZQ1rF%juIE^(b_Bl}VkLFHiqk?Ny!HCViABPu{FEnnvV~+ljtP8{RhfpF z#@Jt?ErYV6&1#ZfRW+f%+Wdes`{`Mf8Zvvx5P#U__6H9kIv`*o;li{pqOZ{l^Dr)> z>p16VYwl$@=eUS(FR3+X(w*4f@+f*MO!F zE7=C3o4!*}n+@Fc1e9_XSwaAhec?idCZBor3hsmSXsEUWUp?S8mJcGsrqo-*v^of_ z06Wyh9@<`CkHEwT1$Hg(YEUS#;vXAbcsMwi_-8&^gHXG(!J)ai@NEomTlBf&nWV5O z7Sv6L?M{+a5>KBwJ)t~v&(BhGaYH-k6jY*nDmEF8^E}PPEs>pvhyU5LXPL2Bh)Z~R zv|NeMbr02?e4U+}n>yoZ7GRIlbMa^vlaqFCXx$mPI9Znp_&62J)5XZC{>_Blh7InyPHHu(V(+>XBI{W z_BBj|IktJ1e=G-D(Jk=nuF!2PnVqdx?Pjmsmk6iH(b2s7m%_rHY1;jsa3(P{2p&ef z#yuTCrJuHk{2eBd^PtO7eje9>pZNw~;h0L0UWCx`d6BF6HpA$P5ojIWCsL7lJ8<-+ zOP7!BpD^ygi9DaAOLmv8qYfN+9Se=~ z=Q=(r`3OFZNFOL1eR`a}MKOR*bVz&l?CH_oRoDgvPGhFht3M+oBPuEx@+0ezUJaoNOVZ@HT=x}~=f(TaeO%{LZUHN6B#-_Fa-h8L z`t=0w4_d#z24l_TWIQb9Q~n~E^6Wl5wwAwpdPP}dpTGY-SyykB>Ri=}TPUh$gsEZe z$K)P+z^NKX<*IM=s(J}H{VKsTEMZZPEPuB_gK`b3gFkJ$7IZmzb-NmKuo17tH2xZ3 z!(T&dyyfFT58e%t^QAc>#2nyrr<`8T88j+A_fxIA^K@@^`FQ#@O!MD7eONH#DBl74 z8(&V3!Dt8M2mHnB^UEyd{DZ%LNQiMg#Txt1rCTRYGm3nzd-#?Zt3DCV+5Jh6*_0|- zq*TZGx9JFzk8Y7<$!(`_&SP_*B2tj$Bks3K~Ude*`kSGOM z7nq={UAssXI&`ITfW@6YeG{8*ranGBT78NY5w#AG8#p+=mR51$+xVwXuS}Zs!=y=j zVhDLyNDJ1mj@uWXnuUMWVp=PeQn045x83Zm5ri|1HJLpKYcR(<__=j>$Mv-aYjy`? zO@E*w#%0Vl?Z&*t_>?A^Zpk>LwmovIT{{3iHl03010l2=viizt_((6L{c0mkw7^^F z7xQ7x1W)5T;dfUF9r!eMvYLR$=~GP{ps?GfE0+-}x1QTZI@xZr{QHZYMF=l@60`6k(+o z(eE|g=Zbld{puPZ_`yI{t?>NRRC*}*BOgLkQ{#m<@Lv0Xp9RxPtYAOoZ_HO)Y=zswa z!R}do^#&-+#8H=-+CbM(lJ&fv0`hnh(}^)h*QrgLHlp5^8P2=Z8ta9%UoF$*NaYuF zf5nm}krk7g!@n2^vwYw;aUcJ1s-w zr+c~68*3OE?`pbjCuWPd>TmMh9B4rw(unK5a5#SxJ;zEt67GXm@Uj0W)=@4VZVPQj zzG;O@8|;yel+xcMOE`7|R|&wx+gr#Mi7N+`=yy2**cd^Rz?%Ax+~?p6-Bo`x zl6H>c8?czeV5MVym2Wa3(75aGKd*tPX|!W{Pu7$|*Vu7Y-|4lA`9fFvYIQ5E@%6+~ z5MO#K0zDHj30mJ#Bdzh48$>&s25~_yqwnhvXw_)KVm~QO92<~oXxNoTXuqIyYc^bi z=sPN!@Oq}fPZ$u{CxFm>m~DK1m8*;7@aBPz;C5=_@?m%j zz`2I*D0hhi z)A_5;ykfd1>KxYl?KCt|lMYwma_8q~a2UpmrG4}r2Sscj=p5x$WYDGEUE^=tPQbd?#sFaL1oWlv* znj)8X51E01T97<^tRYw%&FK}rgHtCJqyb&$FjTo7jV5f7d#?ZZuFN$5bi!||YH5wX zXf$50A+_GB+wpzT`YgBSzkc@;ztfJ0S=8#&WZeARLTf#Cn{n*-PFl_f=PxkvwCPxX zpF=nKl)1@$+^9(Wl*K-Ahta?6k!_|gU0RXFDnWK$;_GlK=5`n3P29k!Y`_f+{$`*R zfpd<#l&wE#b8mJWg=*zoxDZ8eVJy>^fwe~9QeOW)XIU1T0?#a*7&2H6Za<5mdY@G? zr-{eR0F3e8=kzRCV{D8a#)cpGa>&48@+)I8Wbw3zv7(t43ZY%TYsYj{==Ctz8lWu^ zjzOxW?Ck8+opkVYT4jwIDm?xH%@oyl=kXCkCu=Yus4s2)ZYb& zw5D;7LE&?mYOLX(6q2OZ^pJ^+(>nAI1%h9C0EKi%JCxf)!Pazla45AF{8zOjwuQaD zz12r$EDSa2o;6LJZB9#)5!MEb8enDMv=AL;+d?fNY*zvltmzCDSS=k?LaeqLptzQr z;0ryJ(!vA#oDL7C;|ak(YaoQEA=yFN6PR61Wqwn!)Y(kshfqF;k@M!cIka!DiG|Mc zM@w|<25u!?pLB57FSc`-S+t!ZT{5bs= zIUNRevE;5}Xu7#5w6H9mU-4y&pY^<;J01(W+94-bSLS7En~Rry|NRwwX=^;RaI~)j z6umU!S>c=7*6Xk_8DCK!NZC5YLd>x)5stTNgZw;bW_1hQm^`xhSx;m9Lez4X#kyeJ zh?O_fj_2@GTLWx5%zbL1&*VOi%$b~nA8Kn4w0VvB4Y&Ux7eCSW*h-{Cc$F(wr1X+| z1fRFgJSwK!-IQ<|R7UubuZ=b^#Xk*dYJ6ra5Bvvl2II+n4Wio;hUC({*VGZgUqY#y zCE>WX0uV}{A~T`bO&6@tj+A`!+5UJ-lHQbMH9ICt^Wh#2c{bm_5R0Km<0C2Gi@~ts z#dGJ*cN7k{4x%L?mQJnJmj7zd-CL|(ORGk;E>QXEwbl?xx;I>KQ`{a}(@N&?Tl0;<=W6C7Q|W5@HWM1$?j89{9fj z-sPF4P>Gg_%$ys5ASzo}prZ4<%HH_nyk z>Hsb?7os%IET>$q<5zOA@3s}v#|+uQOn3a&O2ww%#w6zwQ>Qp?f#k_9Mn7pt&DPlr zl{mO3x+tpQ)(DQxUfzOhN2%}!bS>)!-(;%7C+PEG7sFo0!RTD-Rt79IJ69RdgWn?z zHbOyS_AQ^-mf4Tl625S|uB5ZGs2GGJmg0p&s>pF&E_vrA>}tBqg1~|rlxfVw0Z6CK zv_(hW#b(`KX>C6!a(+q_<=;h&>PgByGpSLd_GifrI$ET074BV`P+T@PkNcKzXN%k( zLUd(B$K>rQ)+U!^R8$Fiy+_ndX6p+nhBQ6wwWsl&FEcoQEir(o&QUyWS4G$do` zQg(#2++XHy0C|2xe=ktMP59y;)8R8e?c1|jXj;-&e3QqVf9ZUYq~`2V(p&X%*SOmp zOJ%gn+}O;SdFfQFcp}Mo`tar@-Sek{vw{~dJ_c(frm76~+Sn(F+!f5OD00P51km;8`9wsn_1H9g^LLg%4FgXC3V z$2rVt2hBIwI~mxA%^8W%RTPEldBd52#MUr&UJ9fV~{dNs#oQOf*Wb?El5*JJDO3%PUG{245sWZIuA zpi%m0mG>i9>bH_h`~jLU>ULYZ|ElTYE!M&f!aM8a4I!yn!d>k;JT}$kxWKUaV%AHN z6~w(M02PD}Rb87TY80UYf#gVIap6;N4>@M=LZI>Fn$a{++w9j&tHu)BuO;I9#W(Jj zve^P4RPmP5pt#pb!!&zm!C6n2hIhS`^R^8KR#-jIgEFJZ5Drrr(WHm!Wv&H$a<6kQ zVAGmZs>g8>=fQ|06nS&ow!QI$?BmN8beN{#&8l9U5-@CvRBTe@pM9!bXD(mvUgMkP zW0o(U)2Ne&xKIHB>v7{5eYW=0RKe?hnnrJrw&#SNfb)_)67) ztE=B+xdrp-fvo6Lzy0y8rWEZy*A+PzcBxv`1(hDqrK_faS9C?l-g8eMzr7wFn~}lv zN^ZukX#p>L2{7b3WsD{y@J?{H(l&g(VgU6e?4L0?(hR}PxE(*Q8pjH@6kMh?723aPoDF4r|3@2#8@8|bDRp}8Ze`< z`!g0n@L4R9b8nUCPSk;q4xMYqX;4PbwA)1y9XEz2JgBcxE1%0x~U17rv4wsB1WVtG*zgB>FkhH_gCTmK6RRYF& z6vyipO@y6q*Jh55BQdJ9co$$(2^nQkU_8@_!D-G2)s7}_*bxYG z#gZS|n9S>EckH=hx;-pdY@iRtfn>;!ZH+i0{j7(O10hLA1`YCo6D@Z#5VDy_&*G$R zh9Jkv&ZHlI-DDjqW7R)=+F`J~VKzvR(i-yCT$s7($$<{AnwSKQ9zA0_2f@l^!*$j> zs1~n5Ik0kBy2lq;6mn5wI9P;^rYp1IPh=I=Nk6}OHIiUofo21`;@mk%!t-blLI+!k zU4#HIuVQJm5eBK;VT6I6KFbE5Q@2yYs(SrVP&MM!9HASs_3OH8m~g`SM&%tE!g_a{ z&h%GcZMKA8DI3+NvoV>WZgPLlXi-7?2L2)O{{9^_tv^=(1E)(&f~Cu61rH2ru;VGl z^S+YX;7le|Nrf{HC*@TWGmPp6<@7tCH21U*@BZ;%_76G!8RO(iXO))f+v(J zHiR{LKj;I2%KQ9zmu}M^W#H^?TmlC|MuUqv#ty`S5twhxIdrJIJ8O^9j=LXJ7xD9W zkOOeUM*O+>bKH#p2ud!wR2I}6E>Iqy9F1!1$AXvQsxoSCFL=-z#y>YKl-5fI4+^b2 z{2@Lrlh^z5ZJS@|As0O(<3sQ(?uK4XuMUS+K&>(uv$bE1wCzyG(YmVqEA{}9M%Z`1 zxrV!HVp7o%^2A)jU1g8SaEVMeAI#x!kK3hFU3~@za|el7^3dfzo1Z<^dZuS2dp3Rf z`0wNdZ-_T>2W2#rXg1G)dMb!rEsT8eh99WTuYx;KK7`g$^Ee$YXaD0FWtujf9S{(p z40Y>L(_jHTCJ9`aj!lW?Fvm%rZ5eYnZ5@jZc}qyhI43A=xH9N-sEbY-jMN1aa;Xq& zOQGR#`ozyaV~+Dvpu*7XCTZCuLr@ZaD{lw_Trh45NB$;Vn_1I7oILYj1Fib(yqp<6 zgluIo3mrusTl|dYiyRiSRfkJ$A>6)N@z!T=t9A3_4DvwrQ;|uj>X>f6F6^@J05DrQo=tyBRFR*(WGrsEs4A+^IfiOlAyD#kaM?r5dTP;Pc{B zHMGWC;CGA@efqW4uq@t95c}+GoE_iF!cskr!{wA+xr@UGXrDpAOPmKNYg^X>)nLy) zQ+JfunDc5&Q4q4din9i*#?)&U*<<@X#_U!hRl*Un=Cn#E*TO0Zn@w_Os06**FTZ9c z2W7MKaX$E3O$v^_0~3or`povl_?4gEHqgPZ1DPT0!sE>okvL2+J3U9vl+{(3cgP%z zyvzUJ9I#zSZxKuh&<9TM3MwBofT9iF+|&(P&=y_@c?2;nCieW|digb2!L1}@#E20? zD_7>b#j`Ov6fj0OW$2nI57cIK)|j$*Ym8|D&i8dQ3y1X-C2Lrg%?NX2uF##6EcP4T zJ8@W#iM|&SlSi@G26NKzZm!TlPCe!vU$StjpcG@RwDJMcfRlEObH3| zTE8nBLtxKH+)7ZwqMOg1C;IIwQt$L=F+6EuoO`0g0 z*`_ivsgiV1UN2$Qu=tuxPL`sYYnm|mwXb8-8edU3MV$UVbOkeeYqw-zCuOcGmj#!*2&C>*eY)ef)W!?(~ zQsG^-82D`*+WXFDSFetWTH^?y;u0qlRsNq{n38?6idC z({Ac9=f43s`_}+Vxn_+>*)W_rv!dW7fti5VxFg-Il3JgA686#3T7NJ6R_&^4*|NV0 z&gdj~+GQ;N8feISaw-ZV->64eTIykd7X2XyCmOb}JwkCJKhkA3Rd547s?RKK7}XKN2;*q$a z@U&M4g z?D%;J-b@~c$$wm;!n%I7bSaeo0?hULo2hcHG=k9r#%4t@wY(t&dlo#*OiL%uFif_>M%!AVBb z;pNlFk#D~pEb4f4dn(6(2xi2KT>~gJY+EF`%k~jaF`T-gBfNI5nS>uUhEX%>{7Ep^ zUb0a*gLBgP-fPga!?$mr2!AUHT2i!U0WMn5B0|%S9Xpp1u|d#e)n#2C@vr4TrxoCK z1kv9WA^Kb4^py4+z{$&7_2tVXoN*9`!wEltZP`fMMOJqh@5pa&ThQL#!QP%}CzX70 znthNhdYz2s9YA6YZVVkt>TGN*3TDr4C6e$P78X#ywr*mu^r7p(&xtgrA+EPh*|9=} z3gw+ER2UvaO=Q;6fmUMNNhp=uSZTd)R2JSLY=ToUSX8U6k#+5zVi+&in3^@Tu$6+< zF4_X54!$$Y0yene!#Y z+hX0~v8_;Hc@SRR(WtVv2JGEv5vSMxG(h*v%i10{$uFWIE&vN$C#R|~@1+{zk1)qUuKz4-yj9t=*n8Bv z*Q>cwUR6e`-tmJ$CF?0c`I9OZIn}eB41u@Veu?&b5i0iSMUogAnnFT#?~EDE*FE5R zg~QpwNhWfrCTnrGTvZbi-j=^p zfUW!Gm-fyuzQMWOCZex4G!mfq9_$JKl$mvRlPel4dhc$M(511U=S!vJG(23>Uaz50 zOS9wzK3yOJ8?|iNZ5Nyh%fEnT=?)LcagieB!2*%LbXZ~Q>|-zHY=*M;&#CWSquV6A zg;sAEtd@EFc-@pKQzG6G=Jef4v}0j*&)NH0w$88X*3q`s>nVmKbJ~FN{Av!gpc@it zS!p7#^v#AMW727rYj!E)R1LU(F7MBcKdic*7R+S?J)iV{4_|?Lpy!9D4 zXBGECDyq;fi#C7|ZO>)@{+Trljn5U1N`Mbnyci>D@Ho}=rzOx?i;YNYEGw4k1<_rn+EA`8 z&rZ;kH=RNg@}nL@!8q;c(W7+ThO~lhsJdUH8t^%oh#`y?kYyJDa&4-vdgi4*WKJpf zntpzMA%1?vxKvi98|UPvCf}i3sWd?WSJqi-ls#`?>^IfT=W92&{2I3G4bM7lP?n>z z?7)jgx6FGmM4quDFILStgeZ@cm1XhS|CWOJff*IvilbF8ckRPt1=TIwm&gM~zM#K( zilFLk?xQX47%!vZYZCGAj2eQaMid)O@B?P}89pXVh#xAkkx1+KwA+W`hk?-;&teTy zx+nd-_Fvjgid72cPEwbB;IG2c^Zx!Df`!|b+rXF`b-!41#Nz8s$o>glpgjUlTS;$nD{0IONk*47r<=bQsfc5gO~wl-MI zQYr=lk47_^mBUXKw*l9BWg>akngK0jg&pLLtA%1bg9)k3uvD^UIJvHGXR5vO!r#6o z%x7O3uT|8Vz!t%TeyR!OIy7yvL-8p;JYSb_o;sTsSvxbziyXim1A zSxOn3C| z7c@s;N0zcb?iE|w(S6YJZfDR;;0ranD@)eozheda>Vja~7VNGQ=xxUm?Adbe_=^8v zGTn(s?peF-`a5F}U%rCvZboj#dv-dbAa1vs)y#VQzTJFRt%8hiz4$ZRHE8_TOVb%? zAZy&0Kaag%zq4AFn~@ej2|VysFlSb;rAgko;c$=4V-+Q{x@N6^1hlZj}Y*2*_j<;a04 zf+o&qkKf9-inmw#hnq9Fo34nJ3dJ1}sw`?7R8PS7W-sx%y}v4F(fKru#>+E1aX4F( z6}>@BnOnYSfSlv*tHYfZ{lC(-D{X%t+{eN+dt57+J^k@S7E@`run2vfW79!}CPv{& z`narnyr5w*m*K-ZdYjVOW*t2PQ6A7pOZ6$NnlN97q?oZ4e2IjbPYO75_Gn+_vtNv2 z9{GRC0gvGaV8lVRZKh-JYgix;`y+a@CY(29!#5WHii00+EOdh;J)8*DaPQt6R5?Z3 z$u%;}w)^0RMi87Je};{Lg+5EMVxkYZ!-61bfoI?=DNx^il~pUJO2IT~(j1E=iwD-l z!l#Jl9pguQU>pc`i|lblv)M1iP~~#rvuOKjng}x+FZmt}zM^85QZJS+xkm_l!n$Yb zD3JQJj}P3VI6CgCaRs9?PosITeIqCC2seIKbG8Ioa{F7$JE~DcRf6&Up`!IITA`1@ zUw7HB_b+e>EilkOBnuYA#Vr4v!=}(q#Esdl^~IemRv?$WnNdyHqqFxTCo6KcWX2~; z$vJx@>|zXZ#a69+^J>hx<#%EKB@vh>fIO><(Fu}&RdhL4brNtqB zd!!w!SMe@wa714l%1>H(zyUw64-d6xRVdvrYtM`?MF1SCk{l>_Ze>}=`{%gP9J7(a zrym(XXxQuSu)J>Zjyc>DgG#+2C(gZ~vyIoec9;u2!Y=Ff(Mj3dS$c3}_WV^tX}LNY zr#2I(1ECHW>*fU9YN#*B%=#|rShq^xK8`#zZ{ECSv;QE+ZH^z(bzxu7yq6tGT*n-) z?D|8Jis5%&Y{Aocf%2WW+^M3>DNuS~`xbV23q6eP-+znmSjB;V++>T5yKTfjbY_iD z-#zi*mK&M5S+R9l=sS`H4`{^ku~0ZOu0`ga&t`sCkG=0ys`}ka{5z?rm%jAmd+$GD zdoac*Sv8D2f^U0~biU_^W)c%VKHQ^6GS?Y}XFYLd6Hw28=K<4nSn!iAqMevB`SRcV zgL$!U;tO*oPF(&pskD3aTpGH@bxnom8p@Wyg$XY#Z6FnQ-JecOS@4bCbB$D%=Gt#p zY)s4=c<1xne Int32` - array argument type: this declares the type variable `n` as the index type of - the array argument. + to tables with _any_ index type. This is possible by declaring an `n => Int32` + table argument type: this declares the type variable `n` as the index type of + the table argument. -def arrAdd5 (x : n => Int32) : n => Int32 = for i. x.i + 5 +def tabAdd5 (x : n => Float32) : n => Float32 = + for i. x.i + 5.0 -:t arrAdd5 x2 +:t tabAdd5 y ' But function types can help you out even more. For instance, since index types - are statically known, type checking can ensure that array arguments have valid + are statically known, type checking can ensure that table arguments have valid dimensions. This is "shape safety". -' For instance, let's write a function adding two 2D arrays with the same shape: +' Imagine we have `transpose` function. We can encode the shape change in the type. + +def transFloat (x : m => n => Float32) : n => m => Float32 = + for i. for j. x.j.i + +' We can even make it more generic by abstracting over the value type. + +def trans (x : m => n => v) : n => m => v = + for i. for j. x.j.i + + +' We can also use this to check for shape errors: :t x -:t y -def arrAdd (x : m => n => Int32) (y : m => n => Int32) : m => n => Int32 = +def tabAdd (x : m => n => Float32) (y : m => n => Float32) : m => n => Float32 = for i. for j. x.i.j + y.i.j -:t arrAdd x y +:t tabAdd x x + +:t tabAdd x (trans x) + +' The type system checked for us that input tables indeed have the same shape. + + +'## Case Study: MNist + +' 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 + each with a fixed size. + +Batch = Fin 10 +IHeight = Fin 28 +IWidth = Fin 28 +Channels = Fin 3 +Full = Fin ((size Batch) * (size IHeight) * (size IWidth)) + +' To do this we will use Dex's IO to load some images from a file. + This part uses some features we have not yet covered, so you can + ignore it for now. + +raw = + ls = unsafeIO $ \ _. readFile (AsList _ ['e', 'x', 'a', 'm', 'p', 'l', 'e', 's', '/', 'c', 'm', 'n']) + (AsList _ im) = ls + unsafeCastTable Full im + +def pixel (x:Char) : Float32 = + r = W8ToI x + IToF case r < 0 of + True -> (abs r) + 128 + False -> r + +' Here we use comprehensions to create the full data table. + + +ims = + for b: Batch. + for i:IWidth. + for j:IHeight. + pixel raw.((ordinal (b, i, j)) @ Full) + +' We can look at the images we have loaded now using `matshow` + +:html matshow ims.(0 @ Batch) + +:html matshow ims.(1 @ Batch) + +' We might also use aggregation to compute image statistics. + +:html matshow (sum ims) + +' This example overplots three different handwritten images. -:t arrAdd x (trans y) +imscolor = for i. for j. for c:Channels. ims.((ordinal c)@Batch).i.j -' The type system checked for us that input arrays indeed have the same shape. +:t imscolor -'## Writing loops +:html imshow (imscolor / 255.0) + +' This one shows all the images on one channel over the base plot. + +imscolor2 = for b. for i. for j. for c:Channels. + case ordinal c == 0 of + True -> (sum ims).i.j / (IToF (size Batch)) + False -> ims.b.i.j + +:html imseqshow (imscolor2 / 255.0) + +' Sum pooling downsamples the image as the max of each pixel in a tile grid pattern. + +def split (x: m=>v) : n=>o=>v = + for i. for j. x.((ordinal (i,j))@m) + +def imtile (x: a=>b=>v) : n =>o=>p=>q=>v = + for kw. for kh. for w. for h. (split (split x).w.kw).h.kh + +im1 : Fin 2 => Fin 2 => Fin 14 => Fin 14 => Float32 = imtile ims.(0@Batch) + +:html matshow (sum (sum im1)) + +im2 : Fin 4 => Fin 4 => Fin 7 => Fin 7 => Float32 = imtile ims.(0@Batch) + +:html matshow (sum (sum im2)) + + +'## Writing Loops ' Dex is a functional language - but when writing mathematical algorithms, it is often convenient to temporarily put aside immutability and write imperative code using mutation. -' For example, let's say we want to actually implement the `sum` function +' For example, let's say we want to actually implement the `mean` function ourselves by accumulating summed values in-place. In Python, implementing this is not directly possible solely via list comprehensions, so we would write a loop. ' `acc = 0` -' `for i in range(10):` +' `for i in range(len(x)):` ' `acc = acc + x[i]` -' `return acc` +' `return acc / len(x) ' In Dex, values are immutable, so we cannot directly perform mutation. But Dex includes algebraic effects, which are a purely-functional way to modeling @@ -234,20 +323,22 @@ def arrAdd (x : m => n => Int32) (y : m => n => Int32) : m => n => Int32 = the `State` effect, which provides getter and setter functionality (via `get` and `:=` assignment). Here's what it looks like: -def arrSum (x : n => Int32) : Int32 = +def tabMean (x : n => Float32) : Float32 = -- acc = 0 - init = 0 + init = 0.0 - -- (ignore for now) + -- (New Line) withState init $ \acc. - -- for i in range + + -- for i in range(len(x)) for i. -- acc = acc + x[i] acc := (get acc) + x.i - -- return acc - get acc -:p arrSum x2 + -- return acc / len(x) + (get acc) / (IToF (size n)) + +:p tabMean [0.0, 1.0, 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 @@ -255,21 +346,24 @@ def arrSum (x : n => Int32) : Int32 = more detail. ' First: `$`. This symbol is used in Dex just like it is used in Haskell, but - if you haven't seen it before, it seems a bit strange. `$` is the function + if you haven't seen it before, it seems a bit strange. The symbol `$` is the function application operator: it basically replaces of expression-grouping parentheses `(f x)` when it is inconvenient to write them. For example, the following two expressions are identical: -:t arrSum (x2 + x2) +:t tabMean (y + y) -:t arrSum $ x2 + x2 +:t tabMean $ y + y ' 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 - (i.e. closure). In `arrSum` above: the lambda takes an argument named `acc` + (i.e. closure). In `tabMean` above: the lambda takes an argument named `acc` and returns the body, which is the expression following the `.` (a `for` constructor in this case). +:t \ x. x + 10 + +:p (\ x. x + 10) 20 ' That leaves: `withState`. This function uses the `State` effect, enabling us to introduce imperative variables into the computation. @@ -279,6 +373,7 @@ def arrSum (x : n => Int32) : Int32 = :p withState 10 $ \ state. state := 30 + state := 10 get state ' The first element of the returned pair is the body function's result (`20`). @@ -289,10 +384,11 @@ def arrSum (x : n => Int32) : Int32 = The first is the `let` operator that creates an immutable assignment (a "let-binding"). This one is built into the language and can be used anywhere. -q = for i:(Fin 10). +:t for i:Height. -- Bind a temporary variable `temp`, as an example. temp = (ordinal i) + 10 - for j:(Fin 5). temp + for j:Width. + temp ' 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 @@ -302,154 +398,87 @@ q = for i:(Fin 10). '## Typeclasses -' Our `arrSum` function is pretty neat. It lets us work with arrays with any - index type and computes the sum. However, `arrSum` explicitly takes only - integer arrays (of type `n => Int32`). - -:t arrSum - -' If we try to apply `arrSum` to float arrays, we get the following error: +' Our `tabMean` function is pretty neat. It lets us work with tables with any + index type and computes the sum. However, `tabMean` explicitly takes only + integer tables (of type `n => Float32`). -arrSum for i : (Fin 5). 10.0 +:t tabMean -' We can compare the type of our `arrSum` function to the `sum` function found - in the Dex Prelude. +' If we try to apply `tabMean` to other types for get errors. For example, what if + we have a table of pairs of floats, the function does not work. -:t sum +:t (for (i, j). (x.i.j, x.i.j)) -' The Prelude-defined `sum` function also has an additional argument, spelled - like: `(Add v) ?=> ...`. This is a constraint telling us that the function - expects an `Add v` typeclass instance, where `v` is any type that implements - the `Add` typeclass. +tabMean (for (i, j). (x.i.j, x.i.j)) -' We could look in the Dex Prelude to see exactly how `sum` is defined and what - `Add v` means. But we can guess what the `Add v` constraint means: `v` needs - to be a type that works with `add`. We can do that! Let's define our own - typeclass. +' Intuitively this seems like it could work. We just need to be able to + add and divide pairs. Let's look a bit close at the types of add and + divide. -interface MyAdd a:Type - myAdd : a -> a -> a - myZero : a -' This declares a typeclass (i.e. interface or trait) called `MyAdd` with some - typeclass methods (interface requirements). To implement the `MyAdd` - typeclass, a type `a` needs to define functions `myAdd` and `myZero` in a - "typeclass instance", like so: +:t (+) -instance MyAdd Int32 - myAdd = \x y. x + y - myZero = 0 +:t (/) -instance MyAdd Float32 - myAdd = \x y. (x + y) - myZero = 0.0 -' Once we have these two instance definitions (`MyAdd Int32` and - `MyAdd Float32`), we can revisit our array sum function and add a typeclass - constraint: - -def arrSumGeneric [MyAdd v] (x : a => v) : v = - withState myZero $ \acc. - for i. - acc := myAdd (get acc) x.i - get acc +' These types are a bit complex. Add maps `a -> a -> a` with a constraint that + `a` be in the type class `Add`. Whereas divide maps `a -> Float32 -> a` + where `a` is in the type class `VSpace`. -arrSumGeneric for i : (Fin 5). 10 -arrSumGeneric for i : (Fin 5). 10.0 +' If we look in the prelude we can see that these type class interfaces are + defined as: -arrSumGeneric $ for i : (Fin 5). - for j : (Fin 10). 10.0 +interface Add a + add : a -> a -> a + sub : a -> a -> a + zero : a -' This sum function works for any type that implements `MyAdd`, like `Int32` and - `Float32`. But it failed when we tried to pass in a 2D array. What went wrong? - The error tells us that the function could not find a `MyAdd` instance for - `MyAdd ((Fin 10) => Float32)`. This makes sense because we have have not - written one. We need to tell the system "how to add array columns". -' One option is to directly satisfy the type checker and provide a specific - `MyAdd ((Fin 10) => Float32)` instance: +interface [Add a] VSpace a + scaleVec : Float -> a -> a -instance MyAdd ((Fin 10) => Float32) - myAdd = \x y. for i: (Fin 10). (x.i + y.i) - myZero = for i: (Fin 10). 0.0 +' They tell us which functions we need to define for a type to work with them. + It it relatively straightforward to add a new instance. -arrSumGeneric $ for i : (Fin 5). - for j : (Fin 10). 10.0 +' Here is an interface for adding float pairs. -' To be more general, we can instead define a `MyAdd` instance for all array - types. This instance requires that the array element type `v` also has an - `MyAdd` instance; this requirement is represented as a `(MyAdd v) ?=> ...` - constraint. +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 [MyAdd v] MyAdd (a => v) - myAdd = \x y. for i. (myAdd x.i y.i) - myZero = for i. myZero +' And dividing a float pair by a constant. -arrSumGeneric $ for i : (Fin 5). - for j : (Fin 9). 10.0 +instance VSpace (Float32 & Float32) + scaleVec = \s (x, y). (x / s, y / s) -' This instance not only works for 2D arrays, but also 3D and higher-dimensional - arrays: - -arrSumGeneric $ for i : (Fin 5). - for j : (Fin 9). - for k : (Fin 9). 10.0 - -' ## Learn the Prelude - -' The Prelude contains many handy functions. Since Dex types contain so much - information, it is possible to infer what many of these functions do just by - reading and understanding their type. - -' Here are a few used, commonly-used Prelude functions. - -' * `select` for filtering - -:t select - -select True 1 2 -select False 1 2 - -' * `zero` for creating empty arrays - -:t zero - -myzero1 : (Fin 20 & Fin 10) => Float32 = zero -myzero2 : (Fin 20) => (Fin 10) => Float32 = zero - -' * `zip` for creating arrays of pairs - -:t zip - -:t zip x x -:t for i. zip x.i x.i - -' * `iota` for creating "aranges" - -:t iota +' Once we have these two instance definitions (`MyAdd Int32` and + `MyAdd Float32`), we can revisit our table sum function and add a typeclass + constraint: -:p (iota (Fin 10)) -:p for i. for j. (iota (Fin 4 & Fin 4)).(i, j) +def tabMean2 [VSpace v] (x : n => v) : v = + withState zero $ \acc. + for i. + acc := (get acc) + x.i + (get acc) / (IToF (size n)) -' * Pseudorandom number generation +tabMean2 [0.1, 0.5, 1.0] -:t newKey -:t splitKey -:t randn +tabMean2 [(1.0, 0.5), (0.5, 0.8)] -key = newKey 0 -[key1, key2, key3] = splitKey key +' To be more general, we could have also defined these instance for all tuple + types. -:p randn key1 -' * `randVec` for creating a vector of random numbers +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) -randv = randVec 20 randn key2 -:t randv +instance [VSpace v, VSpace w] VSpace (v & w) + scaleVec = \s (x, y). (x / s, y / s) -randv2 = randVec 20 randInt key3 -:t randv2 '## Worked examples: Project Euler From 902a68bf09fef256aaf00b0480ddc7632ec9cb2d Mon Sep 17 00:00:00 2001 From: Sasha Rush Date: Sat, 9 Jan 2021 21:24:05 -0500 Subject: [PATCH 09/14] update tutorial with more examples --- examples/tutorial.dx | 64 +++++++++++++++++++++++++++++--------------- 1 file changed, 42 insertions(+), 22 deletions(-) diff --git a/examples/tutorial.dx b/examples/tutorial.dx index cc6e1f04d..5271078a6 100644 --- a/examples/tutorial.dx +++ b/examples/tutorial.dx @@ -224,7 +224,7 @@ def tabAdd (x : m => n => Float32) (y : m => n => Float32) : m => n => Float32 = using MNist digits. For this example we will first read in a batch of images each with a fixed size. -Batch = Fin 10 +Batch = Fin 100 IHeight = Fin 28 IWidth = Fin 28 Channels = Fin 3 @@ -256,7 +256,8 @@ ims = ' We can look at the images we have loaded now using `matshow` -:html matshow ims.(0 @ Batch) +im = ims.(0 @ Batch) +:html matshow im :html matshow ims.(1 @ Batch) @@ -480,33 +481,52 @@ instance [VSpace v, VSpace w] VSpace (v & w) scaleVec = \s (x, y). (x / s, y / s) -'## Worked examples: Project Euler +'## More MNist -' To demonstrate Dex in practice, below are some examples of solving problems - from [Project Euler](https://projecteuler.net). -def ignore (y:a) (x : Maybe a) : a = - case x of - Just x -> x - Nothing -> y +' Now that we has more functions we can revisit some of the MNist examples. -instance [Add v] Add (Maybe v) - add = \x y. Just $ ignore zero x + ignore zero y - sub = \x y. Just $ ignore zero x - ignore zero y - zero = Just zero -' ### Problem 1: Find the sum of all the multiples of 3 or 5 below 1000. +' Function that uses state to produce a histogram -prob1 = for i : (Fin 1000). - i' = ordinal i - case ((i' `mod` 3) == 0 || (i' `mod` 5) == 0) of - True -> Just i' - False -> Nothing +Pixels = Fin 256 + +def bincount (inp : a => b) : b => Int = + withState zero \ acc . + for i. + v = acc!(inp.i) + v := (get v) + 1 + get acc + +' Plot how many times each pixel value occurs in an image + +hist = bincount $ for (i,j). (FToI (ims.(0 @ Batch).i.j + 1.0) @Pixels) +:t hist + +:html showPlot $ xyPlot (for i. ( (IToF $ ordinal i))) (for i. (IToF hist.i)) + +' Find nearest images in the dataset. + + +def imdot (x : m=>n=>Float32) (y : m=>n=>Float32) : Float32 = + sum for (i, j). x.i.j * y.i.j + +dist = for b1. for b2. + case b1 == b2 of + True -> 0.0 + False -> -imdot ims.b1 ims.b2 + +nearest = for i. argmin dist.i + +double = for b:Batch. for i. for j. for c:Channels. + case ordinal c == 0 of + True -> ims.b.i.j + False -> ims.(nearest.b).i.j + +:html imseqshow double -:p fromJust $ sum prob1 -' ### Problem 2: By considering the terms in the Fibonacci sequence whose values do not exceed four million, find the sum of the even-valued terms. +'## Conclusion -' TODO: Finish this part with some more examples \ No newline at end of file From 1cbd5b162a2fa7be248660d3c8ace0ea4a0cb2cb Mon Sep 17 00:00:00 2001 From: srush Date: Mon, 11 Jan 2021 10:43:07 -0500 Subject: [PATCH 10/14] Update tutorial to use string literals --- examples/{cmn => mnist.5.bin} | Bin examples/tutorial.dx | 2 +- 2 files changed, 1 insertion(+), 1 deletion(-) rename examples/{cmn => mnist.5.bin} (100%) diff --git a/examples/cmn b/examples/mnist.5.bin similarity index 100% rename from examples/cmn rename to examples/mnist.5.bin diff --git a/examples/tutorial.dx b/examples/tutorial.dx index 5271078a6..18907c294 100644 --- a/examples/tutorial.dx +++ b/examples/tutorial.dx @@ -235,7 +235,7 @@ Full = Fin ((size Batch) * (size IHeight) * (size IWidth)) ignore it for now. raw = - ls = unsafeIO $ \ _. readFile (AsList _ ['e', 'x', 'a', 'm', 'p', 'l', 'e', 's', '/', 'c', 'm', 'n']) + ls = unsafeIO $ \ _. readFile "examples/mnist.5.bin" (AsList _ im) = ls unsafeCastTable Full im From 93a7aac9fbf70bdbc582693dc4705a6f4afe48c3 Mon Sep 17 00:00:00 2001 From: srush Date: Thu, 14 Jan 2021 15:30:46 -0500 Subject: [PATCH 11/14] remove binary files and update Adam comments --- examples/mnist.5.bin | Bin 78400 -> 0 bytes examples/tutorial.dx | 290 ++++++++++++++++++++++++++++++------------- 2 files changed, 202 insertions(+), 88 deletions(-) delete mode 100644 examples/mnist.5.bin diff --git a/examples/mnist.5.bin b/examples/mnist.5.bin deleted file mode 100644 index 7fe2667ff1e32ab58ac6c4869fa648a603752c6f..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 78400 zcmeHw2V50L*Y`vP5yXOE0~C9Sy+n;sv6qq@gZ4Ap*9=b6QQx_G4Q!jXGu=;OgKK$ek>DjYsH4TKE9?MwRiOdu&Tk&__ zG!El%2lVMi9z#Vw*@y=U_zG(&KAX=7bU2GU7-6VVO4QczpBTVBk};lE#sIASC&ues z4ZvbUB>a~FhEO)n_7sA3=AOj(hA1V~*2F;0<(%NvN_#z}dHVO)98{{!J&J_&;0!wL zlkdZY?uA&TCPC3uCw;yHiy*WJfV&HQi}6Sv=U>f%^3~@gB>X0lZny3&fee1YW1Ida zgruw+X~#h&Hj<>Py{eVt0AQ@ZD+`PG$bQbVueN6^dU$3|35tygq37o3twevl~~ zgrZH+fsm2Hl=p?K5A-ugHXDIF`k%`IA0PT?n>=}o3P3>)^Q2sG!9G45CUZSGHu3~f z0h=FDxNCK|Hk|XCShLwc*h(RQ0h=C@==RI*nKE@FOJwarBf*~N9 znS5lFNYZ5R@dU2ycr65RF!=2`RtKyM+mq!9W8|02N1qdEw=rsB^8SRf$}UYf{!0ffqLy^ilM z8!t*Xh}%{cbPz;l@_7Gx4&-yHvuIJeDdjs(rRdNd@I2!;kFHhXuz3`DeOXkM2fV|X z<6GC}R44;pome3N%*|N%D9PdjaE>S_GnQ#&5)Hur9_A94UD42J6pp)hZ-)384Wjvi z&$bdN=bPGT<}Hl5mX<18<}to**oheP4%?`L-1VL@RyNug^ToFe!}}Vm4L~lm{|v_W zF=T-_rVeWe&YoLP2-b$uHOq%Dk*P4n4t5l(A&(;j4-iAZeLuG6J$h;NjKHNBZ?rW4 zKYf9*y8(t;5HiRJ`vT)5|1@^a*ygm^_^r4LPxA~5tB88b?;SDWEKx1z;hPH;>Okek0KVj zaig&U(LC0FEeGnh{&wdqfr?|B)sN}@ddFg)??3RI-l#v8cheX61-?6#g;OFQ&8%En zH=tf%?PAw*IC)P;!62st#+!?HiC+c4R_LEDYgBCZWMceqn86D+GAkRj+WudvSx zoM?XVH9+|`GEwpxUZdeE-lxmuYm)@ri^ItIvSpo0jZDN_`6_NbhHSov zcO~i31aVWTrl+Sshqsc)`G<3$O#KZJngiAmr6-M@|iuoHJ+6 z#7?8RvY(gC@6roiN24?@|S6T6y;f=n$!-}T6~Uy&>@mIw=B3;f0LB*47d;`&=n`~jaKIs z+4N0Hz9gJhZ0ZS4{I)ZJd~9T~;E)MyMw|1%<+y~U7ZIBp@p)40xC9vd$2DZZPlACz z{uRa9l^4YTN@^)9)MRf)70}9D(3yRXWMPMn4>G~t*-mU&3O!`}Su7i@-%q5Y zikIdqi(yRjq+75F<6u?6eEsA$+`G=9sc;{Ta&<`g>&pF$7{pa&(7Cun@9iGOULN^R zvJT0!9ZbM#ovbuHGKNW_>5gSi2(mNzoICiZeFq*tI+ z{?Ruxym_|F8G(u6K-VR_NZj&9sK_>AO4z}*^kkFHb;mEbjdQP#<%1kT!?LS9?pg#F z%@N03WqFrJv$*My3v&Ca@t||KIcM`CIkcC+luXu-9E1vQ$bbRwFzoHQmPqCe=xH% z`)Zo?E^y5=h(rRG?k<>IUeM)4=q64rX>|8Km9Vc7h9={fx<+8pRrr((DN}||d6jXSH+P(K1~Qhz#zJFAcCW%& zYi5pG!(|sW> zxdHC1mP%JKk>jeLUYBXQ^TopPF)c>ItWTHi3A{s#t%*-rrIzk6%lCyALz7~0(m;9K zw{A2(&b%#6&cg!v^XJcBc&T(Fbei@H=%frZJX87$vdnegU-u6y;Gd(>FcYm_`xstTy-iw1kATpADkvda zAcVYNv{ZKC8Ycm?(B|4T&^Z`fj1sfWKV@aVdaf+5X zPeftS`*5*WZ|>glVSm`1!otP~Dp;aKiG?|YOS>boYppcTxvoX2WwTEyP1~sLjGo{j+Z$yw?_(Js(m zsb>~5UtD)W;+B3h_jwj!x(^_b|64$1r|(%Py7{a9`iziWHM!n{0^1cXY=D@9{zxy* z-rnAxkoMu;cknn}9(X6G(lO9v@5k9v;ym5-=yVwV4B0XOM&+Ju`9j}5@BU6&R1L=W zmOYxGjGAa{4wa-ZN|q7S(`7D5Z~AFub>6ZUq_=%^91T(CqLkWGL+iYyE=ljyM^Oh* zqQq56>d0};jFA|d_~x|&<{K{IOhGGAM)QrhCLQxMTj4IfvZPRMsHj;V<#isHA-&Oe zs?f;PQ)U|z(xrpiw+wYjm$t5~QKJSeC#FkMpf;>(&*0vHySi=b)-#f%??ViD^X|n6J zYO+|9B!aJh-;!lhy3s4??Etn$F$+GIq*t?NH`9&Gs5VY3(Kx}qw;-@^HMq-?bY2yv z*M5^Vb~>In4bzYz5!#}?Hja>6{fhQUDc+hM+c3OK)1@x*bLK_Mki!BgN?EIwdQRP9 z$u&J@yELMxO_(lyMiQ`Bq){aPjD-K*6ZyiWOt3qm8&jmAg5&^!e^EK6j)1n$JCsx%Gv`7v6i9dOS5X7q2g?wWtJDV9+MW(GC6B)n(R* zM;Fj%R32F6usSAk@7Tz$UC|(R0JUI)bYgI10IHXPi69(m zy#%cBA-TKCav=euK_osL@CNT?g0hmmPQDqgQ>?VLorSKKpx@By)65xBd z%`)^=KQptw9>a;pMp8~y?{pk&4VlN969VjX^>eRJSqegvm=$3?!eX5IzhVXuYbG?W2%Mj( zuYhZ2Mf(|J28UV53VrEu7tQ+iZ6*lP-4yKwM^JzhoKFEs2n+1%?geS&RQsw&dA#rB z4&?Q|^t>0-jRon`EuY?@XQ`C?du#^sXL`7sLun>D|3o>gq*=7cWM6u8M__cc@NT(# z!PycZVCnSZGFY%qph%DL4~)AF-R7f~&=v zYyevKL|u1Ou)zh`aL1ItX7vi76~Wn3z^;H@YojeTEn&8aljHal=4sj6UR+seBI7wv zs#{d3r?|{jf2MO-!ba*~=O@-4eOoI1WDSvLKqon%`e~cP)cZSWVx7+l-$q= zM6+^I4HrM5%Xqq@k!BezEoZQ*lU2qBZVh%H+*JX~68ya?X1?~3;+j=O&6*8M!}s+A zB2b;CVJRV$PBEnSVANoCXxZ7b$$(uknqc8H@)(*NC}2Bz3isgWuT?8QYQFv%^aRgn zWM%JBa;iYt%e0diz`RSPH%l>49Q*sYy1FvA&}Ius|BAJw&~5&B^_Qm@DhUyIn{cOZ zaa$g*lp5}BUzAsUHr=-jT*p7Rb)Q}mtX&z2u4vcFvEtrsg`rv>n>Hi1KMnam3dN}#M z^YZelWy2WcjN~zx9DuW~d>EEW%BNb1!C<*rZc-(+SE}WS#D|0d<_RZ=32h3GH8UFy zrfLT6J?D7Axs&fvghRfJtwJIU!jn(!GS*a*Z=mb>KC=J@3-pvYf>|FPgnLI}9}z|) zVhVJ24Q{huKbFNf}wjQ*&D+?*9`+{GULbVz;xETBdAQdeq*`_mR)|8Wjxq_Z4YnD%;}KU+6Z%tjWUAJ8hXlC`7d1s z0xeDVbL5fEljT^{;Ud8y-`B2P`{%chSgiG%fCfr=+#R!+mELHK+1!b<$}v8FqI5v4 z>;hwy2?D#NxxcYBU{MT>&rjS3hGy_*uG!ta`1A2lINhd()t1HA;6A}8ephQV3p>wa z&Vd53o*P^~K0_)Mm_>VD7;odSx;aN=RY$vkf z2RKJUKQ?dCb%V3Y)>I$**vZ#6&v5Gb(VfAC;WRyjP_<)n z7DE~`R_L@SVcQ%A3c&e$a8MrOznKFrl`B`)H-}Y&rKdcB*6YdDDs8zIFOF8pEnBk1 z!ZUk{o}7Zt5^}M7-MadAG~lbr1k}piT`;tfe`zjmh1fz+HtDdKkU!W^%=AE5aI&qY zs0ILmc^AS>Bzl(MO{d!S&DR~y3TbaP#9s#DoG-Q9UoL5=9HQ&Rhdr?-skuZ}X(Ul9 zc{SBpVU#^ZUhBG4P45%(d{^Uo;GU68>mCYO+`i*)X-XcGC_z2^Y2#gw2#MJ@TpO6x z?_8-;UVqt|9si>~`|2HfS8qAEdUa+n79!@~D44 z2a2~@0u!A0@7cWRhA$=QWfF|$#q!uTNm}Glt9|?StvIaEd1(PxWtgRoOJ|HAWWtL} zmoCjbWoA7(rYPa0ulY9*HO5l>$p^45S~PC8tzQM?Qf8sFm5Zgy7$sd13{1&r{y=Q_ zB9)e;+NufmI$nye!1B!Wr}2`m#?gvB!MBAKC%j@?@zI)EQLDdPfD~r{)qg3yFzClY zG%mPXjp%$&7XMgG$M`sj{I<4A7m`W7L#;LI&!?X^E^XdE3Sj_I{2ZY>P z*uu3GVmk}P1EBIhHbU@H6zCsJF7*`OCEFW>JgRQThNIBGq{62An~TLybxpg^mfj+F z^s0{5=gw|O!b{!r6cjSl5=^B8;$tDe)1AcMm}L&9QbPI&EtYSOKzt;1`@?XbzdNOSuCAJeK z+EjvOOyri6`uG?2PS3toy=eFDzirvl!Q25gOB8>E6PdQPMfVauV3`%LFcr@*lGc-9 zSxDI9opVkYLl9{)B`lL%Fl>ob4ka@zhFDKIvYTb8bkoCRwd&VhyAODV%xQR!XOR zeSPO|l|_nZ6>YwJC2giHf`aa&4j(>juf>W|ahcF#06m||LhJ)#j(BN0At>$&tUnTZ zH5gEYJj&^O4F~WFGRNf>xn%%#f`w^*D_0H`wUdv_ z6%oO=1OZM2EaS@6T>QJW<*x=Y2tEN+12%ys>rbYa;lU>I8}+~jIaSHoe{Wm2jk?U@Y+seo8Wj z2IOEYFLH`dO01W*qc=I5C7gEf?^}>Q%r^@DxQ+@n3>JC#yX+$P+PnZ>~ zn31(a98HjE`H~zmG+X`~LAhhbPZGlr(fs#d`-E7vYpoF~ zoqSYq|4>8eZOGa%>lC6jg5djdOIq5N_uLDe@P8U{0={?b>+9&~NSh}Px@NeWazF!A zw{a_1u6%u63$~F`r(KFOH;E+a4{cGhSAw~r%DsCJyLRo3l(bp7_q1$}`xFk?%3OT%NncuRQ^%|z)^(N#+RgNn&N<`zA1`vGg zIqFlf7D9e_j}e66jLU0t+}+(p0`@`5+)3cDW*!{w*tF?hI7$YFXJRgi-rj<4U;8aP zf=S|`L!7Re;dLg9gzzQ08Etc$1ZndOp-cNMa{+J$to|9khR>UYt45Rc`ZC|~Cb=e0 z@62k?4g|yon70&E<#5L4BiNx-B?qUpezSjJNRNlObu44 z=)7h%YtDX1Ue4zW>?;JmZgKZoFCIZC@Zz>9_3|EBHaq`c(Km#qe&(I#1Z2>bkY`L3x3+eLg+m!U~|i+ z+1+@1a5Pg2T^wp6cWUWXWNP-JMT>rDeMEb_3nTS8PGLA!($7fG!FdwN7S$_`j-Q@| z5?QwrT(-CS!Gq`*Fx^j9J6Y|UeVfhs_(-rYiaX>2d>2Iep4-eI^Kr(B0f_o_HegoVj zF>7h5d}cZQ1rF%juIE^(b_Bl}VkLFHiqk?Ny!HCViABPu{FEnnvV~+ljtP8{RhfpF z#@Jt?ErYV6&1#ZfRW+f%+Wdes`{`Mf8Zvvx5P#U__6H9kIv`*o;li{pqOZ{l^Dr)> z>p16VYwl$@=eUS(FR3+X(w*4f@+f*MO!F zE7=C3o4!*}n+@Fc1e9_XSwaAhec?idCZBor3hsmSXsEUWUp?S8mJcGsrqo-*v^of_ z06Wyh9@<`CkHEwT1$Hg(YEUS#;vXAbcsMwi_-8&^gHXG(!J)ai@NEomTlBf&nWV5O z7Sv6L?M{+a5>KBwJ)t~v&(BhGaYH-k6jY*nDmEF8^E}PPEs>pvhyU5LXPL2Bh)Z~R zv|NeMbr02?e4U+}n>yoZ7GRIlbMa^vlaqFCXx$mPI9Znp_&62J)5XZC{>_Blh7InyPHHu(V(+>XBI{W z_BBj|IktJ1e=G-D(Jk=nuF!2PnVqdx?Pjmsmk6iH(b2s7m%_rHY1;jsa3(P{2p&ef z#yuTCrJuHk{2eBd^PtO7eje9>pZNw~;h0L0UWCx`d6BF6HpA$P5ojIWCsL7lJ8<-+ zOP7!BpD^ygi9DaAOLmv8qYfN+9Se=~ z=Q=(r`3OFZNFOL1eR`a}MKOR*bVz&l?CH_oRoDgvPGhFht3M+oBPuEx@+0ezUJaoNOVZ@HT=x}~=f(TaeO%{LZUHN6B#-_Fa-h8L z`t=0w4_d#z24l_TWIQb9Q~n~E^6Wl5wwAwpdPP}dpTGY-SyykB>Ri=}TPUh$gsEZe z$K)P+z^NKX<*IM=s(J}H{VKsTEMZZPEPuB_gK`b3gFkJ$7IZmzb-NmKuo17tH2xZ3 z!(T&dyyfFT58e%t^QAc>#2nyrr<`8T88j+A_fxIA^K@@^`FQ#@O!MD7eONH#DBl74 z8(&V3!Dt8M2mHnB^UEyd{DZ%LNQiMg#Txt1rCTRYGm3nzd-#?Zt3DCV+5Jh6*_0|- zq*TZGx9JFzk8Y7<$!(`_&SP_*B2tj$Bks3K~Ude*`kSGOM z7nq={UAssXI&`ITfW@6YeG{8*ranGBT78NY5w#AG8#p+=mR51$+xVwXuS}Zs!=y=j zVhDLyNDJ1mj@uWXnuUMWVp=PeQn045x83Zm5ri|1HJLpKYcR(<__=j>$Mv-aYjy`? zO@E*w#%0Vl?Z&*t_>?A^Zpk>LwmovIT{{3iHl03010l2=viizt_((6L{c0mkw7^^F z7xQ7x1W)5T;dfUF9r!eMvYLR$=~GP{ps?GfE0+-}x1QTZI@xZr{QHZYMF=l@60`6k(+o z(eE|g=Zbld{puPZ_`yI{t?>NRRC*}*BOgLkQ{#m<@Lv0Xp9RxPtYAOoZ_HO)Y=zswa z!R}do^#&-+#8H=-+CbM(lJ&fv0`hnh(}^)h*QrgLHlp5^8P2=Z8ta9%UoF$*NaYuF zf5nm}krk7g!@n2^vwYw;aUcJ1s-w zr+c~68*3OE?`pbjCuWPd>TmMh9B4rw(unK5a5#SxJ;zEt67GXm@Uj0W)=@4VZVPQj zzG;O@8|;yel+xcMOE`7|R|&wx+gr#Mi7N+`=yy2**cd^Rz?%Ax+~?p6-Bo`x zl6H>c8?czeV5MVym2Wa3(75aGKd*tPX|!W{Pu7$|*Vu7Y-|4lA`9fFvYIQ5E@%6+~ z5MO#K0zDHj30mJ#Bdzh48$>&s25~_yqwnhvXw_)KVm~QO92<~oXxNoTXuqIyYc^bi z=sPN!@Oq}fPZ$u{CxFm>m~DK1m8*;7@aBPz;C5=_@?m%j zz`2I*D0hhi z)A_5;ykfd1>KxYl?KCt|lMYwma_8q~a2UpmrG4}r2Sscj=p5x$WYDGEUE^=tPQbd?#sFaL1oWlv* znj)8X51E01T97<^tRYw%&FK}rgHtCJqyb&$FjTo7jV5f7d#?ZZuFN$5bi!||YH5wX zXf$50A+_GB+wpzT`YgBSzkc@;ztfJ0S=8#&WZeARLTf#Cn{n*-PFl_f=PxkvwCPxX zpF=nKl)1@$+^9(Wl*K-Ahta?6k!_|gU0RXFDnWK$;_GlK=5`n3P29k!Y`_f+{$`*R zfpd<#l&wE#b8mJWg=*zoxDZ8eVJy>^fwe~9QeOW)XIU1T0?#a*7&2H6Za<5mdY@G? zr-{eR0F3e8=kzRCV{D8a#)cpGa>&48@+)I8Wbw3zv7(t43ZY%TYsYj{==Ctz8lWu^ zjzOxW?Ck8+opkVYT4jwIDm?xH%@oyl=kXCkCu=Yus4s2)ZYb& zw5D;7LE&?mYOLX(6q2OZ^pJ^+(>nAI1%h9C0EKi%JCxf)!Pazla45AF{8zOjwuQaD zz12r$EDSa2o;6LJZB9#)5!MEb8enDMv=AL;+d?fNY*zvltmzCDSS=k?LaeqLptzQr z;0ryJ(!vA#oDL7C;|ak(YaoQEA=yFN6PR61Wqwn!)Y(kshfqF;k@M!cIka!DiG|Mc zM@w|<25u!?pLB57FSc`-S+t!ZT{5bs= zIUNRevE;5}Xu7#5w6H9mU-4y&pY^<;J01(W+94-bSLS7En~Rry|NRwwX=^;RaI~)j z6umU!S>c=7*6Xk_8DCK!NZC5YLd>x)5stTNgZw;bW_1hQm^`xhSx;m9Lez4X#kyeJ zh?O_fj_2@GTLWx5%zbL1&*VOi%$b~nA8Kn4w0VvB4Y&Ux7eCSW*h-{Cc$F(wr1X+| z1fRFgJSwK!-IQ<|R7UubuZ=b^#Xk*dYJ6ra5Bvvl2II+n4Wio;hUC({*VGZgUqY#y zCE>WX0uV}{A~T`bO&6@tj+A`!+5UJ-lHQbMH9ICt^Wh#2c{bm_5R0Km<0C2Gi@~ts z#dGJ*cN7k{4x%L?mQJnJmj7zd-CL|(ORGk;E>QXEwbl?xx;I>KQ`{a}(@N&?Tl0;<=W6C7Q|W5@HWM1$?j89{9fj z-sPF4P>Gg_%$ys5ASzo}prZ4<%HH_nyk z>Hsb?7os%IET>$q<5zOA@3s}v#|+uQOn3a&O2ww%#w6zwQ>Qp?f#k_9Mn7pt&DPlr zl{mO3x+tpQ)(DQxUfzOhN2%}!bS>)!-(;%7C+PEG7sFo0!RTD-Rt79IJ69RdgWn?z zHbOyS_AQ^-mf4Tl625S|uB5ZGs2GGJmg0p&s>pF&E_vrA>}tBqg1~|rlxfVw0Z6CK zv_(hW#b(`KX>C6!a(+q_<=;h&>PgByGpSLd_GifrI$ET074BV`P+T@PkNcKzXN%k( zLUd(B$K>rQ)+U!^R8$Fiy+_ndX6p+nhBQ6wwWsl&FEcoQEir(o&QUyWS4G$do` zQg(#2++XHy0C|2xe=ktMP59y;)8R8e?c1|jXj;-&e3QqVf9ZUYq~`2V(p&X%*SOmp zOJ%gn+}O;SdFfQFcp}Mo`tar@-Sek{vw{~dJ_c(frm76~+Sn(F+!f5OD00P51km;8`9wsn_1H9g^LLg%4FgXC3V z$2rVt2hBIwI~mxA%^8W%RTPEldBd52#MUr&UJ9fV~{dNs#oQOf*Wb?El5*JJDO3%PUG{245sWZIuA zpi%m0mG>i9>bH_h`~jLU>ULYZ|ElTYE!M&f!aM8a4I!yn!d>k;JT}$kxWKUaV%AHN z6~w(M02PD}Rb87TY80UYf#gVIap6;N4>@M=LZI>Fn$a{++w9j&tHu)BuO;I9#W(Jj zve^P4RPmP5pt#pb!!&zm!C6n2hIhS`^R^8KR#-jIgEFJZ5Drrr(WHm!Wv&H$a<6kQ zVAGmZs>g8>=fQ|06nS&ow!QI$?BmN8beN{#&8l9U5-@CvRBTe@pM9!bXD(mvUgMkP zW0o(U)2Ne&xKIHB>v7{5eYW=0RKe?hnnrJrw&#SNfb)_)67) ztE=B+xdrp-fvo6Lzy0y8rWEZy*A+PzcBxv`1(hDqrK_faS9C?l-g8eMzr7wFn~}lv zN^ZukX#p>L2{7b3WsD{y@J?{H(l&g(VgU6e?4L0?(hR}PxE(*Q8pjH@6kMh?723aPoDF4r|3@2#8@8|bDRp}8Ze`< z`!g0n@L4R9b8nUCPSk;q4xMYqX;4PbwA)1y9XEz2JgBcxE1%0x~U17rv4wsB1WVtG*zgB>FkhH_gCTmK6RRYF& z6vyipO@y6q*Jh55BQdJ9co$$(2^nQkU_8@_!D-G2)s7}_*bxYG z#gZS|n9S>EckH=hx;-pdY@iRtfn>;!ZH+i0{j7(O10hLA1`YCo6D@Z#5VDy_&*G$R zh9Jkv&ZHlI-DDjqW7R)=+F`J~VKzvR(i-yCT$s7($$<{AnwSKQ9zA0_2f@l^!*$j> zs1~n5Ik0kBy2lq;6mn5wI9P;^rYp1IPh=I=Nk6}OHIiUofo21`;@mk%!t-blLI+!k zU4#HIuVQJm5eBK;VT6I6KFbE5Q@2yYs(SrVP&MM!9HASs_3OH8m~g`SM&%tE!g_a{ z&h%GcZMKA8DI3+NvoV>WZgPLlXi-7?2L2)O{{9^_tv^=(1E)(&f~Cu61rH2ru;VGl z^S+YX;7le|Nrf{HC*@TWGmPp6<@7tCH21U*@BZ;%_76G!8RO(iXO))f+v(J zHiR{LKj;I2%KQ9zmu}M^W#H^?TmlC|MuUqv#ty`S5twhxIdrJIJ8O^9j=LXJ7xD9W zkOOeUM*O+>bKH#p2ud!wR2I}6E>Iqy9F1!1$AXvQsxoSCFL=-z#y>YKl-5fI4+^b2 z{2@Lrlh^z5ZJS@|As0O(<3sQ(?uK4XuMUS+K&>(uv$bE1wCzyG(YmVqEA{}9M%Z`1 zxrV!HVp7o%^2A)jU1g8SaEVMeAI#x!kK3hFU3~@za|el7^3dfzo1Z<^dZuS2dp3Rf z`0wNdZ-_T>2W2#rXg1G)dMb!rEsT8eh99WTuYx;KK7`g$^Ee$YXaD0FWtujf9S{(p z40Y>L(_jHTCJ9`aj!lW?Fvm%rZ5eYnZ5@jZc}qyhI43A=xH9N-sEbY-jMN1aa;Xq& zOQGR#`ozyaV~+Dvpu*7XCTZCuLr@ZaD{lw_Trh45NB$;Vn_1I7oILYj1Fib(yqp<6 zgluIo3mrusTl|dYiyRiSRfkJ$A>6)N@z!T=t9A3_4DvwrQ;|uj>X>f6F6^@J05DrQo=tyBRFR*(WGrsEs4A+^IfiOlAyD#kaM?r5dTP;Pc{B zHMGWC;CGA@efqW4uq@t95c}+GoE_iF!cskr!{wA+xr@UGXrDpAOPmKNYg^X>)nLy) zQ+JfunDc5&Q4q4din9i*#?)&U*<<@X#_U!hRl*Un=Cn#E*TO0Zn@w_Os06**FTZ9c z2W7MKaX$E3O$v^_0~3or`povl_?4gEHqgPZ1DPT0!sE>okvL2+J3U9vl+{(3cgP%z zyvzUJ9I#zSZxKuh&<9TM3MwBofT9iF+|&(P&=y_@c?2;nCieW|digb2!L1}@#E20? zD_7>b#j`Ov6fj0OW$2nI57cIK)|j$*Ym8|D&i8dQ3y1X-C2Lrg%?NX2uF##6EcP4T zJ8@W#iM|&SlSi@G26NKzZm!TlPCe!vU$StjpcG@RwDJMcfRlEObH3| zTE8nBLtxKH+)7ZwqMOg1C;IIwQt$L=F+6EuoO`0g0 z*`_ivsgiV1UN2$Qu=tuxPL`sYYnm|mwXb8-8edU3MV$UVbOkeeYqw-zCuOcGmj#!*2&C>*eY)ef)W!?(~ zQsG^-82D`*+WXFDSFetWTH^?y;u0qlRsNq{n38?6idC z({Ac9=f43s`_}+Vxn_+>*)W_rv!dW7fti5VxFg-Il3JgA686#3T7NJ6R_&^4*|NV0 z&gdj~+GQ;N8feISaw-ZV->64eTIykd7X2XyCmOb}JwkCJKhkA3Rd547s?RKK7}XKN2;*q$a z@U&M4g z?D%;J-b@~c$$wm;!n%I7bSaeo0?hULo2hcHG=k9r#%4t@wY(t&dlo#*OiL%uFif_>M%!AVBb z;pNlFk#D~pEb4f4dn(6(2xi2KT>~gJY+EF`%k~jaF`T-gBfNI5nS>uUhEX%>{7Ep^ zUb0a*gLBgP-fPga!?$mr2!AUHT2i!U0WMn5B0|%S9Xpp1u|d#e)n#2C@vr4TrxoCK z1kv9WA^Kb4^py4+z{$&7_2tVXoN*9`!wEltZP`fMMOJqh@5pa&ThQL#!QP%}CzX70 znthNhdYz2s9YA6YZVVkt>TGN*3TDr4C6e$P78X#ywr*mu^r7p(&xtgrA+EPh*|9=} z3gw+ER2UvaO=Q;6fmUMNNhp=uSZTd)R2JSLY=ToUSX8U6k#+5zVi+&in3^@Tu$6+< zF4_X54!$$Y0yene!#Y z+hX0~v8_;Hc@SRR(WtVv2JGEv5vSMxG(h*v%i10{$uFWIE&vN$C#R|~@1+{zk1)qUuKz4-yj9t=*n8Bv z*Q>cwUR6e`-tmJ$CF?0c`I9OZIn}eB41u@Veu?&b5i0iSMUogAnnFT#?~EDE*FE5R zg~QpwNhWfrCTnrGTvZbi-j=^p zfUW!Gm-fyuzQMWOCZex4G!mfq9_$JKl$mvRlPel4dhc$M(511U=S!vJG(23>Uaz50 zOS9wzK3yOJ8?|iNZ5Nyh%fEnT=?)LcagieB!2*%LbXZ~Q>|-zHY=*M;&#CWSquV6A zg;sAEtd@EFc-@pKQzG6G=Jef4v}0j*&)NH0w$88X*3q`s>nVmKbJ~FN{Av!gpc@it zS!p7#^v#AMW727rYj!E)R1LU(F7MBcKdic*7R+S?J)iV{4_|?Lpy!9D4 zXBGECDyq;fi#C7|ZO>)@{+Trljn5U1N`Mbnyci>D@Ho}=rzOx?i;YNYEGw4k1<_rn+EA`8 z&rZ;kH=RNg@}nL@!8q;c(W7+ThO~lhsJdUH8t^%oh#`y?kYyJDa&4-vdgi4*WKJpf zntpzMA%1?vxKvi98|UPvCf}i3sWd?WSJqi-ls#`?>^IfT=W92&{2I3G4bM7lP?n>z z?7)jgx6FGmM4quDFILStgeZ@cm1XhS|CWOJff*IvilbF8ckRPt1=TIwm&gM~zM#K( zilFLk?xQX47%!vZYZCGAj2eQaMid)O@B?P}89pXVh#xAkkx1+KwA+W`hk?-;&teTy zx+nd-_Fvjgid72cPEwbB;IG2c^Zx!Df`!|b+rXF`b-!41#Nz8s$o>glpgjUlTS;$nD{0IONk*47r<=bQsfc5gO~wl-MI zQYr=lk47_^mBUXKw*l9BWg>akngK0jg&pLLtA%1bg9)k3uvD^UIJvHGXR5vO!r#6o z%x7O3uT|8Vz!t%TeyR!OIy7yvL-8p;JYSb_o;sTsSvxbziyXim1A zSxOn3C| z7c@s;N0zcb?iE|w(S6YJZfDR;;0ranD@)eozheda>Vja~7VNGQ=xxUm?Adbe_=^8v zGTn(s?peF-`a5F}U%rCvZboj#dv-dbAa1vs)y#VQzTJFRt%8hiz4$ZRHE8_TOVb%? zAZy&0Kaag%zq4AFn~@ej2|VysFlSb;rAgko;c$=4V-+Q{x@N6^1hlZj}Y*2*_j<;a04 zf+o&qkKf9-inmw#hnq9Fo34nJ3dJ1}sw`?7R8PS7W-sx%y}v4F(fKru#>+E1aX4F( z6}>@BnOnYSfSlv*tHYfZ{lC(-D{X%t+{eN+dt57+J^k@S7E@`run2vfW79!}CPv{& z`narnyr5w*m*K-ZdYjVOW*t2PQ6A7pOZ6$NnlN97q?oZ4e2IjbPYO75_Gn+_vtNv2 z9{GRC0gvGaV8lVRZKh-JYgix;`y+a@CY(29!#5WHii00+EOdh;J)8*DaPQt6R5?Z3 z$u%;}w)^0RMi87Je};{Lg+5EMVxkYZ!-61bfoI?=DNx^il~pUJO2IT~(j1E=iwD-l z!l#Jl9pguQU>pc`i|lblv)M1iP~~#rvuOKjng}x+FZmt}zM^85QZJS+xkm_l!n$Yb zD3JQJj}P3VI6CgCaRs9?PosITeIqCC2seIKbG8Ioa{F7$JE~DcRf6&Up`!IITA`1@ zUw7HB_b+e>EilkOBnuYA#Vr4v!=}(q#Esdl^~IemRv?$WnNdyHqqFxTCo6KcWX2~; z$vJx@>|zXZ#a69+^J>hx<#%EKB@vh>fIO><(Fu}&RdhL4brNtqB zd!!w!SMe@wa714l%1>H(zyUw64-d6xRVdvrYtM`?MF1SCk{l>_Ze>}=`{%gP9J7(a zrym(XXxQuSu)J>Zjyc>DgG#+2C(gZ~vyIoec9;u2!Y=Ff(Mj3dS$c3}_WV^tX}LNY zr#2I(1ECHW>*fU9YN#*B%=#|rShq^xK8`#zZ{ECSv;QE+ZH^z(bzxu7yq6tGT*n-) z?D|8Jis5%&Y{Aocf%2WW+^M3>DNuS~`xbV23q6eP-+znmSjB;V++>T5yKTfjbY_iD z-#zi*mK&M5S+R9l=sS`H4`{^ku~0ZOu0`ga&t`sCkG=0ys`}ka{5z?rm%jAmd+$GD zdoac*Sv8D2f^U0~biU_^W)c%VKHQ^6GS?Y}XFYLd6Hw28=K<4nSn!iAqMevB`SRcV zgL$!U;tO*oPF(&pskD3aTpGH@bxnom8p@Wyg$XY#Z6FnQ-JecOS@4bCbB$D%=Gt#p zY)s4=c<1xne` symbol whereas tables use `=>`. + +:t add5 + + ' 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" to tables with _any_ index type. This is possible by declaring an `n => Int32` @@ -215,59 +244,72 @@ def tabAdd (x : m => n => Float32) (y : m => n => Float32) : m => n => Float32 = :t tabAdd x (trans x) -' The type system checked for us that input tables indeed have the same shape. +' The type system checked for us that the input tables indeed have the same shape. '## Case Study: MNist +' To run this section, move the following binary files to examples: + +' `wget https://github.com/srush/learns-dex/raw/main/mnist.bin` + +' `wget https://github.com/srush/learns-dex/raw/main/labels.bin` + + ' 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 each with a fixed size. -Batch = Fin 100 +Batch = Fin 5000 IHeight = Fin 28 IWidth = Fin 28 -Channels = Fin 3 +Channels = Fin 3 +Class = Fin 10 +Image = (IHeight => IWidth => Float) + Full = Fin ((size Batch) * (size IHeight) * (size IWidth)) ' To do this we will use Dex's IO to load some images from a file. - This part uses some features we have not yet covered, so you can + This section uses features outside the scope of the tutorial, so you can ignore it for now. -raw = - ls = unsafeIO $ \ _. readFile "examples/mnist.5.bin" - (AsList _ im) = ls - unsafeCastTable Full im - def pixel (x:Char) : Float32 = r = W8ToI x IToF case r < 0 of True -> (abs r) + 128 False -> r -' Here we use comprehensions to create the full data table. +def getIm : Batch => Image = + (AsList _ im) = unsafeIO do readFile "examples/mnist.bin" + raw = unsafeCastTable Full im + 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 + for i. (W8ToI r.i @ Class) -ims = - for b: Batch. - for i:IWidth. - for j:IHeight. - pixel raw.((ordinal (b, i, j)) @ Full) +' Once you have downloaded the files, uncomment these lines to + see the images of below. -' We can look at the images we have loaded now using `matshow` +all_ims = getIm +all_labels = getLabel -im = ims.(0 @ Batch) +ims = for i : (Fin 100). all_ims.(ordinal i@_) + +im = ims.(0 @ _) :html matshow im -:html matshow ims.(1 @ Batch) +:html matshow ims.(1 @ _) -' We might also use aggregation to compute image statistics. +' This show the mean pixel value aggregation over all images. :html matshow (sum ims) ' This example overplots three different handwritten images. -imscolor = for i. for j. for c:Channels. ims.((ordinal c)@Batch).i.j +imscolor = for i. for j. for c:Channels. ims.((ordinal c)@_).i.j :t imscolor @@ -282,19 +324,22 @@ imscolor2 = for b. for i. for j. for c:Channels. :html imseqshow (imscolor2 / 255.0) -' Sum pooling downsamples the image as the max of each pixel in a tile grid pattern. +' This example utilizes the type system to help manipulate the shape + of an image. Sum pooling downsamples the image as the max of each + pixel in a tile grid pattern. See if you can figure out the other + types. def split (x: m=>v) : n=>o=>v = - for i. for j. x.((ordinal (i,j))@m) + for i j. x.(ordinal (i,j)@_) -def imtile (x: a=>b=>v) : n =>o=>p=>q=>v = - for kw. for kh. for w. for h. (split (split x).w.kw).h.kh +def imtile (x: a=>b=>v) : n=>o=>p=>q=>v = + for kh kw h w. (split (split x).h.kh).w.kw -im1 : Fin 2 => Fin 2 => Fin 14 => Fin 14 => Float32 = imtile ims.(0@Batch) +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@Batch) +im2 : Fin 4 => Fin 4 => Fin 7 => Fin 7 => Float32 = imtile ims.(0@_) :html matshow (sum (sum im2)) @@ -310,13 +355,13 @@ im2 : Fin 4 => Fin 4 => Fin 7 => Fin 7 => Float32 = imtile ims.(0@Batch) is not directly possible solely via list comprehensions, so we would write a loop. -' `acc = 0` +' `acc = 0.0` ' `for i in range(len(x)):` ' `acc = acc + x[i]` -' `return acc / len(x) +' `return acc / len(x)` ' In Dex, values are immutable, so we cannot directly perform mutation. But Dex includes algebraic effects, which are a purely-functional way to modeling @@ -325,11 +370,9 @@ im2 : Fin 4 => Fin 4 => Fin 7 => Fin 7 => Float32 = imtile ims.(0@Batch) and `:=` assignment). Here's what it looks like: def tabMean (x : n => Float32) : Float32 = - -- acc = 0 - init = 0.0 - -- (New Line) - withState init $ \acc. + -- acc = 0 + withState 0.0 $ \acc. -- for i in range(len(x)) for i. @@ -339,7 +382,7 @@ def tabMean (x : n => Float32) : Float32 = -- return acc / len(x) (get acc) / (IToF (size n)) -:p tabMean [0.0, 1.0, 0.5] +tabMean [0.0, 1.0, 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 @@ -364,7 +407,8 @@ def tabMean (x : n => Float32) : Float32 = :t \ x. x + 10 -:p (\ x. x + 10) 20 +(\ x. x + 10) 20 + ' That leaves: `withState`. This function uses the `State` effect, enabling us to introduce imperative variables into the computation. @@ -372,13 +416,12 @@ def tabMean (x : n => Float32) : Float32 = "mutable value" reference (`acc` here), and returns a pair of the body function's result and the final value. Here's a simple example: -:p withState 10 $ \ state. +withState 10 $ \ state. state := 30 state := 10 get state -' The first element of the returned pair is the body function's result (`20`). - The second element is the final value of the variable (`30`). +' The element returned pair is the body function's result (`10`) ' Finally: this is a good point to talk a bit about some other operators in Dex. In the examples above, we see two types of equal sign operators: `=` and `:=`. @@ -393,7 +436,7 @@ def tabMean (x : n => Float32) : Float32 = ' 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 - `withState`. `ref := x` assigns the value `x` to the mutable reference `ref`. + `withState`). `ref := x` assigns the value `x` to the mutable reference `ref`. Reading the value in `ref` is possible via the `get` function. or via using the final result returned by `withState`. @@ -487,7 +530,7 @@ instance [VSpace v, VSpace w] VSpace (v & w) ' Now that we has more functions we can revisit some of the MNist examples. -' Function that uses state to produce a histogram +' Function that uses state to produce a histogram: Pixels = Fin 256 @@ -500,10 +543,10 @@ 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 @ Batch).i.j + 1.0) @Pixels) +hist = bincount $ for (i,j). (FToI (ims.(0 @ _).i.j + 1.0) @Pixels) :t hist -:html showPlot $ xyPlot (for i. ( (IToF $ ordinal i))) (for i. (IToF hist.i)) +:html showPlot $ yPlot (for i. (IToF hist.i)) ' Find nearest images in the dataset. @@ -518,15 +561,86 @@ dist = for b1. for b2. nearest = for i. argmin dist.i -double = for b:Batch. for i. for j. for c:Channels. - case ordinal c == 0 of - True -> ims.b.i.j - False -> ims.(nearest.b).i.j +double = for b i j. [ims.b.i.j, ims.(nearest.b).i.j, 0.0] :html imseqshow double +'## Variable Length Lists + + +' So far all the examples have assumed that we + know the exact size of our tables. This is a + common assumption in array languages, but + it makes some operations surprisingly difficult + to do. + +' For instance, we might want to filter our set of + images to only allow for images of 5's. But what is + the type of this table? + +' Dex allows for tables with an unknown and varying length + using the `List` construct. You can think of list as + hiding one finite dimension of a table. + +:t for i:Height. 0.0 + +AsList _ $ for i:Height. 0.0 + +:t AsList _ $ 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 + +' And they can be deconstructed to fetch a new table. + +(AsList _ temptab) = z +temptab + +' Using this construct we can return to extracting + the 5's from the image set. Here `mempty` is + synonymous with `AsList _ []`. + +def findFives (x : a=>b) (y : a=>Class) : List b = + concat for i. case (y.i == (5 @ _)) of + True -> AsList _ [x.i] + False -> mempty + + +' Note though that the type here does not tell us + how many 5's 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 + +nFives + +' 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) + '## Conclusion +' We hope this gives you enough information to start playing with Dex. + This is just a start though of the different functionality available + in the language. If you are interested in continuing to learn, we recommend + you look at the examples in the `examples/` directory, check out the prelude + in `lib/prelude.dx`, and file issues on the GitHub repo. We have a welcoming + and excited community, and we hope you are interested enough to join us. + +' Here are some topics to check out in the Prelude: + +' * Randomness and Keys + * Laziness of For Comprehensions + * Records and Variant Types + * File IO + * Effects Beyond State From 255ccbe05439843947f93da5785975c783bcd279 Mon Sep 17 00:00:00 2001 From: srush Date: Thu, 14 Jan 2021 15:33:24 -0500 Subject: [PATCH 12/14] Adam comment --- examples/tutorial.dx | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/examples/tutorial.dx b/examples/tutorial.dx index c6befea90..03894c331 100644 --- a/examples/tutorial.dx +++ b/examples/tutorial.dx @@ -88,7 +88,8 @@ include "plot.dx" ' `y = [1.0 for j in range(width) for i in range(height)]` ' The analogous table construct in Dex is written in the following form. It - produces a one-dimensional table of `Height x Width` elements. + produces a one-dimensional table of `Height x Width` elements. Here `&` + indicates a tuple constructor. y = for (i, j) : (Height & Width) . 1.0 @@ -140,6 +141,7 @@ row = x.(3 @ Height) ' Another consequence is that you cannot use indices as integers. It is necessary to explicitly annotate index types with `ordinal`. + This is because finite sets i.e. `Fin` are not closed under addition. :t for i:Height. for j:Width. i + j From 11168894b29655b090195682a40e2e9ccef234f9 Mon Sep 17 00:00:00 2001 From: Dan Zheng Date: Fri, 15 Jan 2021 02:43:48 -0500 Subject: [PATCH 13/14] Stylistic edits. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Consistent space: no triple newline. - Spell out `tabXX` function names to `tableXX`. - Rename dummy `Add`` and `VSpace`` interface requirements. - Prevents clash with Prelude interfaces and requirements of the same name. - Rename title: "Dex Tutorial" → "Introduction to Dex" - Fix English typos. --- examples/tutorial.dx | 157 ++++++++++++++++++------------------------- 1 file changed, 65 insertions(+), 92 deletions(-) diff --git a/examples/tutorial.dx b/examples/tutorial.dx index 03894c331..cfc351daa 100644 --- a/examples/tutorial.dx +++ b/examples/tutorial.dx @@ -1,4 +1,4 @@ -'# Dex Tutorial +'# Introduction to Dex ' Dex is a functional, statically typed language for array processing. There are many tools for array processing, from @@ -11,8 +11,6 @@ MATLAB students are told repeatedly to "avoid for loops". *Dex gives for loops back*. - - '## Table comprehensions ' Let us begin with the most useful component of Dex, the `for` @@ -39,7 +37,6 @@ x :t x - ' 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 enumeration variable. @@ -147,8 +144,8 @@ row = x.(3 @ Height) :t for i:Height. for j:Width. (ordinal i) + (ordinal j) -' If we want to convert these to floats we do it manually with the IToF function. - We can use to this to make an image gradient. +' 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 @@ -177,7 +174,6 @@ for pair:(Fin 2 & Fin 3). ordinal pair ' Again, we rely on type inference in order to avoid explicitly spelling the ranges. - ' ## Defining functions over tables ' One use case of packing and unpacking table indices is that it allows us to @@ -190,7 +186,6 @@ for pair:(Fin 2 & Fin 3). ordinal pair :t mean y - ' The `mean` function works independently of the index type of the table. ' Let's see how we can define our own table functions. Defining a function in @@ -208,17 +203,16 @@ add5 1.0 :t add5 - ' 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" to tables with _any_ index type. This is possible by declaring an `n => Int32` table argument type: this declares the type variable `n` as the index type of the table argument. -def tabAdd5 (x : n => Float32) : n => Float32 = +def tableAdd5' (x : n => Float32) : n => Float32 = for i. x.i + 5.0 -:t tabAdd5 y +:t tableAdd5' y ' 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 @@ -234,21 +228,19 @@ def transFloat (x : m => n => Float32) : n => m => Float32 = def trans (x : m => n => v) : n => m => v = for i. for j. x.j.i - ' We can also use this to check for shape errors: :t x -def tabAdd (x : m => n => Float32) (y : m => n => Float32) : m => n => 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 tabAdd x x +:t tableAdd' x x -:t tabAdd x (trans x) +:t tableAdd' x (trans x) ' The type system checked for us that the input tables indeed have the same shape. - '## Case Study: MNist ' To run this section, move the following binary files to examples: @@ -257,7 +249,6 @@ def tabAdd (x : m => n => Float32) (y : m => n => Float32) : m => n => Float32 = ' `wget https://github.com/srush/learns-dex/raw/main/labels.bin` - ' 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 each with a fixed size. @@ -345,7 +336,6 @@ im2 : Fin 4 => Fin 4 => Fin 7 => Fin 7 => Float32 = imtile ims.(0@_) :html matshow (sum (sum im2)) - '## Writing Loops ' Dex is a functional language - but when writing mathematical algorithms, @@ -371,20 +361,17 @@ im2 : Fin 4 => Fin 4 => Fin 7 => Fin 7 => Float32 = imtile ims.(0@_) the `State` effect, which provides getter and setter functionality (via `get` and `:=` assignment). Here's what it looks like: -def tabMean (x : n => Float32) : Float32 = - +def tableMean (x : n => Float32) : Float32 = -- acc = 0 withState 0.0 $ \acc. - -- for i in range(len(x)) for i. -- acc = acc + x[i] acc := (get acc) + x.i - -- return acc / len(x) (get acc) / (IToF (size n)) -tabMean [0.0, 1.0, 0.5] +:p tableMean [0.0, 1.0, 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 @@ -397,13 +384,13 @@ tabMean [0.0, 1.0, 0.5] `(f x)` when it is inconvenient to write them. For example, the following two expressions are identical: -:t tabMean (y + y) +:t tableMean (y + y) -:t tabMean $ y + y +:t tableMean $ y + y ' 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 - (i.e. closure). In `tabMean` above: the lambda takes an argument named `acc` + (i.e. closure). In `tableMean` above: the lambda takes an argument named `acc` and returns the body, which is the expression following the `.` (a `for` constructor in this case). @@ -411,7 +398,6 @@ tabMean [0.0, 1.0, 0.5] (\ x. x + 10) 20 - ' That leaves: `withState`. This function uses the `State` effect, enabling us to introduce imperative variables into the computation. `withState` takes an initial value `init` and a body function taking a @@ -442,116 +428,108 @@ withState 10 $ \ state. Reading the value in `ref` is possible via the `get` function. or via using the final result returned by `withState`. -'## Typeclasses +'## Interfaces -' Our `tabMean` function is pretty neat. It lets us work with tables with any - index type and computes the sum. However, `tabMean` explicitly takes only +' Our `tableMean` function is pretty neat. It lets us work with tables with any + index type and computes the sum. However, `tableMean` explicitly takes only integer tables (of type `n => Float32`). -:t tabMean +:t tableMean -' If we try to apply `tabMean` to other types for get errors. For example, what if - we have a table of pairs of floats, the function does not work. +' 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)) -tabMean (for (i, j). (x.i.j, x.i.j)) - -' Intuitively this seems like it could work. We just need to be able to - add and divide pairs. Let's look a bit close at the types of add and - divide. +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 (+) :t (/) +' 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. -' These types are a bit complex. Add maps `a -> a -> a` with a constraint that - `a` be in the type class `Add`. Whereas divide maps `a -> Float32 -> a` - where `a` is in the type class `VSpace`. +' 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 type class interfaces are - defined as: +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 +' *Interfaces* define *requirements*: the functions needed for a type to + implement the interface (via an *instance*). -interface [Add a] VSpace a - scaleVec : Float -> a -> a +' Here is an `Add'` instance for the float pair type: -' They tell us which functions we need to define for a type to work with them. - It it relatively straightforward to add a new instance. +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) -' Here is an interface for adding float pairs. +' And here is a `VSpace'` 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 VSpace' (Float32 & Float32) + scaleVec' = \s (x, y). (x / s, y / s) -' And dividing a float pair by a constant. +' Once we have these two instance definitions, we can revisit our table sum + function using them: -instance VSpace (Float32 & Float32) - scaleVec = \s (x, y). (x / s, y / s) - -' Once we have these two instance definitions (`MyAdd Int32` and - `MyAdd Float32`), we can revisit our table sum function and add a typeclass - constraint: - -def tabMean2 [VSpace v] (x : n => v) : v = - withState zero $ \acc. +def tableMean' [Add' v, VSpace' v] (x : n => v) : v = + z: v = zero' + yieldState z $ \acc: (Ref _ v). for i. - acc := (get acc) + x.i - (get acc) / (IToF (size n)) + acc := add' (get acc) x.i -- `Add'` requirement + scaleVec' (IToF (size n)) (get acc) -- `VSpace'` requirement -tabMean2 [0.1, 0.5, 1.0] +tableMean' [0.1, 0.5, 1.0] -tabMean2 [(1.0, 0.5), (0.5, 0.8)] +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 +' tuple types. -' To be more general, we could have also defined these instance for all 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 [VSpace v, VSpace w] VSpace (v & w) - scaleVec = \s (x, y). (x / s, y / s) +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) '## More MNist - ' Now that we has more functions we can revisit some of the 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 get acc -' Plot how many times each pixel value occurs in an image +' Plot how many times each pixel value occurs in an image: hist = bincount $ for (i,j). (FToI (ims.(0 @ _).i.j + 1.0) @Pixels) :t hist :html showPlot $ yPlot (for i. (IToF hist.i)) -' Find nearest images in the dataset. - +' Find nearest images in the dataset: def imdot (x : m=>n=>Float32) (y : m=>n=>Float32) : Float32 = sum for (i, j). x.i.j * y.i.j @@ -567,10 +545,8 @@ double = for b i j. [ims.b.i.j, ims.(nearest.b).i.j, 0.0] :html imseqshow double - '## Variable Length Lists - ' So far all the examples have assumed that we know the exact size of our tables. This is a common assumption in array languages, but @@ -612,7 +588,6 @@ def findFives (x : a=>b) (y : a=>Class) : List b = True -> AsList _ [x.i] False -> mempty - ' Note though that the type here does not tell us how many 5's there are. The type system cannot know this. To figure it out we need to unpack the list. @@ -628,10 +603,8 @@ nFives :html matshow (sum fives) - '## Conclusion - ' We hope this gives you enough information to start playing with Dex. This is just a start though of the different functionality available in the language. If you are interested in continuing to learn, we recommend From d7e872fac030e84ad670bb7bb74507ee435251d3 Mon Sep 17 00:00:00 2001 From: srush Date: Tue, 19 Jan 2021 17:24:15 -0500 Subject: [PATCH 14/14] delete trailing whitespace --- examples/tutorial.dx | 48 ++++++++++++++++++++++---------------------- 1 file changed, 24 insertions(+), 24 deletions(-) diff --git a/examples/tutorial.dx b/examples/tutorial.dx index cfc351daa..48a10fb41 100644 --- a/examples/tutorial.dx +++ b/examples/tutorial.dx @@ -86,7 +86,7 @@ include "plot.dx" ' The analogous table construct in Dex is written in the following form. It produces a one-dimensional table of `Height x Width` elements. Here `&` - indicates a tuple constructor. + indicates a tuple constructor. y = for (i, j) : (Height & Width) . 1.0 @@ -116,7 +116,7 @@ mean y r = x.3 ' Instead, it is necessary to cast the integer into the index type of the - current shape. This type annotation is done with the `@` operator. + current shape. This type annotation is done with the `@` operator. :t x @@ -128,7 +128,7 @@ row = x.(3 @ Height) ' 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. + did not provide and explicit type annotation. :t row.(5 @ _) @@ -159,7 +159,7 @@ gradient = for i:Height. for j:Width. IToF ((ordinal i) + (ordinal j)) :t y.(3 @ Height, 5 @ Width) -' Tuple indices also provide an ordinal value. +' Tuple indices also provide an ordinal value. for pair:(Fin 2 & Fin 3). ordinal pair @@ -189,7 +189,7 @@ for pair:(Fin 2 & Fin 3). ordinal pair ' The `mean` function works independently of the index type of the table. ' Let's see how we can define our own table functions. Defining a function in - Dex uses the following syntax. + Dex uses the following syntax. def add5 (x:Float32) : Float32 = x + 5.0 @@ -218,12 +218,12 @@ def tableAdd5' (x : n => Float32) : n => Float32 = are statically known, type checking can ensure that table arguments have valid dimensions. This is "shape safety". -' Imagine we have `transpose` function. We can encode the shape change in the type. +' Imagine we have `transpose` function. We can encode the shape change in the type. def transFloat (x : m => n => Float32) : n => m => Float32 = for i. for j. x.j.i -' We can even make it more generic by abstracting over the value type. +' We can even make it more generic by abstracting over the value type. def trans (x : m => n => v) : n => m => v = for i. for j. x.j.i @@ -264,7 +264,7 @@ Full = Fin ((size Batch) * (size IHeight) * (size IWidth)) ' To do this we will use Dex's IO to load some images from a file. This section uses features outside the scope of the tutorial, so you can - ignore it for now. + ignore it for now. def pixel (x:Char) : Float32 = r = W8ToI x @@ -272,7 +272,7 @@ def pixel (x:Char) : Float32 = True -> (abs r) + 128 False -> r -def getIm : Batch => Image = +def getIm : Batch => Image = (AsList _ im) = unsafeIO do readFile "examples/mnist.bin" raw = unsafeCastTable Full im for b: Batch i j. @@ -311,9 +311,9 @@ imscolor = for i. for j. for c:Channels. ims.((ordinal c)@_).i.j ' This one shows all the images on one channel over the base plot. imscolor2 = for b. for i. for j. for c:Channels. - case ordinal c == 0 of + case ordinal c == 0 of True -> (sum ims).i.j / (IToF (size Batch)) - False -> ims.b.i.j + False -> ims.b.i.j :html imseqshow (imscolor2 / 255.0) @@ -324,7 +324,7 @@ imscolor2 = for b. for i. for j. for c:Channels. def split (x: m=>v) : n=>o=>v = for i j. x.(ordinal (i,j)@_) - + def imtile (x: a=>b=>v) : n=>o=>p=>q=>v = for kh kw h w. (split (split x).h.kh).w.kw @@ -362,15 +362,15 @@ im2 : Fin 4 => Fin 4 => Fin 7 => Fin 7 => Float32 = imtile ims.(0@_) and `:=` assignment). Here's what it looks like: def tableMean (x : n => Float32) : Float32 = - -- acc = 0 + -- acc = 0 withState 0.0 $ \acc. -- for i in range(len(x)) for i. -- acc = acc + x[i] acc := (get acc) + x.i -- return acc / len(x) - (get acc) / (IToF (size n)) - + (get acc) / (IToF (size n)) + :p tableMean [0.0, 1.0, 0.5] ' So, even though Dex is a functional language, it is possible to write loops @@ -396,7 +396,7 @@ def tableMean (x : n => Float32) : Float32 = :t \ x. x + 10 -(\ x. x + 10) 20 +(\ x. x + 10) 20 ' That leaves: `withState`. This function uses the `State` effect, enabling us to introduce imperative variables into the computation. @@ -456,7 +456,7 @@ 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: interface Add' a add' : a -> a -> a @@ -551,7 +551,7 @@ double = for b i j. [ims.b.i.j, ims.(nearest.b).i.j, 0.0] know the exact size of our tables. This is a common assumption in array languages, but it makes some operations surprisingly difficult - to do. + to do. ' For instance, we might want to filter our set of images to only allow for images of 5's. But what is @@ -568,10 +568,10 @@ AsList _ $ for i:Height. 0.0 :t AsList _ $ for i:Height. 0.0 ' Tables of lists can be concatenated down to - single lists. + single lists. z = concat [AsList _ [3.0], - AsList _ [1.0, 2.0 ]] + AsList _ [1.0, 2.0 ]] z ' And they can be deconstructed to fetch a new table. @@ -581,7 +581,7 @@ temptab ' Using this construct we can return to extracting the 5's from the image set. Here `mempty` is - synonymous with `AsList _ []`. + synonymous with `AsList _ []`. def findFives (x : a=>b) (y : a=>Class) : List b = concat for i. case (y.i == (5 @ _)) of @@ -590,9 +590,9 @@ def findFives (x : a=>b) (y : a=>Class) : List b = ' Note though that the type here does not tell us how many 5's there are. The type system cannot know this. - To figure it out we need to unpack the list. + To figure it out we need to unpack the list. -temp = findFives all_ims all_labels +temp = findFives all_ims all_labels (AsList nFives fives) = temp nFives @@ -615,7 +615,7 @@ nFives ' Here are some topics to check out in the Prelude: ' * Randomness and Keys - * Laziness of For Comprehensions + * Laziness of For Comprehensions * Records and Variant Types * File IO * Effects Beyond State