Data

Dataset types.

Definitions

record Dataset : (0 _ : Shape) -> (0 _ : Shape) -> Type

  Observed pairs of data points from feature and target domains. Data sets such as this are
  commonly used in supervised learning settings.
  
  @features The shape of the feature domain.
  @targets The shape of the target domain.

Totality: total
Visibility: public export
Constructor: 

MkDataset : Tensor (S s :: featureShape) F64 -> Tensor (S s :: targetShape) F64 -> Dataset featureShape targetShape

Projections:

.features : ({rec:0} : Dataset featureShape targetShape) -> Tensor (S ({rec:0} .s) :: featureShape) F64

  The feature data

.s : Dataset featureShape targetShape -> Nat

.targets : ({rec:0} : Dataset featureShape targetShape) -> Tensor (S ({rec:0} .s) :: targetShape) F64

  The target data

Hint: 

Taggable (Dataset f t)

.s : Dataset featureShape targetShape -> Nat

Totality: total
Visibility: public export

.features : ({rec:0} : Dataset featureShape targetShape) -> Tensor (S ({rec:0} .s) :: featureShape) F64

  The feature data

Totality: total
Visibility: public export

.targets : ({rec:0} : Dataset featureShape targetShape) -> Tensor (S ({rec:0} .s) :: targetShape) F64

  The target data

Totality: total
Visibility: public export

concat : Dataset features targets -> Dataset features targets -> Dataset features targets

  Concatenate two datasets along their leading axis.

Totality: total
Visibility: export