fc.idr

interface Layer (layer : Vect ir Nat -> Vect or Nat -> Type) where
  runLayer :    Tensor ir i Double
             -> layer i o
             -> Tensor or o Double

data FullyConnected : (ir : Nat) -> (or : Nat) -> Vect ir Nat -> Vect or Nat -> Type where
  MkFullyConnected :      (ir = 1)
                      ->  (or = 1)
                      ->  (biases  : Tensor 1 o Double)
                      ->  (weights : Tensor 2 ((head o) :: i) Double)
                      ->  FullyConnected 1 1 i o

Layer (FullyConnected 1 1) where
  runLayer input (MkFullyConnected ir or biases weights) = biases