Erase the distinction between terms and types

dex.cabal

@@ -16,10 +16,10 @@ flag inotify
   default:             False
 
 library
-  exposed-modules:     Record, Env, Syntax, Type, Inference, JIT, LLVMExec,
+  exposed-modules:     Env, Syntax, Type, Inference, JIT, LLVMExec,
                        Parser, Util, Imp, PPrint, Array,
-                       Actor, Cat, Flops, Normalize, Embed, Serialize,
-                       RenderHtml, Plot, LiveOutput, Subst, Simplify, TopLevel,
+                       Actor, Cat, Flops, Embed, Serialize,
+                       RenderHtml, Plot, LiveOutput, Simplify, TopLevel,
                        Autodiff, JAX, Interpreter, Logging, PipeRPC
   build-depends:       base, containers, mtl, binary, bytestring,
                        time, tf-random, llvm-hs-pure ==9.*, llvm-hs ==9.*,

examples/ad-tests.dx

@@ -1,78 +1,27 @@
-:p
-   f : Real -> Real
-   f x = x
-   jvp f 3.0 2.0
-> 2.0
-
-:p
-   f x = x * x
-   jvp f 3.0 1.5
-> 9.0
 
 :p
-   f x = x + x
-   jvp f 3.0 2.0
-> 4.0
-
-:p
-   f x = x * x * x
-   jvp f 2.0 1.5
-> 18.0
-
-:p
-   f x = x * x * x
+   f = \x. x * x * x
    jvp (\x. jvp f x 1.0) 2.0 1.0
 > 12.0
 
 :p
-   f x = 4.0 * x * x * x
+   f = \x. 4.0 * x * x * x
    deriv (deriv (deriv f)) 1.234
 > 24.0
 
+-- TODO: handle pairs and re-enable
 :p
-   f : Real --o Real
-   f x = x
-   transposeLinear f 2.0
-> 2.0
-
-:p
-   f : Real --o Real
-   f x = x + x
-   transposeLinear f 1.0
-> 2.0
-
-:p
-   f : Real --o Real
-   f x = x + (x + x) * 2.0
-   transposeLinear f 1.0
-> 5.0
-
-:p
-   f : Real --o Real
-   f x = x * 2.0
-   transposeLinear f 1.0
-> 2.0
-
-:p
-   f : Real --o Real
-   f x = 2.0 * x
-   transposeLinear f 1.0
-> 2.0
-
-:p
-   f : Real --o (Real, Real)
-   f x = (x, 2.0 * x)
+   f : Real --o (Real & Real) = \x. (x, 2.0 * x)
    transposeLinear f (1.0, 3.0)
 > 7.0
 
+-- TODO: handle pairs and re-enable
 :p
-   f : (Real, Real) --o Real
-   f (x,y) = x + 2.0 * y
+   f : (Real & Real) --o Real = \(x,y). x + 2.0 * y
    transposeLinear f 1.0
 > (1.0, 2.0)
 
-:p grad (\x. x * x) 1.0
-> 2.0
+-- TODO: handle user-defined linearity rules an re-enable
 
 :p deriv cos 0.0
 > 0.0
@@ -110,12 +59,6 @@
 :p checkDeriv (deriv cos) 1.0
 > True
 
-:p deriv (fdiv 3.0) 2.0
-> -0.75
-
-:p deriv (\x. x / 2.0) 3.0
-> 0.5
-
 badDerivFun : Real -> Real
 badDerivFun x = x
 

examples/brownian_motion.dx

@@ -1,21 +1,21 @@
 
 
-type UnitInterval = Real
+UnitInterval = Real
 
-bmIter : (Key, Real, Real, UnitInterval) -> (Key, Real, Real, UnitInterval)
-bmIter (key, y, sigma, t) =
-  (kDraw, kL, kR) = splitKey3 key
-  t' = abs (t - 0.5)
-  y' = sigma * randn kDraw * (0.5 - t')
-  key' = select (t > 0.5) kL kR
-  (key', y + y', sigma / sqrt 2.0, t' * 2.0)
+bmIter : (Key & Real & Real & UnitInterval) -> (Key & Real & Real & UnitInterval) =
+  \(key, y, sigma, t).
+    (kDraw, kL, kR) = splitKey3 key
+    t' = abs (t - 0.5)
+    y' = sigma * randn kDraw * (0.5 - t')
+    key' = select (t > 0.5) kL kR
+    (key', y + y', sigma / sqrt 2.0, t' * 2.0)
 
-sampleBM : Key -> UnitInterval -> Real
-sampleBM key t =
-  (_, y, _, _) = fold (key, 0.0, 1.0, t) \i:10. bmIter
-  y
+sampleBM : Key -> UnitInterval -> Real =
+  \key t.
+    (_, y, _, _) = fold (key, 0.0, 1.0, t) \i:(Fin 10). bmIter
+    y
 
-xs = linspace @1000 0.0 1.0
+xs = linspace (Fin 1000) 0.0 1.0
 ys = map (sampleBM (newKey 0)) xs
 
 :plot zip xs ys

examples/easy-ad-tests.dx

@@ -0,0 +1,53 @@
+:p
+   f : Real -> Real = \x. x
+   jvp f 3.0 2.0
+> 2.0
+
+:p
+   f = \x. x * x
+   jvp f 3.0 1.5
+> 9.0
+
+:p
+   f = \x. x + x
+   jvp f 3.0 2.0
+> 4.0
+
+:p
+   f = \x. x * x * x
+   jvp f 2.0 1.5
+> 18.0
+
+:p
+   f : Real --o Real = \x. x
+   transposeLinear f 2.0
+> 2.0
+
+:p
+   f : Real --o Real = \x. x + x
+   transposeLinear f 1.0
+> 2.0
+
+:p
+   f : Real --o Real = \x. x + (x + x) * 2.0
+   transposeLinear f 1.0
+> 5.0
+
+:p
+   f : Real --o Real = \x. x * 2.0
+   transposeLinear f 1.0
+> 2.0
+
+:p
+   f : Real --o Real = \x. 2.0 * x
+   transposeLinear f 1.0
+> 2.0
+
+:p grad (\x. x * x) 1.0
+> 2.0
+
+:p deriv (\x. 3.0 / x) 2.0
+> -0.75
+
+:p deriv (\x. x / 2.0) 3.0
+> 0.5