From 3bcda8521174bc5752a4a34f12145d7e35624096 Mon Sep 17 00:00:00 2001 From: srush Date: Fri, 8 Jan 2021 20:21:26 -0500 Subject: [PATCH 1/9] 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 0dab3fa21fe6211977477b78381a65612a447e90 Mon Sep 17 00:00:00 2001 From: Dan Zheng Date: Sat, 9 Jan 2021 00:01:41 -0500 Subject: [PATCH 2/9] 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 c3f6a10b111bee0bb19cd7ece231e92f539928b2 Mon Sep 17 00:00:00 2001 From: Dan Zheng Date: Sat, 9 Jan 2021 00:02:58 -0500 Subject: [PATCH 3/9] 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 f7459d64c187e436d421f5fbdba5bc60197203b4 Mon Sep 17 00:00:00 2001 From: Dan Zheng Date: Sat, 9 Jan 2021 01:07:47 -0500 Subject: [PATCH 4/9] 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 f521e306328f74cf4a36cb80c1ccd56f84f16119 Mon Sep 17 00:00:00 2001 From: Dan Zheng Date: Sat, 9 Jan 2021 03:38:23 -0500 Subject: [PATCH 5/9] 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 1288790aac9760a14ed16c0948fb6b7ed98d7f81 Mon Sep 17 00:00:00 2001 From: Dan Zheng Date: Sat, 9 Jan 2021 09:25:58 -0500 Subject: [PATCH 6/9] 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 2476af79e83047d7a18b89c94be3472792bda912 Mon Sep 17 00:00:00 2001 From: srush Date: Sat, 9 Jan 2021 10:51:53 -0500 Subject: [PATCH 7/9] 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 ad7f9328177dd8c12d808481a15d5fdab75d11f5 Mon Sep 17 00:00:00 2001 From: srush Date: Sat, 9 Jan 2021 19:53:14 -0500 Subject: [PATCH 8/9] 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 3c1d9f23f32831b0a5af245a3fb00770f60b534f Mon Sep 17 00:00:00 2001 From: srush Date: Sat, 9 Jan 2021 21:24:05 -0500 Subject: [PATCH 9/9] 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