Menu
I have defined a vector as such:
{-# LANGUAGE GADTs, DataKinds, TypeFamilies, UndecidableInstances, TypeOperators #-}
data Nat = Z | S Nat
type family (+) (n :: Nat) (m :: Nat) :: Nat
type instance Z + m = m
type instance (S n) + m = S (n + m)
type family (*) (n :: Nat) (m :: Nat) :: Nat
type instance Z * m = Z
type instance (S n) * m = n * m + m
data Vec (n :: Nat) a where
VNil :: Vec Z a
VCons :: a -> Vec n a -> Vec (S n) a
and am attempting to make a vectorConcat, as such:
vectorConcat :: Vec m (Vec n a) -> Vec (m * n) a
However, when trying to do this:
vectorAppend :: Vec n a -> Vec m a -> Vec (n + m) a
vectorAppend VNil ys = ys
vectorAppend (VCons x xs) ys = VCons x (vectorAppend xs ys)
vectorConcat :: Vec m (Vec n a) -> Vec (m * n) a
vectorConcat VNil = VNil
vectorConcat (VCons x xs) = vectorAppend x (vectorConcat xs)
I get the following error, and am not sure how to resolve it:
Could not deduce (((n1 * n) + n) ~ (n + (n1 * n)))
from the context (m ~ 'S n1)
bound by a pattern with constructor
VCons :: forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a,
in an equation for `concatV'
I have been stuck on this for a while, and wondering if I could get any direction.
963
The concatenation of vectors can be done by using combination function c. For example, if we have three vectors x, y, z then the concatenation of these vectors can be done as c(x,y,z). Also, we can concatenate different types of vectors at the same time using the same same function.
To concatenate a vector or multiple vectors in R use c() function. This c() function is used to combine the objects by taking two or multiple vectors as input and returning the vector with the combined elements from all vectors.
Can you combine vectors C++? Using insert() to combine two vectors in C++ vector::insert() is an in-built function in the standard template library of C++. This function can be used to insert elements before the element at a specific position. We can utilize this function to merge two vectors in C++.
GHC doesn't really know many facts about arithmetic, and in particular (in this case) doesn't know that addition is commutative. It's not easy to teach GHC this fact, either.
However, in this specific case, you can simply commute the terms in your definition of (*) by hand, and then things compile just fine:
type instance (S n) * m = m + (n * m)
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With
