hide Tensor constructor (#34)

src/GaussianProcess.idr

@@ -78,9 +78,9 @@ log_marginal_likelihood : {samples : Nat}
 log_marginal_likelihood (MkGP _ kernel) (MkGaussian _ cov) (x, y) =
   map foo $ inverse (kernel x x + cov) where
     foo : Tensor [S samples, S samples] Double -> Tensor [] Double
-    foo inv = let n = the (Tensor [] _) $ MkTensor $ the Double $ cast samples
-                  log2pi = the (Tensor [] _) $ log $ MkTensor $ 2.0 * PI
-                  half = the (Tensor [] _) $ MkTensor $ 1.0 / 2
+    foo inv = let n = the (Tensor [] _) $ const $ the Double $ cast samples
+                  log2pi = the (Tensor [] _) $ log $ const $ 2.0 * PI
+                  half = the (Tensor [] _) $ const $ 1.0 / 2
                in - half * ((@@) {head=[]} ((@@) {head=[]} y inv) y - log (det inv) + n * log2pi)
 
 ||| Find the hyperparameter values that optimize the log marginal likelihood of the `data` for the

src/MeanFunction.idr

@@ -30,4 +30,3 @@ MeanFunction features = {sm : Nat} -> Tensor (sm :: features) Double -> Tensor [
 ||| A mean function where the mean is zero in all target dimensions.
 export
 zero : MeanFunction features
-zero {sm} (MkTensor x) = replicate {over=[sm]} $ MkTensor 0

src/Tensor.idr

@@ -39,16 +39,15 @@ ArrayLike : Shape -> Type -> Type
 ArrayLike [] dtype = dtype
 ArrayLike (d :: ds) dtype = Vect d (ArrayLike ds dtype)
 
-||| A `Tensor` contains an array of values, and is differentiated from a nested `Vect` by having
-||| its own type and API.
-public export
+||| A `Tensor` is either a scalar value or array of values.
+export
 data Tensor : (shape: Shape) -> (dtype: Type) -> Type where
-  ||| Construct a `Tensor` from an array.
   MkTensor : ArrayLike shape dtype -> Tensor shape dtype
 
+||| Construct a `Tensor` from `ArrayLike` data.
 export
-Show (ArrayLike shape dtype) => Show (Tensor shape dtype) where
-  show (MkTensor x) = "Tensor " ++ show x
+const : ArrayLike shape dtype -> Tensor shape dtype
+const = MkTensor
 
 ----------------------------- structural operations ----------------------------
 
@@ -76,44 +75,21 @@ public export
 ||| @idx The row to fetch.
 export
 index : (idx : Fin d) -> Tensor (d :: ds) dtype -> Tensor ds dtype
-index idx (MkTensor x) = MkTensor $ index idx x
-
-zipWith : {shape : _} -> (a -> b -> c) -> Tensor shape a -> Tensor shape b -> Tensor shape c
-zipWith f (MkTensor x) (MkTensor y) = MkTensor (zipWithArray f x y) where
-  zipWithArray : {shape': _} ->
-                 (a -> b -> c) -> ArrayLike shape' a -> ArrayLike shape' b -> ArrayLike shape' c
-  zipWithArray {shape'=[]} f x y = f x y
-  zipWithArray {shape'=(d :: ds)} f x y = zipWith (zipWithArray f) x y
 
-||| Tranpose a tensor. For example, `transpose $ MkTensor [[1, 2], [3, 4]]` is
-||| `MkTensor [[1, 3], [2, 4]]`.
+||| Tranpose a tensor. For example, `transpose $ const [[1, 2], [3, 4]]` is
+||| `const [[1, 3], [2, 4]]`.
 export
 transpose : {n, m : _} -> Tensor [m, n] dtype -> Tensor [n, m] dtype
-transpose (MkTensor x) = MkTensor $ transpose x
-
--- why does this work with a and b but not other names?
--- see http://docs.idris-lang.org/en/latest/tutorial/interfaces.html#functors-and-applicatives
-public export
-{shape : _} -> Functor (Tensor shape) where
-  map f (MkTensor x) = MkTensor (g x) where
-    g : {s : _} -> ArrayLike s a -> ArrayLike s b
-    g {s = []} y = f y
-    g {s = (_ :: _)} ys = map g ys
 
 ||| Replicate a tensor over shape `over`.
 |||
 ||| @over The shape over which to replicate the tensor.
 export
 replicate : {over : Shape} -> Tensor shape dtype -> Tensor (over :++ shape) dtype
-replicate (MkTensor x) = MkTensor (f over x) where
-  f : (over: Shape) -> ArrayLike shape dtype -> ArrayLike (over :++ shape) dtype
-  f [] x' = x'
-  f (d :: ds) x' = replicate d (f ds x')
 
 ||| Cast the tensor elements to a dtype inferred from the expected type.
 export
 cast_dtype : Cast dtype dtype' => {shape : _} -> Tensor shape dtype -> Tensor shape dtype'
-cast_dtype tensor = map cast tensor
 
 ||| Construct a diagonal tensor from the given value, where all off-diagonal elements are zero.
 |||
@@ -229,4 +205,3 @@ inverse : Tensor [S n, S n] Double -> Maybe $ Tensor [S n, S n] Double
 ||| The product of all elements along the diagonal of a matrix.
 export
 trace_product : Num dtype => Tensor [S n, S n] dtype -> Tensor [] dtype
-trace_product (MkTensor x) = MkTensor $ product $ diag x

test/integration/BayesianOptimization.idr

@@ -50,6 +50,6 @@ data_model_mapping : Map String $ Pair (Data [2] [1]) Model
 
 new_point_constrained : Maybe $ Tensor [1, 2] Double
 new_point_constrained = let eci = "OBJECTIVE" >>> expectedConstrainedImprovement
-                            pof = "CONSTRAINT" >>> (probabilityOfFeasibility $ MkTensor 0.5)
+                            pof = "CONSTRAINT" >>> (probabilityOfFeasibility $ const 0.5)
                             acquisition = map optimizer $ eci <*> pof
                          in apply acquisition data_model_mapping