Skip to content

Instantly share code, notes, and snippets.

@ryanorendorff
Last active July 9, 2020 10:20
Show Gist options
  • Save ryanorendorff/d05c378b71829e3c0c33de462cb9a973 to your computer and use it in GitHub Desktop.
Save ryanorendorff/d05c378b71829e3c0c33de462cb9a973 to your computer and use it in GitHub Desktop.
name: vector-list
depend: standard-library
include: .
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
{-# 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)
@ryanorendorff
Copy link
Author

ryanorendorff commented Jul 9, 2020

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.

@christiaanb
Copy link

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment