google-research/dex-lang

Research language for array processing in the Haskell/ML family

Dex

Dex (named for "index") is a research language for typed, functional array processing. The goal of the project is to explore:

• Type systems for array programming
• Mathematical program transformations like differentiation and integration
• User-directed compilation to parallel hardware
• Interactive and incremental numerical programming and visualization

To learn more, check out our paper, our tutorial or these example programs:

• Dex prelude
• Mandelbrot set
• Ray tracer
• Estimating pi
• Hamiltonian Monte Carlo
• ODE integrator
• Sierpinski triangle
• Basis function regression
• Brownian bridge
• Dynamic programming (Levenshtein distance)
• Molecular dynamics simulation

Or for a more comprehensive look, there's

• The InDex of all documents, libraries, and examples included in this repository.

🚨 Dex is an experimental research project at an early stage of development. Expect monstrous bugs and razor-sharp edges!

🤝 Contributions welcome! See our issue tracker for good first issues, or browse by thematic labels.

Dependencies

• Install stack
• Install LLVM 12
  • Ubuntu/Debian: apt-get install llvm-12-dev
  • macOS: brew install llvm@12
    • Make sure llvm@12 is on your PATH before building. Example: export PATH="$(brew --prefix llvm@12)/bin:$PATH"
• Install clang 12 (may be installed together with llvm)
  • Ubuntu/Debian: apt-get install clang-12
  • macOS: installs with llvm
• Install libpng (often included by default in *nix platforms)
  • Ubuntu/Debian: apt-get install libpng-dev
  • macOS: brew install libpng

Installing

To build and install a release version of Dex run make install.

The default installation directory is $HOME/.local/bin, so make sure to add that directory to $PATH after installing Dex. To install Dex somewhere else, set the PREFIX environment variable before running make install. For example, PREFIX=$HOME make install installs dex in $HOME/bin.

Building

• Build Dex in development (unoptimized) mode: make
• Run tests in development mode: make tests

It is convenient to set up a dex alias (e.g. in .bashrc) for running Dex in development mode:

# Linux:
alias dex="stack exec dex -- --lib-path lib"

# macOS:
alias dex="stack exec --stack-yaml=stack-macos.yaml dex -- --lib-path lib"

You might also want to consider other development build targets:

• build-opt for local optimized builds,
• build-dbg for local debug builds,
• build-prof for local optimized builds with profiling enabled.

Those non-standard targets require different aliases. Please consult the documentation at the top of the makefile for detailed instructions.

Haskell Language Server

In order to use HLS with the Haskell code in this project:

• Install ghcup
• Run ghcup install hls
• Create a file in the root dex directory called hie.yaml with the following contents:

cradle:
  stack:
    stackYaml: "./stack-macos.yaml"  # Or stack.yaml if not on MacOS

Unfortunately one cannot dynamically select the stack.yaml file to use based on the environment, and so one has to create an appropriate hie.yaml file manually. This will be ignored by git.

This should work out of the box with Emacs' lsp-haskell package.

Building with Nix

Nix is a functional package manager and build system.

To build with vanilla Nix:

$ nix-build

To build with flakes-enabled Nix:

$ nix build .#dex

The resulting dex binary should be in result/bin/dex.

For development purposes, you can use a Nix environment with

$ nix-shell
$ nix develop  # With flakes

and use make to use Stack to build Dex.

Running

• Traditional REPL: dex repl
• Execute script: dex script examples/pi.dx
• Live-updated notebook display dex web examples/pi.dx (html) or dex watch examples/pi.dx (terminal).

License

BSD-3

This is an early-stage research project, not an official Google product.

dex-lang's Issues

A composition operator

In #35

@dougalm said:

This is calling out for a composition operator. I'm tempted to co-opt o for composition. Haskell uses . but we're already overloading that in a few places. Then we could write neg o f instead of defining a separate negf.

@oxinabox said

Yes.
Julia uses ∘, and endowers the REPL (and all text editors via plugins) with ability to type that as \circ tab
Could be interresting here.
Could go with something like ($) or $$

---

Making this an issue so it doesn't get lost.

mandelbrot.dx demo is currently broken

Somewhere between 9877efb and fd2c8ac, the mandelbrot.dx demo became broken somehow. It currently looks like this for me:

If I reduce the number of iterations to 50, it starts looking more correct:

Unfortunately quite a lot changed between the last commit where it worked and the first commit where it failed, so I haven't been able to track down what's causing the problem. Frustratingly, the individual operations in the example all seem to work as expected. I've been wondering if there's some small floating-point error or similar that might be causing it.

btw: It might be convenient to validate this example's output in the tests if, after displaying the 300x200 matrix, it was evaluated over a smaller number of elements (say 7x5) and then dumped using :p.

Function redefinition is ignored

Fresh build today, using the REPL:

It said it redefined, but it did not

>=> f :: Real -> Real
... f x = 2.0*x

>=> f 2.3
4.6
>=> f :: Real -> Real
... f x = 3.0*x
Variable redefined: f
>=> f 2.3
4.6

Please print all floating-point digits

>=> 3.14159265
3.1415927

Sadness.

Dex represents floating-point numbers internally in Double precision, and AFAICT correctly parses inputs as such, but truncates to single precision on output here. That was clearly done intentionally, but I think that choice should be revisited.

I see the rationales for printing all available digits to be as follows:

• Read-print and print-read invariance are desirable on general principle, and floating-point numbers need not violate them.
• In particular, the print-read invariance property test currently fails on doubles.
• Loss of information on print can be very confusing when trying to debug a program.

