Haskell beginner here. I've defined the following types:
data Nat = Z | S Nat data Vector a n where Nil :: Vector a Z (:-) :: a -> Vector a n -> Vector a (S n) infixl 5 :-
I'm trying to write the function, takeWhileVector which behaves the same as takeWhile does on lists, but on Vectors.
My implementation is as follows:
takeWhileVector :: (a -> Bool) -> Vector a n -> Vector a m takeWhileVector f Nil = Nil takeWhileVector f (x :- xs) = if (f x) then (x :- takeWhileVector f xs) else Nil
This doesn't compile and produces the following error:
Could not deduce (m ~ 'S n0) from the context (n ~ 'S n1) bound by a pattern with constructor :- :: forall a (n :: Nat). a -> Vector a n -> Vector a ('S n), in an equation for ‘takeWhileVector’ at takeWhileVector.hs:69:20-26 ‘m’ is a rigid type variable bound by the type signature for takeWhileVector :: (a -> Bool) -> Vector a n -> Vector a m at takeWhileVector.hs:67:20 Expected type: Vector a m Actual type: Vector a ('S n0) Relevant bindings include takeWhileVector :: (a -> Bool) -> Vector a n -> Vector a m (bound at takeWhileVector.hs:69:1) In the expression: (x :- takeWhileVector f xs) In an equation for ‘takeWhileVector’: takeWhileVector f (x :- xs) = (x :- takeWhileVector f xs)
I would have thought that my type definition for takeWhileVector says the following:
For all types 'a' and 'n's of kind Nat, this function returns a 'Vector a m', where 'm' is kind Nat.
Do I need to change the type signature of takeWhileVector to be more specific so that it shows that the result is Vector a (m :: Nat)? Otherwise, how can I change this to have it compile?