CODEWITHSUNDEEP
haskelldependent-type
Ignat Insarov
Ignat Insarov

Reputation: 4832

Can I convert a list to a length indexed vector with a class?

To avoid ragged matrices, I want to design a type wrapper for lists that holds length in type. (Please correct me if I should not call it a "length-indexed vector".) I would like to provide it as an abstract type with smart constructors, among which would be an IsList instance or something similar in spirit.

This is where I am:

data Nat = Z | S Nat

data Vector (n :: Nat) a = Vector [a] deriving Show

v0 :: Vector Z a
v0 = Vector [ ]

put :: a -> Vector n a -> Vector (S n) a
put x (Vector xs) = Vector (x:xs)

class Fold a where
    type Elem a
    fold :: [Elem a] -> a

instance Fold (Vector Z a) where
    type Elem (Vector Z a) = a
    fold [ ] = v0

instance Fold (Vector (S n) a) where
    type Elem (Vector (S n) a) = a
    fold (x:xs) = put x (fold xs)

The Fold typeclass is supposed to take elements from a list one by one and put them to the vector. The instances I intend to represent the base case and the inductive case for structural induction along the Naturals.

However, the code I posted does not work, and I cannot sort the errors out. In essence, it talks about the element types of vectors of different length not being equal:

...
  Expected type: [Elem (Vector n a)]
    Actual type: [Elem (Vector ('S n) a)]
...
     fold (x:xs) = put x (fold xs)
                               ^^

If I assume the magical coercion function:

    fold (x:xs) = put x (fold $ undefined xs)

− I will then reach another error:

    • No instance for (Fold (Vector n a)) arising from a use of ‘fold’
...
     fold (x:xs) = put x (fold $ undefined xs)
                          ^^^^^^^^^^^^^^^^^^^

This saddens me because it must mean my inductive instance does not iterate.

I need help with this.

Upvotes: 1

Views: 390

Answers (2)

HTNW
HTNW

Reputation: 29193

Can I obtain [an IsList instance] at all?

No. IsList a implies a function [Elem a] -> a. This is impossible for length-indexed vectors, because the signature demands the ouput type not depend on the input length. The closest you can get is the following:

data VecSomeLen a = forall (n :: Nat). VecSomeLen (Vector n a)
instance IsList (VecSomeLen a) where ...
-- and also
instance IsList (Maybe (Vector n a)) where ...

It’s not entirely useless, because it lifts a list with no size into one with unknown but manipulatable size/checks whether a list has a given length, but it’s pretty useless when you consider it’s usually used when the size is known.

I’d just use varargs.

-- untested but *should* compile
class MkVector n a n' r | r -> n a n' where
  mkVector :: (Vector n a -> Vector n' a) -> r
instance MkVector Z a n (Vector n a) where
  mkVector f = f $ Vector []
instance (MkVector n a n' r) => MkVector (S n) a n' (a -> r) where
  mkVector f x = mkVector $ \(Vector xs) -> f $ Vector $ x:xs

vector :: MkVector n a n r => r
vector = mkVector id

-- vector 1 5 3 :: Vector (S(S(S(Z)))) Int

Now, the thing is that your Fold class, though it can compile with @Alec’s change, is totally the wrong thing to do. Look at the type of the function you’ll create:

fold :: forall n. [a] -> Vector n a

That’s no good! Given a list of elements, you can make a sized list, except the new size is not related in any way to the input list. You seem to be getting around that with non-totality, which is just a terrible idea. Furthermore, if anyone comes by and tries to make fold total, it’s easy to break the Vector invariants by accident. Honestly, your definiton of Vector is somewhat odd. It’s easy to break its invariants because the backing data is not as strongly typed as its interface. I’d redefine it:

data Vector (n :: Nat) a where
  (:%:) :: a -> Vector n a -> Vector (S n) a
  VNil  :: Vector Z a
infixr 5 :%:
-- infixr 5 :

Which makes it impossible to write a total fold (and that’s good, because its existence is a bug). However, you can no longer (safely) coerce to a normal list because this is no longer a newtype (but I believe they have the same representation anyway and can still be unsafeCoerce'd).

A better idea would be to encode the partiality with Maybe. Additionally, you can abstract out a certain pattern from the Fold class to make writing similar functions easier.

-- can’t match on types so match on SNat representatives
data SNat (n :: Nat) where
  SZ :: SNat Z
  SS :: SNat n -> SNat (S n)
-- pass SNats around implicitly
class KNat (n :: Nat) where kNat :: SNat n
instance KNat Z where kNat = SZ
instance KNat n => KNat (S n) = SS kNat
fromList' :: SNat n -> [a] -> Maybe (Vector n a)
fromList' (SS n) (x:xs) = (x :%:) <$> fromList' n xs
fromList' SZ [] = return VNil
fromList' _ _ = Nothing
fromList :: KNat n => [a] -> Maybe (Vector n a)
fromList = fromList' kNat

Upvotes: 1

Alec
Alec

Reputation: 32309

The compiler is informing you of two different problems.

In essence, it talks about the element types of vectors of different length not being equal:

Spot on! You have two approaches here. If you want to keep the Elem family as part of the typeclass, you'll have to add an extra constraint to the inductive case basically telling GHC "my element types are equal":

instance (Elem (Vector n a) ~ a) => Fold (Vector (S n) a) where
    type Elem (Vector (S n) a) = a
    fold (x:xs) = put x (fold xs)

Alternately, you could make that type family completely separate and have only one (more sensible) instance:

type family Elem xs :: *
type instance Elem (Vector n x) = x

class Fold a where
  fold :: [Elem a] -> a

Up to you!

This saddens me because it must mean my inductive instance does not iterate.

Sure it doesn't "iterate", because you haven't told GHC to go find a recursive subproblem! Just add that subproblem to your constraint for the inductive case.

-- If you decided to keep the type family associated
instance (Elem (Vector n a) ~ a, Fold (Vector n a)) => Fold (Vector (S n) a) where
  type Elem (Vector (S n) a) = a
  fold (x:xs) = put x (fold xs)

or

-- If you decided not to keep the type family associated
instance Fold (Vector n a) => Fold (Vector (S n) a) where
  fold (x:xs) = put x (fold xs)

Upvotes: 3

Related Questions