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)

I would like to get the code from Agda working directly in Haskell. However the direct translation does not work. It returns the following error when trying to compile concat:

VectorList.hs: error:
    • Could not deduce (KnownNat (Sum ns1)) arising from a use of ‘#’
      from the context: (ns ~ (n : ns1), KnownNat n)
        bound by a pattern with constructor:
                   ::: :: forall (n :: Nat) (ns :: [Nat]).
                          KnownNat n =>
                          R n -> VectorList ns -> VectorList (n : ns),
                 in an equation for ‘concat’
        at VectorList.hs
    • In the expression: r # (concat rs)
      In an equation for ‘concat’: concat (r ::: rs) = r # (concat rs)
   |
53 | concat (r ::: rs) = r # (concat rs)
   |                     ^^^^^^^^^^^^^^^

where (#) is the same as Agda's _++_.

I believe the problem is that the generic solver and solver plugin (from ghc-typelits-knownnat) cannot automatically derive the KnownNat instance for the Sum type level function. There is some documentation in the solver plugin for how to extend constraints to new type level functions but I'm not sure how to extend the concept to type level functions over type level lists.

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.