diff --git a/src/GaussianProcess.idr b/src/GaussianProcess.idr index 81ab2a2c3..12cc49fcd 100644 --- a/src/GaussianProcess.idr +++ b/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 diff --git a/src/MeanFunction.idr b/src/MeanFunction.idr index ebb802fed..eb94bfd80 100644 --- a/src/MeanFunction.idr +++ b/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 diff --git a/src/Tensor.idr b/src/Tensor.idr index e2c2d631a..edca3b01c 100644 --- a/src/Tensor.idr +++ b/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 diff --git a/test/integration/BayesianOptimization.idr b/test/integration/BayesianOptimization.idr index 545101c13..78b42361c 100644 --- a/test/integration/BayesianOptimization.idr +++ b/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