As an example of the consequences of not printing everything, this can happen:

>=> y > x
True
>=> [y, x]
[1.0, 1.0]
-- !!?

It's not even very hard to arrange:

>=> x = 0.99999999

>=> y = 1.0

Presumably the desideratum on the other side is avoiding overwhelming the user with excess or unwarranted precision, and also arranging for neat tabular output. The latter can be arranged without loss of information, by padding to enough digits.

Trouble when indexing into a table of tuples of tables

Reduced from the expression generator

[(pi, (for c::4 . 5))].(%asidx(1))

produces

Compiler bug!
Please report this at github.com/google-research/dex-lang/issues

Not implemented: (afor  c::4 . 
    5)
CallStack (from HasCallStack):
  error, called at src/lib/Imp.hs:104:8 in dex-0.1.0.0-929S7EHOUuk4iExhj4Ea4l:Imp
CallStack (from -prof):
  Imp.toImpAtom (src/lib/Imp.hs:(100,1)-(104,49))
  Imp.toImp (src/lib/Imp.hs:(49,1)-(75,48))
  Imp.impPass.\ (src/lib/Imp.hs:(30,30)-(42,2))
  Imp.impPass.liftTop (src/lib/Imp.hs:(44,5)-(46,38))
  Imp.impPass (src/lib/Imp.hs:(30,1)-(46,38))
  Pass.>+>.\ (src/lib/Pass.hs:(42,51)-(50,11))
  Cat.liftIO (src/lib/Cat.hs:26:54-60)
  Cat.>>= (src/lib/Cat.hs:26:35-39)
  Pass.>+> (src/lib/Pass.hs:(42,1)-(50,11))
  Main.fullPassJit (src/dex.hs:(51,1)-(56,21))
  Cat.runCatT (src/lib/Cat.hs:(80,1)-(82,22))
  Pass.runTopPassM (src/lib/Pass.hs:37:1-46)
  Pass.runFullPass (src/lib/Pass.hs:(32,1)-(34,49))
  System.Console.Haskeline.MonadException.controlIO.\.\.run' (System/Console/Haskeline/MonadException.hs:151:21-81)
  System.Console.Haskeline.MonadException.catch.\ (System/Console/Haskeline/MonadException.hs:(98,49)-(100,67))
  System.Console.Haskeline.MonadException.controlIO.\.\ (System/Console/Haskeline/MonadException.hs:(150,62)-(152,55))
  System.Console.Haskeline.MonadException.controlIO (System/Console/Haskeline/MonadException.hs:139:5-49)
  System.Console.Haskeline.MonadException.controlIO.\ (System/Console/Haskeline/MonadException.hs:(150,34)-(152,55))
  System.Console.Haskeline.MonadException.controlIO (System/Console/Haskeline/MonadException.hs:(150,5)-(152,55))
  System.Console.Haskeline.MonadException.catch (System/Console/Haskeline/MonadException.hs:(98,1)-(100,67))
  Main.evalDecl (src/dex.hs:(71,1)-(76,12))
  Main.evalFile (src/dex.hs:(83,1)-(87,35))
  Main.runMode.runEnv (src/dex.hs:61:7-33)
  Main.runMode (src/dex.hs:(59,1)-(68,42))
  Main.main (src/dex.hs:(160,1)-(164,76))

Interestingly, subexpressions of this execute fine.

Crash out from showing index

Similar to #17 I think, but this one still crashes

can get it from asidx

>=> kk::4 = asidx 4

>=> kk
dex: can't show 4
CallStack (from HasCallStack):
  error, called at src/lib/Imp.hs:176:12 in dex-0.1.0.0-9pQ6aTLha3fLdCjkbXPWRy:Imp

Can also get it out of for

>=> v = for ii::4 . ii

>=> v
dex: can't show 4
CallStack (from HasCallStack):
  error, called at src/lib/Imp.hs:176:12 in dex-0.1.0.0-9pQ6aTLha3fLdCjkbXPWRy:Imp

In both cases it fully crashes out to the shell

Trouble running script

When I try to run dex script foo it always prints

