Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

hide Tensor constructor #34

Merged
merged 3 commits into from
Jun 3, 2021
Merged
Show file tree
Hide file tree
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Next Next commit
wip
  • Loading branch information
joelberkeley committed Jun 3, 2021
commit 833045f8074adbed7f322bf79fef2e712139e1c0
6 changes: 3 additions & 3 deletions src/GaussianProcess.idr
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
1 change: 0 additions & 1 deletion src/MeanFunction.idr
Original file line number Diff line number Diff line change
Expand Up @@ -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
35 changes: 5 additions & 30 deletions src/Tensor.idr
Original file line number Diff line number Diff line change
Expand Up @@ -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 `TensorLike` 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 ----------------------------

Expand Down Expand Up @@ -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]]`.
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.
|||
Expand Down Expand Up @@ -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