Bassel Mabsout
Constructing Dependent Vectors
This is not yet another blog post on the benefits of dependently typed length indexed vectors and how they’re defined, if you’re looking for that Justin Le did a much better job than I can: https://blog.jle.im/entry/fixed-length-vector-types-in-haskell.html. I will only try to construct such vectors. But, as a short description: they are Vectors with their length encoded at the type level like:
Vector 3 Float.
Libs
I will be using V from Linear.V simply because it was missing something like this when I wanted it.
For a general purpose dependent Vector replacement there’s the vector-sized library.
Extensions and imports:
{-# LANGUAGE DataKinds #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE ViewPatterns #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE PartialTypeSignatures #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} import Linear.V import qualified Data.Vector as V import GHC.TypeLits import Data.Kind as K import Data.Proxy
Construction
Ideally
We use the OverloadedLists language extension and everything works perfectly!
Sadly this is not currently possible, there is a trac ticket for it #7495 but it doesn’t have much activity.
A simple way
We make a cons operator:
(:>) :: a -> V n a -> V (n+1) a
(:>) h (V tl) = V (V.cons h tl)
Nil :: V 0 a
Nil = V V.empty
>> :t (0 :> 1 :> 2 :> Nil)
Num a => V 3 a
This isn’t perfect since each cons call is a O(n) operation meaning the whole thing is O(n²) not to mention it’s a bit annoying syntax wise. Can we do better?
Variadic functions
Variadic functions can actually be defined in haskell by abusing type classes, here’s what it looks like:
newtype SizedList (n::Nat) a = SizedList [a]
sizedListCons :: a
-> SizedList n a
-> SizedList (n+1) a
sizedListCons h (SizedList t) = SizedList (h:t)
class Make n a func | func -> a n where
make :: SizedList n a -> func
instance (ErrorIfUnequal n x, n~x)
=> Make n a (V x a) where
make (SizedList l) = V $ V.fromList (reverse l)
{-# INLINE make #-}
instance (Make (n+1) a f)
=> Make n a (a -> f) where
make acc a = make (a `sizedListCons` acc)
{-# INLINE make #-}
type family ErrorIfUnequal (a :: Nat) (b :: Nat)
where
ErrorIfUnequal a a = (() :: K.Constraint)
ErrorIfUnequal a b =
TypeError
('Text "The created vector has size: "
':<>: 'ShowType a
':$$: 'Text " While the expected size is: "
':<>: 'ShowType b)
empty :: SizedList 0 a
empty = SizedList []
construct :: (Make 1 a f) => a -> f
construct = make empty
{-# INLINE construct #-}
Okay let’s break it down:
Let’s remove some complexity
class Make n a func where make :: SizedList n a -> func instance (Make (n+1) a f) => Make n a (a -> f) where make accumulator a = make (a `sizedListCons` accumulator) {-# INLINE make #-}n is the current size of the list, a is the type it is holding and func is what allows the variadicness to work. In the instance we match func as (a -> f) and there’s a constraint that makes sure that f is part of a Make. Which means we expect to take an argument and return a function that may take an argument. the type signature of make in this case is
make :: (Make (n+1) a f) => SizedList a n -> a -> f
That SizedList is what gets threaded through all these arguments to be able to cons all of them. Then there’s the base case where we take a sized list, reverse it (since we were consing the arguments backwards) and then fromList it to get our final sized vector.
The functional dependencies and ErrorIfUnequal are there for usability purposes, we get better errors and better type inference because of them. Also construct is there so that we don’t have to repeat empty at the beginning every time.
Now let’s construct a vector of numbers of size 4:
vec :: Num a => V 4 a
vec = construct 1 2 3 4
That’s it, if you try adding a number or removing one you will get a friendly error message.
This method has a bunch of disadvantages:
We lose a bit of type inference: If you lost the type signature from vec, an ambiguous variable error pops up. I’m not sure if this is a solvable problem or not. However if you try to use that vector anywhere which expects to take a vector everything will work out, you can also use partial type signatures and set the type as
V _ _which is what makes this method the one I use.It’s fairly complex for a constructor.
One advantage of this is we were able to first put the arguments in a list and then we fromListed them to get the vector. This allows us to go from O(n²) to O(n).
I tried it with vectors of size > 1000 and it didn’t really bring down compile times.
At the type level
type family Length (a :: [k]) = (n::Nat) where
Length '[] = 0
Length (x ': xs) = Length xs + 1
class MakeVector list where
toValueLevel :: Num a
=> Proxy list
-> SizedList (Length list) a
instance MakeVector '[] where
toValueLevel _ = empty
instance forall x xs.
(KnownNat x, MakeVector xs)
=> MakeVector (x ': xs) where
toValueLevel _ =
fromIntegral (natVal (Proxy @x))
`sCons` toValueLevel (Proxy @xs)
create :: forall list a .
(MakeVector list,Num a)
=> Proxy list
-> V (Length list) a
create list =
(\(SizedList l) -> V $ V.fromList l)
(create list)
test = create (Proxy @[1,2,3,4])
or with AllowAmbiguousTypes to make it slightly more user friendly
{-# LANGUAGE AllowAmbiguousTypes #-}
class ToValueLevel list where
toValueLevel :: Num a
=> SizedList (Length list) a
instance ToValueLevel '[] where
toValueLevel = empty
instance forall x xs.
(KnownNat x, ToValueLevel xs)
=> ToValueLevel (x ': xs) where
toValueLevel = fromIntegral (natVal (Proxy @x))
`sCons` toValueLevel @xs
create :: forall list a .
(ToValueLevel list, Num a)
=> V (Length list) a
create =
(\(SizedList l) -> V $ V.fromList l)
(toValueLevel @list)
If you look at this funny it looks a bit like the value level function one would write with some pattern matching.
>> :t create @[1,2,3,4]
Num a => V 4 a
The difference between this and the above is that this gains type inference but can only handle types that can be unpromoted from the type level, for example you cannot write 2.3 at the type level yet.
At run time
Reification:
reifyVector :: forall a r. V.Vector a -> (forall (n :: Type). Dim n => V n a -> r) -> r reifyVector v f = reifyDim (V.length v) (\(Proxy :: Proxy n) -> f (V v :: V n a))
Since we do not know the length of the vector at run time, applying functions which accepts Vs of any length works.
Maybe:
fromVector :: forall n a. Dim n => V.Vector a -> Maybe (V n a) fromVector v | V.length v == reflectDim (Proxy @n) = Just (V v) | otherwise = Nothing
We can also fail if a vector is not of a certain length otherwise gaining the information at the type level.
Both of these are already available and exported from Linear.V
Destruction
Alright, now that we’ve constructed our precious vectors it is also very useful to pattern match on them. This is the way CLaSH does it:
pattern Nil :: V 0 a
pattern Nil <- _
where Nil = V V.empty
uncons :: V (n+1) a -> (a, V n a)
uncons (V ht) = (V.head ht, V $ V.tail ht)
infixr 5 :>
pattern (:>) :: a -> V n a -> V (n+1) a
pattern h :> t <- (uncons -> (h, t))
where (:>) h (V t) = V $ V.cons h t
Instead of a simple cons operator as we had above, we use PatternSynonyms in order to pattern match as well. For pattern matching there is no performance issue since splitting vectors is O(1).
>> let test (a :> b :> c :> Nil) = a + b + c
>> :t test
Num a => Vec 3 a -> a
Final Thoughts
I am not sure if PatternSynonyms can be used with the variadic function I wrote. If it can, having a unified interface would be great. It should also be possible to fix the type inference problem, since all the information is available to the type system.