When using the script command, you must provide a resolver argument
On the terminal screen and then does nothing.
What's the correct syntax for running scritps with dex?
(Also maybe a related doubt, but what's the difference between .cd and .dx files?)

Syntax Change / Problem?

I am trying out the tutorial.

Oddly, I see this in the REPL:

>=> f = lam z. x + z * y
Error: variable not in scope: lam

I'd appreciate any help.

Variable names are not reusuable, even if an error prevented them getting defined

Lets say I made a typo when assigning a value to a variable.
And so I get an error saying something on the RHS is not valid.

If I want to go and assign it again, I get an error saying that my variable has already been defined.

>=> x = 1 + 1
Type error:
Expected: Real
  Actual: Int
In: 1

x = 1 + 1
    ^^

>=> x
Error: variable not in scope: x
>=> x = 1.0 + 1.0
Error: variable already defined: x
>=> x
Error: variable not in scope: x

I am down with not allowing variables to be redefined.
But I don't think erroring should count as defining.

I am thinking that the flag to mark a variable as defined or not needs to occur after it is determined that the RHS did not error.

matmul

It would be nice to have matrix multiplication defined.
Or possibly an interface for tensor-contractor / einsum.

I am assuming one does not want too do that inside Dex itself,
as it wants to hit some BLAS.
(or what ever XLA is doing in this space)

Reading off the end of a table

[1].(%asidx(9))

runs, and emits various interesting numbers, like 0, 18, 22, 183385288, and 139624557584448. This should be at least a runtime error (though, for the literal case, compile-time might be nicer).

I am amused that the behavior is well-typed, e.g.

[(for c::4 . 5)].(%asidx(9))

emits things like [179572448, 179571328, 4810363372640, 179613120],
[162423056, 162421936, 4810363372640, 162141280], [1, 0, 0, 145], etc.

repeated inlinings?

In the simplify pass, it seems the rhs of the definition will be processed at every occurrence site? For example:

:simp (arr = for i::2 . 0; (arr, arr))
(tab::2=>Int = (for  i::2 . 
    0);
(tab_1::2=>Int = (for  i::2 . 
    0);
(tab, tab_1)))

Instead of creating one array, the program ends up constructing two after simplify pass? This will also cause exponential inlinings?

:simp (arr = (arr2 = for i::2 . 1; (arr2, arr2)); (arr, arr))
(tab::2=>Int = (for  i::2 . 
    1);
(tab_1::2=>Int = (for  i::2 . 
    1);
(tab_2::2=>Int = (for  i::2 . 
    1);
(tab_3::2=>Int = (for  i::2 . 
    1);
(tab, tab_1, tab_2, tab_3)))))

Is array printing broken?

This could be me having a bad LLVM build some how.

But it seems lilke I can't :p an array.

~/dex-lang(git✱≠master)❱ ✘ ❱ stack --  exec dex repl
>=> c = [1, 2, 3]

>=> :p c
Assertion failed: ((i >= FTy->getNumParams() || FTy->getParamType(i) == Args[i]->getType()) && "Calling a function with a bad signature!"), function init, file /Users/oxinabox/progmisc2/llvm/llvm-8.0.0.src/lib/IR/Instructions.cpp, line 379.
fish: 'stack --  exec dex repl' terminated by signal SIGABRT (Abort)

There are examples of this working in the tuitorial.

include seems not to be bringing things into scope

I was working on another example and I wanted to use the PSO optimize function.
So I did:

include "examples/particle-swarm-optimizer.dx"

and that caused a bunch of text to show-up in my output (i think all the :p print statements).
so I figured it was working

but when I tried to call optimize
I got: Error: variable not in scope: optimize

cf #40

Whitespace at start of function signature is a parse error

>=>  foo :: x -> x
Parse error:1:2:
  |
1 |  foo :: x -> x
  |  ^^
unexpected "fo"
expecting ".." or end of line

Slicing?

Been trying to knot my way through getting something akin to slicing through filters and existentials.

But can't get past the need to create a range that's somehow convertible to an index set. Or put differently, a way to get an E n from a dynamic input j.

Attempts:

slice :: Int -> Int -> (E k. k=>(n=>Real -> Real))
slice i j =
rr = filter (lam k. and (ge k i) (lt k j)) iota @n -- No `ge` or `lt` :(((
for k. ki = rr.k; lam a. a.(asidx ki)

Should anything, besides the absence of comparators (ge, lt), make this not work?

Trouble building on Mac

I get part-way through the make set and I hit an error relating to hinotify-0.4

attoparsec          > [21 of 21] Compiling Data.Attoparsec
attoparsec          > copy/register
attoparsec          > Installing library in /Users/oxinabox/.stack/snapshots/x86_64-osx/19f92992da84ddd872e7f776ca44f
7ddcdce0f7b17815902723d4090d435093e/8.6.5/lib/x86_64-osx-ghc-8.6.5/attoparsec-0.13.2.2-6XZWdvg7dAKGuzy18iXIM3
attoparsec          > Registering library for attoparsec-0.13.2.2..

--  While building package hinotify-0.4 using:
      /Users/oxinabox/.stack/setup-exe-cache/x86_64-osx/Cabal-simple_mPHDZzAJ_2.4.0.1_ghc-8.6.5 --builddir=.stack-wor
k/dist/x86_64-osx/Cabal-2.4.0.1 configure --user --package-db=clear --package-db=global --package-db=/Users/oxinabox/
.stack/snapshots/x86_64-osx/19f92992da84ddd872e7f776ca44f7ddcdce0f7b17815902723d4090d435093e/8.6.5/pkgdb --libdir=/Users/oxinabox/.stack/snapshots/x86_64-osx/19f92992da84ddd872e7f776ca44f7ddcdce0f7b17815902723d4090d435093e/8.6.5/lib -
-bindir=/Users/oxinabox/.stack/snapshots/x86_64-osx/19f92992da84ddd872e7f776ca44f7ddcdce0f7b17815902723d4090d435093e/
8.6.5/bin --datadir=/Users/oxinabox/.stack/snapshots/x86_64-osx/19f92992da84ddd872e7f776ca44f7ddcdce0f7b17815902723d4
090d435093e/8.6.5/share --libexecdir=/Users/oxinabox/.stack/snapshots/x86_64-osx/19f92992da84ddd872e7f776ca44f7ddcdce
0f7b17815902723d4090d435093e/8.6.5/libexec --sysconfdir=/Users/oxinabox/.stack/snapshots/x86_64-osx/19f92992da84ddd87
2e7f776ca44f7ddcdce0f7b17815902723d4090d435093e/8.6.5/etc --docdir=/Users/oxinabox/.stack/snapshots/x86_64-osx/19f929
92da84ddd872e7f776ca44f7ddcdce0f7b17815902723d4090d435093e/8.6.5/doc/hinotify-0.4 --htmldir=/Users/oxinabox/.stack/sn
apshots/x86_64-osx/19f92992da84ddd872e7f776ca44f7ddcdce0f7b17815902723d4090d435093e/8.6.5/doc/hinotify-0.4 --haddockd
ir=/Users/oxinabox/.stack/snapshots/x86_64-osx/19f92992da84ddd872e7f776ca44f7ddcdce0f7b17815902723d4090d435093e/8.6.5
/doc/hinotify-0.4 --dependency=async=async-2.2.2-EbxQ7tk0OFk9dJNMtaidSf --dependency=base=base-4.12.0.0 --dependency=
bytestring=bytestring-0.10.8.2 --dependency=containers=containers-0.6.0.1 --dependency=unix=unix-2.7.2.2 --exact-conf
iguration --ghc-option=-fhide-source-paths
    Process exited with code: ExitFailure 1
Progress 8/53
make: *** [all] Error 1

System Details:

~/ProgO/dex-lang(git:master)❱ ✘ ❱ llvm-config --version
7.1.0
~/ProgO/dex-lang(git:master)❱ ✔ ❱ stack --version
Version 2.1.3, Git revision 0fa51b9925decd937e4a993ad90cb686f88fa282 (7739 commits) x86_64 hpack-0.31.2
~/ProgO/dex-lang(git:master)❱ ✔ ❱

Segfaults on Mac

Since I synced on Thursday evening, about half the tests fail with segfault, as does the web interface. I also built a fresh pull of the current repo from scratch today but it has the same errors. Here's the output of make tests:

% make tests
rm -rf test-scratch/
mkdir -p test-scratch/
python3 misc/py/generate-dex-data.py
stack build
misc/check-quine examples/uexpr-tests.dx stack exec         dex -- script --allow-errors
OK
misc/check-quine examples/type-tests.dx stack exec         dex -- script --allow-errors
OK
misc/check-quine examples/eval-tests.dx stack exec         dex -- script --allow-errors
misc/check-quine: line 11: 53538 Segmentation fault: 11  ${@:2} $1 > $tmpout 2> $errout
misc/check-quine examples/shadow-tests.dx stack exec         dex -- script --allow-errors
OK
misc/check-quine examples/monad-tests.dx stack exec         dex -- script --allow-errors
OK
misc/check-quine examples/ad-tests.dx stack exec         dex -- script --allow-errors
OK
misc/check-quine examples/mandelbrot.dx stack exec         dex -- script --allow-errors
OK
misc/check-quine examples/pi.dx stack exec         dex -- script --allow-errors
OK
misc/check-quine examples/sierpinsky.dx stack exec         dex -- script --allow-errors
misc/check-quine: line 11: 53601 Segmentation fault: 11  ${@:2} $1 > $tmpout 2> $errout
misc/check-quine examples/regression.dx stack exec         dex -- script --allow-errors
misc/check-quine: line 11: 53609 Segmentation fault: 11  ${@:2} $1 > $tmpout 2> $errout
misc/check-quine examples/brownian_motion.dx stack exec         dex -- script --allow-errors
misc/check-quine: line 11: 53617 Segmentation fault: 11  ${@:2} $1 > $tmpout 2> $errout
misc/check-quine examples/particle-swarm-optimizer.dx stack exec         dex -- script --allow-errors
misc/check-quine: line 11: 53625 Segmentation fault: 11  ${@:2} $1 > $tmpout 2> $errout
misc/check-quine examples/ode-integrator.dx stack exec         dex -- script --allow-errors
misc/check-quine: line 11: 53633 Segmentation fault: 11  ${@:2} $1 > $tmpout 2> $errout
misc/check-quine examples/parser-tests.dx stack exec         dex -- script --allow-errors
OK
misc/check-quine examples/serialize-tests.dx stack exec         dex -- script --allow-errors
OK
misc/check-quine examples/tiled-matmul.dx stack exec         dex -- script --allow-errors
OK
misc/check-quine examples/mcmc.dx stack exec         dex -- script --allow-errors
misc/check-quine: line 11: 53674 Segmentation fault: 11  ${@:2} $1 > $tmpout 2> $errout
misc/check-no-diff \
	  examples/repl-multiline-test-expected-output \
	  <(stack exec         dex -- repl < examples/repl-multiline-test.dx)
OK

The latest commit that I had pulled when I first saw these errors on Thursday was the AD merge but since it's a segfault error maybe it was one of the earlier ones that day, perhaps the malloc_dex one or the OrcJIT one. Just guessing.

The only change I made to the repo before building is the one I always make, which is adding

+
+flags:
+  llvm-hs:
+    shared-llvm: false

to stack.yaml.

Can't write a prepend / concatenate function

I'm trying to prepend an element to sequence in such a way that I can iterate over them together, but

1. I'm not sure which of 3 approaches is most "Dex"y, and
2. None of those three approaches works right now.

Approach A: using product types

v = Fin 4
l = [3@v, 2@v, 3@v, 2@v]   -- The list
blank = 0@v           -- The thing I want to prepend

def prependA (m:Type) ?-> (v:Type) ?-> (blank:v) (seq: m=>v) : (v & m=>v) =
  (blank, seq)

s3 = prependA blank l
:p s3
(0@(Fin 4), [3@(Fin 4), 2@(Fin 4), 3@(Fin 4), 2@(Fin 4)])

So far so good! But I don't know how to iterate over this whole collection with a flat for loop:

:p for k. s3.k
Type error:
Expected: (a=>b)
  Actual: ((Fin 4) & ((Fin 4)=>(Fin 4)))
(Solving for: [a:Type, b:Type])

:p for k. s3.k
          ^^

Approach B: using dependent types

def prependB (n:Int) ?-> (blank:v) (seq: (Fin n)=>v) : (Fin (1 + n))=>v =
  for i. select (i == 0) blank blank  -- ignore implementation for now

which gives:

Type error:Can't reduce type expression: Fin (+) 1 n

def prependB (n:Int) ?-> (blank:v) (seq: (Fin n)=>v) : (Fin (1 + n))=>v =
                                                       ^^^^^^^^^^^^^^^^

Approach C: using sum types

I tried

def prependC (m:Type) ?-> (v:Type) ?-> (blank:v) (seq: m=>v) : (Unit|m)=>v =
  for idx. case idx
    Left () -> blank
    Right i -> seq.i

s3 = prependC blank l

crashed with

Not implemented Unit
CallStack (from HasCallStack):
  error, called at src/lib/Embed.hs:567:8 in dex-0.1.0.0-WMAsfoEK61B3EtpA608ix:Embed

Crash-out when showing Key

>=> newKey 1
dex: can't show Key
CallStack (from HasCallStack):
  error, called at src/lib/Imp.hs:202:12 in dex-0.1.0.0-9pQ6aTLha3fLdCjkbXPWRy:Imp

Unimplemented operation should not crashed

The program crashed after calling 2^10.

stack exec dex -- repl 
>=> 2^10 
dex: Primop not implemented: %pow 
CallStack (from HasCallStack):  
error, called at src/lib/JIT.hs:422:8 in dex-0.1.0.0-BmgK6CqjQc0JOcfO3y99YJ:JIT

I would be nice to have the REPL treats this as an error, not crashing the whole program.

SIGSEGV when interacting with array literals

On current master:

~/dex_b/round/dex-lang(git✱≠ox/PSO)❱ ✘ ❱ ./run_dex.fish
>=> :p [1.0, 2.0]
fish: 'stack exec dex -- repl --prompt…' terminated by signal SIGSEGV (Address boundary error)

should `(x, 1) = (4, 1)` work?

I was trying out what the tuitoral called tuple pattern-matching,
trying to see if it was just what
Javascript, and Julia and Python, etc call destructuring.

>=> (x,y)=(1, 2.0)

>=> x
1
>=> y
2.0
>=> (a,(b,c))=(1, (2.0, 3))

>=> a
1
>=> b
2.0
>=> c
3
>=> (z,1)=(10, 1)
Parse error:1:6:
  |
1 | (z,1)=(10, 1)
  |      ^^
unexpected "=("
expecting "#deriv", "- ", "::", '$', '*', '+', '.', '/', '<', '>', '^', end of input, end of line, or term

I thought (z,1)=(10, 1) might work, but it did not parse.

It would work with tuple-pattern matching in F#
see docs

I am not sure if either that should be fixed,
or if the tutorial should just be amended to say destructuring

Entering multi-line expressions in REPL

I thought I would copy-paste some of the examples in the tutorial into the REPL.
All the multiline ones seem to fail.
I moved them into a script and run the script and that works.

e.g.:

:p x = 1.                -- let binding
   y = (z = 2.; z + 1.)  -- let binding of a nested let expression
   ..                    -- escaped cosmetic line break
   x + y                 -- body of let expression

Results in:

>=> :p x = 1.                -- let binding
Parse error:2:1:
  |
2 | <empty line>
  | ^
unexpected end of input
expecting decl or expr

>=>    y = (z = 2.; z + 1.)  -- let binding of a nested let expression
Parse error:1:4:
  |
1 |    y = (z = 2.; z + 1.)  -- let binding of a nested let expression
  |    ^^
unexpected "y "
expecting ".." or end of line

>=>    ..                    -- escaped cosmetic line break
Parse error:2:1:
  |
2 | <empty line>
  | ^
unexpected end of input
expecting end of line

>=>    x + y                 -- body of let expression
Parse error:1:4:
  |
1 |    x + y                 -- body of let expression
  |    ^^
unexpected "x "
expecting ".." or end of line

Either I am doing something wrong,
or the REPL needs to try parsing when Enter is pressed
and if that fails du to unexpected end of input, it needs to continue to allow input.

allow expressions to be ended by end of file?

If one has a file that does not end with a new line then this is an error.

Example:

:p (1. + 2.) * 3.
Parse error:1:18:
  |
1 | :p (1. + 2.) * 3.
  |                  ^
unexpected end of input
expecting "--o", "->", "..", "..<", "<..", "<..<", "=>", '$', '-', '.', backquoted name, end of line, expression, or infix operator

The error message tells the truth, it was not expecting an end of input there, and putting in a end of line makes the code work,
but it is a otherwise complete expression.

Strange crashes when using tuple index sets

Some things work with tuple index sets, but other things don't.

For instance, array creation works, but printing fails:

>=> arr : ((Fin 10) & (Fin 3)) => Real = for idx. 1.0

>=> :p arr
dex: Not implemented: %fst (0@((Fin 10)) , 0@((Fin 3)))
CallStack (from HasCallStack):
  error, called at src/lib/Interpreter.hs:80:8 in dex-0.1.0.0-HJSwFDIBGLApX0gaH8Fs9:Interpreter

ordinal works, but fromOrdinal fails

>=> (0 @ (Fin 2), 0 @ (Fin 3))
(0@(Fin 2), 0@(Fin 3))
>=> :t (0 @ (Fin 2), 0 @ (Fin 3))
((Fin 2) & (Fin 3))
>=> ordinal (0 @ (Fin 2), 0 @ (Fin 3))
0
>=> 0 @ (Fin 2 & Fin 3)
dex: Cannot convert IVar ((:>) (Name GenName "v" 2) (IValType IntType)) to TC (PairType (TC (IntRange (Con (Lit (IntLit 0))) (Con (Lit (IntLit 2))))) (TC (IntRange (Con (Lit (IntLit 0))) (Con (Lit (IntLit 3))))))
CallStack (from HasCallStack):
  error, called at src/lib/Imp.hs:384:19 in dex-0.1.0.0-HJSwFDIBGLApX0gaH8Fs9:Imp

Allow linebreak (..) in type-signature line

It would be nice to be able to put line breaks in the type signature.

e.g.

apply2Net:: ((hz=>(iz=>Real), hz=>Real), (oz=>(hz=>Real), oz=>Real)) -> iz=>Real -> oz=>Real
apply2Net (layer1, layer2) input = 
    sigmoid $ applyAffine layer2 $ sigmoid $ applyAffine layer1 input

vs

apply2Net:: ( ..
    (hz=>(iz=>Real), hz=>Real), ..
    (oz=>(hz=>Real), oz=>Real)..
    )..
    -> iz=>Real ..
    -> oz=>Real
apply2Net (layer1, layer2) input = 
    sigmoid $ applyAffine layer2 $ sigmoid $ applyAffine layer1 input

This also showed up in
https://github.com/google-research/dex-lang/pull/33/files#diff-f3df4243876e24a9f40bddc8ba8ae4d9R67

Add missing LLVM libm intrinsics

It seems reasonably to follow up to #153
by adding in the rest of the LLVM intrinsics that overlap with libm.

Which are (last time i looked: JuliaMath/Libm.jl#8)

• exp2
• log10
• log2
• fabs (might be better to just implement in Dex? not like it is complicated)
• ceil (how did we end up with floor but not ceil ?)
• trunc (seems not that useful but 🤷)
• round, (maybe rint, nearbyint instead?)

Probably not maxnum, minnum, since hard to see how they would be any different to the ones we already have in Dex.

Dictionary inference not working for Eq

def is_equal (dict: Eq a) ?-> (v1:a) -> (v2:a) : Bool =
  v1 == v2

Gives

Type error:Couldn't synthesize a class dictionary for: Eq dict

modulo operation on negative number

A result mismatch of JIT and interpreter from the prop tests:

:p mod 3 -2
3

The interpreter gives the correct result: -1.

The urem operation here should be changed to the signed version srem? However, it's still not the modulo operator. Maybe renaming the function to rem instead?

Accidental branches

Here's a class of bugs uncovered by @jyh1's excellent property-based tester (#24).

Dex doesn't currently have if, and that's by design. If we had branches, then we couldn't do defunctionalization and AD without having sum types too, and that would substantially complicate the compiler. And in a SIMD world we're usually better off with a strict select instead of a real branch anyway.

But it turns out that Dex offers some accidental "join points" where you can deviously encode a branch. And the property-based tester is clever enough to find them. For example:

cond :: (() -> a) -> (() -> a) -> Bool -> a
cond f g p = [f, g].(asidx (b2i p)) ()

With the interpreter backend, this actually works. But in the compiler, it fails at defunctionalization, because it can't turn the table of functions [f, g] into a table of closures, since f and g can have different closures.

The proposed solution is to only allow non-function types in table constructors and similar places, like select and scan arguments. We can do this with a typeclass, Data, which admits everything except arrow types. This is the same typeclass we want anyway for things that can be serialized.

Note that we can still have tables of functions, like for i. lam x. ..., but they'll always consist of a single function body, so that they'll be lowerable to a table of closures.

Thanks to @axch for help thinking through this problem and the solution.

How to make comments on their own line

In previous versions of Dex .. -- comment worked.
But it seems like .. has stopped working in general lately.

Attempt 1 (failed)

foo:: Real->Real
foo x = 
    .. -- Now we compute foo
    2.0 * x

Parse error:5:5:
  |
5 |     .. -- Now we compute foo
  |     ^^^^^
unexpected ".. --"
expecting decl or expr
foo 0.5
Error: variable not in scope: foo

Attempt 2 (failed)

foo:: Real->Real
foo x = 
    -- Now we compute foo
    2.0 * x

Parse error:5:26:
  |
5 |     -- Now we compute foo
  |                          ^
unexpected "<newline>    "
expecting decl or expr

Attempt 3 (works but kinda ugly?)

foo:: Real->Real
foo x = ( 
    -- Now we compute foo
    2.0 * x
)

treat --o as a special case of -> ?

Consider a function defined with --o like neg

>=> neg2:: Real->Real
... neg2 x = -1.0 * x

>=> map neg2 [1.0, 2.0]
[-1.0, -2.0]
>=> map neg [1.0, 2.0]
Compiler bug!
Please report this at github.com/google-research/dex-lang/issues

App: (Real -> Real) != (Real --o Real)

Unexpected number of dests: 2%select

In the following example I think that minbyI (implemented using indexing),
and minbyS implemented using select
should have the same behavour.
but minbyS errrors when applied to tuples.

minbyI:: A a::Data. (a->Real)->a->a->a
minbyI f x y = [x,y].(asidx $ b2i $ (f x) > (f y))

minbyI sq -1.0 0.5
'0.5
minbyI fst (0.7, 1000.0) (3.0, 12.0)
'(0.7, 1000.0)

minbyS:: A a::Data. (a->Real)->a->a->a
minbyS f x y = select ((f x) < (f y)) x y

minbyS sq -1.0 0.5
' 0.5
minbyS fst (0.7, 1000.0) (3.0, 12.0)
' Compiler bug!
Please report this at github.com/google-research/dex-lang/issues

' Unexpected number of dests: 2%select
CallStack (from HasCallStack):
  error, called at src/lib/Imp.hs:112:31 in dex-0.1.0.0-9pQ6aTLha3fLdCjkbXPWRy:Imp

Can't use Unicode in function name?

What is this, 2003?

works

>=> s:: Real->Real
... s x = 1.0/(1.0 + exp (neg x))

>=> :p s 0.0
0.5

errors

>=> σ:: Real->Real
... σ x = 1.0/(1.0 + exp (neg x))
Parse error:2:1:
  |
2 | σ x = 1.0/(1.0 + exp (neg x))
  | ^
unexpected 'σ'
expecting 'Ã'

>=> :p σ 0.0
Error: variable not in scope: Ã

Weirdly the error message refers to Ã but the variable was σ.
I am guessing this is something like the input being read as Latin1 or something like that, rather than UTF8, as all modern things should be.

"Compiler bug" message when printing a lambda

>=> :p \x. x + 1.0
Compiler bug!
Please report this at github.com/google-research/dex-lang/issues

src/lib/TopLevel.hs:177:20-59: Non-exhaustive patterns in lambda

Admittedly, printing a lambda is a weird thing to do. But it seems like there could be a better error message here, and it seems like it's failing even before getting to the pretty printer.

Use : instead of :: for type declarations

I realize I'm bikeshedding, but I suggest changing type and index annotations from "::" to ":".

This blog post says "Haskell uses :: as the type operator. That was a mistake that costs us over 1 million characters of source code." and "Most other FP languages with types use :, including Scala, OCaml, Agda, Idris and Elm."

There's more discussion in this r/haskell discussion

:p linearize errors with CompilerBug

For example:

>=> f :: Real -> Real
... f x = 2.0 * x

>=> f 2.4
4.8
>=> linearize f
Compiler bug!Can't lower type to imp: (Real -> (Real, (Real -> Real)))
CallStack (from HasCallStack):
  error, called at src/lib/Imp.hs:121:8 in dex-0.1.0.0-EI9xXWhSqyj2zqWgzLwNt8:Imp
>=>

I believe this is as mentioned in the Prelude:

Vector spaces and automatic differentiation. Note that many of the following have implicit vector space typeclass constraints. For now these are not checked by the type checker.

But I figure I open an issue track, and so this is googleable by anyone running into this later

Allow trailing `,`

It would be nice to allow trainling commas in tuples and vectors.
Because it means one can have a convention of always using them,
which gives a consistent look to multiline lists.
and then moving code becomes easier,

=> [1, 2,]

Parse error:179:1:
    |
179 | <empty line>
    | ^^^^^^^
unexpected "<newline>[1, 2,"
expecting decl or expr

=> (1, 2,)

Parse error:182:7:
    |
182 | (1, 2,)
    |       ^^
unexpected ")<newline><newline><newline><newline>"
expecting term

More realizstic example:

netParams = ( ..
    initAffine @2 @60 (newKey 10), ..
    initAffine @60 @60 (newKey 30), ..
    initAffine @60 @60 (newKey 30), ..
    initAffine @60 @60 (newKey 30), ..
    initAffine @60 @1 (newKey 20), ..
)

Way to split code into multiple files

Per brief discussion at NeurIPS.
Sometime Input is not really IO,
In that it is deterministic, e.g. the loading of data.
So just code in another format, in another file.
This kind of input is thus actually more closely linked to metaprogramming than normal IO.

But right now, we can't actually load code in the Dex language, from another file. AFAIK.

I propose the additional of :include file/path.dx
as a command allowed to occur at top level.

Then I will do some metaprogramming in some other language (obs. Julia), in order to generate some Dex code that contains my data.
Which I will :include at the top of my script.

I don't want to put it directly in my script as it's probably going to be thousands of lines long.
Also I might want to regenerate it.

A possible generalisation of this would be includeby::(String->AST)->Path->Nothing
Which would take in a function to do the metaprogramming.
But I don't think we are anywhere near there yet?

:flops not producing any output

Consider:

>=> vdot [1.0, 2.0] [10.0, 11.0]
32.0
>=> :flops vdot [1.0, 2.0] [10.0, 11.0]

>=>

Parametric type aliases

Type signatures could be much clear if we had a way to define parameterized types with newtype.

From #47:
which has:

eval2NetLoss:: (oz=>Real->oz=>Real->Real) -> oz=>Real -> iz=>Real -> ((hz=>(iz=>Real), hz=>Real), (oz=>(hz=>Real), oz=>Real)) -> Real

if we had {x} do just basic templatish replacement:

This could be

newtype Layer{i,h} = (h=>(i=>Real), h=>Real)
newtype LossFunc{y} = (y=>Real->y=>Real->Real)

eval2NetLoss:: LossFunc{oz} -> oz=>Real -> iz=>Real -> (Layer{iz,hz},Layer{hz,oz}) -> Real

Related to #45

Compiler bug!Not an int

I don't yet have a MWE for this,
and I don't know when I will next have time to work on it.

Here is a Gist that causes the error on the last ;p

• code
• Error (It has like 200 lines of "context")

The code has a bunch of extra type-asserts because I was debugging other mistakes of my own.

Can't iterate over all possible values of a table

I'm writing a test to see if probabilities sum to one over the set of all possible inputs. Normally, one has to write tedious code to iterate over the entire set, but Dex should shine at this! However, writing e.g.
seqs = for seq:((Fin 3)=>(Fin 4)). seq
crashes the interpreter:

Unexpected type ((Fin 3)=>(Fin 4))
CallStack (from HasCallStack):
  error, called at src/lib/Embed.hs:600:8 in dex-0.1.0.0-WMAsfoEK61B3EtpA608ix:Embed

Amusingly, this somehow corrupted the interpreter which then printed

UnexpectedU nteyxppee c(t(eFdi nt y3p)e= >(((FFiinn  43)))=
>C(aFlilnS t4a)c)k
 C(aflrloSmt aHcaks C(aflrloSmt aHcaks)C:a
l l Setrarcokr),: 
c a lelrerdo ra,t  csarlcl/eldi ba/tE msbrecd/.lhisb:/6E0m0b:e8d .ihns :d6e0x0-:08. 1i.n0 .d0e-xW-M0A.s1f.o0E.K06-1WBM3AEstfpoAE6K0681iBx3:EEtmpbAe6d0
8ix:Embed

What is the plan for structured sparse matrixes?

in #50 we really wanted a lower triangular matrix.
But we had to use a fully dense matrix.

One thing I felt while writing it, was if the iteration with nested for was somehow knowing of all the indexs (since structured sparse is basically characterized purely by indexes for a user facing perspective) then that might be it.
But those are two seperate for-loops right now.

More broadly, structured sparse matrixes don't play nice with the concept of a matrix as a collection of row vectors.
But making them anything else messes with the nice symetry between:
a->b->Real and N=>M=>Real, and between currying and slicing.

Multiple-dispatch is really strong in for structured matrixes.
Because you need extensibility that requires knowing 2+ types.
And we know that new structured matrixes are constantly being created and its beyond any one library to actually contain them all.
It really surprised me how keen PDE folk are on their Banded Block Banded Matrixes.
I finally wrote up some of my thoughts on this and a few other things re-composability,
https://white.ucc.asn.au/2020/02/09/whycompositionaljulia.html

I think its important to find a solution for structured matrixes that is at least as easy to extend as multiple dispatch.
Haskell-style type-classes may be an answer, one worry i have their is that if people are not using them constantly they will not leap to them as the natural solution.

I have no idea what the XLA story for structured sparse matrixes is.

Document in tutorial the lack of loops and branchs

As far as I can tell dex does not have branchs.
Instead on should just compute both sides,
and then use select.

Similarly there are not any loops.
This is common for functional languages, but the normal solution of using recursion doesn't work as without branches one can never stop recursing.
Instrad one should use fold.
(And maybe scan / scan'?)

Question: Let cabal handle cbits compilation?

Q: Is there a reason to compile libdex.c as a separate step in the makefile?

I'm keen to try letting Cabal compile libdex.c, in the pattern that is often used elsewhere (eg. see this example in the bytestring package).

However, since it might well be set up the way it is for good reasons, I thought I'd check first before I give it a go. Is this a good idea? :-)

btw: my motivation is to allow stack install to work properly. Currently, if I stack install and then try to run dex from a different directory, I see this:

$ dex
dyld: Library not loaded: cbits/libdex.so
  Referenced from: /Users/jsm/.local/bin/dex
  Reason: image not found
[2]    48521 abort      dex

Since it's trying to load libdex.so dynamically rather than statically linking that code.

Dex support in Jupyter notebooks.

Way-far-down-the-road feature request:
But Jupyter just recently added supported for SQLite, and has support for specialized language kernels, such as Haskell. Would it be possible to add support for Dex?

rand only makes very small and strictly increasing numbers

As far as I can tell rand i is a short-hand for: i * 2.220446e-16
This is not what I expected.

I expected rand i to generate random numbers between 0 and 1.
I expected that i would act as a seed / state of the random number generator.
And for the correlation between i and rand i not to be equal to 1.

>=> for ii::10. rand(asint(ii))
[ 0.0
, 2.220446e-16
, 4.440892e-16
, 6.661338e-16
, 8.881784e-16
, 1.110223e-15
, 1.3322676e-15
, 1.5543122e-15
, 1.7763568e-15
, 1.9984014e-15 ]
>=> for ii::10. (real (asint ii))*2.220446e-16
[ 0.0
, 2.220446e-16
, 4.440892e-16
, 6.661338e-16
, 8.881784e-16
, 1.110223e-15
, 1.3322676e-15
, 1.5543122e-15
, 1.7763568e-15
, 1.9984014e-15 ]

Unable to print transposed matrix when elements are not constant?

The following example seems to work correctly:

mat1 = for i::4 j::4. 0
mat2.i.j = mat1.j.i
:p mat2
> [[0, 0, 0, 0], [0, 0, 0, 0], [0, 0, 0, 0], [0, 0, 0, 0]]

However, weird error happened when the matrix contains different elements:

mat3 = for i::4 j::4. asint i
mat4.i.j = mat3.j.i
:p mat4
Compiler bug!Lookup failed:i
context:
[4=>4=>Int]
(tab::4=>Int = (for  j::4 . 
    mat3.j.i);
(tab_1::4=>4=>Int = (for  i::4 . 
    tab);
tab_1))

The type seems to be correctly inferred:

:t mat4
(4=>(4=>Int))