vector-list.agda-lib

name: vector-list
depend: standard-library
include: .

VectorList.agda

module VectorList where

open import Data.List using (List; sum) renaming ([] to []ᴸ; _∷_ to _∷ᴸ_)
open import Data.Nat using (ℕ)
open import Data.Vec using (Vec; _++_) renaming ([] to []ⱽ; _∷_ to _∷ⱽ_)

infixr 5 _∷ⱽ_
data VectorList (A : Set) : List ℕ → Set where
  []ⱽ : VectorList A []ᴸ
  _∷ⱽ_ : {n : ℕ} {ns : List ℕ} → Vec A n → VectorList A ns → VectorList A (n ∷ᴸ ns)

concat : {A : Set} {ns : List ℕ} → VectorList A ns → Vec A (sum ns)
concat []ⱽ = []ⱽ
concat (v ∷ⱽ vs) = v ++ concat vs

VectorList.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

-- ghc-typelits-knownnat package
{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}

-- ghc-typelits-natnormalise package
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}


module VectorList
    ( VectorList(..)
    , Sum
    , exVectorList
    , exVectorListSum
    -- , concat
    )
where

import           GHC.TypeLits
import           Numeric.LinearAlgebra.Static -- HMatrix package
import Prelude hiding (concat)


-- | Sum a type level list of naturals
type family Sum (xs :: [Nat]) :: Nat where
    Sum '[] = 0
    Sum (n ': ns) = n + Sum ns

data VectorList (ns :: [Nat]) where
    VNil :: VectorList '[]
    (:::) :: (KnownNat n) => R n -> VectorList ns -> VectorList (n ': ns)

infixr 6 :::

-- | An example of how to construct an VectorList
exVectorList :: VectorList '[2, 3]
exVectorList = konst 1 ::: konst 2 ::: VNil

-- I assume this works because the inputs are more than KnownNat's: they are specific Nats!
exVectorListSum :: R (Sum '[2, 3])
exVectorListSum = (konst 1 :: R 3) # (konst 2 :: R 2)

-- This does not work but I think it is because I have lost the size of the
-- vector, so the size of r and rs are not known to the compiler.
concat :: VectorList ns -> R (Sum ns)
concat (r ::: VNil) = r
concat (r ::: rs) = r # (concat rs)

As I said in my email, the only possible solution I could think of was:

concat :: VectorList ns -> R (Sum ns)
concat rs = case concatWorker rs of
  RWorker rsW -> rsW

data RWorker n where
  RWorker :: KnownNat n => R n -> RWorker n

concatWorker :: VectorList ns -> RWorker (Sum ns)
concatWorker (r ::: VNil) = RWorker r
concatWorker (r ::: rs) = case concatWorker rs of
  RWorker rsW -> RWorker (r # rsW)

Because KnownNat constraints can only be constructed from other KnownNat constraints, because constraints are terms; they can't be constructed from types, because types are erased before run-time.