Search code examples
haskellgadttype-level-computation

Length indexed heterogeneous vector

I have a Vector data type which is length indexed

data Vector :: Nat -> Type -> Type where
  VNil  :: Vector 0 a
  VCons :: a -> Vector n a -> Vector (n + 1) a

Now what I would like to do is that every single element in the list contains a function one type a to a type b but that type b is different for every index in the vector.

hMap :: forall n a. Vec n (forall b. a -> b) -> a -> Vec n (forall b. b)
hMap VNil _ = VNil
hMap (f `VCons` fs) a = f a `VCons` hMap fs a

Now of course this doesn't compile. Because GHC doesn't support impredicative types. Is there some kind of workaround for this? Maybe some kind of HVector? I'm not really familiar with such advanced features but really would like to know how hMap could be implemented.

Any help is appreciated!

Solution

  • The vector type that you've defined, as you've already pointed out, is homogeneous. And you can't really use forall to turn a homogeneous type into a heterogeneous one, as that's not really what it's for.

    Instead, what we really need is a heterogeneous vector type. First, let's get the formalities out of the way. We're going to need a lot of GHC extensions by the end of this, so here we go.

    {-# LANGUAGE GADTs, DataKinds, TypeOperators, KindSignatures, TypeFamilies,
             MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances,
             UndecidableInstances #-}

    I'm assuming the Nat type you're using comes from GHC.TypeLits and the Type type comes from Data.Kind.

    import Data.Kind
import GHC.TypeLits

    Now your original vector type looked like this.

    data Vector :: Nat -> Type -> Type where
  VNil  :: Vector 0 a
  VCons :: a -> Vector n a -> Vector (n + 1) a

    I'm going to propose this instead.

    data Vector (n :: Nat) (xs :: [Type]) where
  VNil :: Vector 0 '[]
  VCons :: t -> Vector n ts -> Vector (n + 1) (t ': ts)

infixr 9 `VCons`

    Rather than having a single type of element, we have a list of element types. Note that xs is a list (as in, the built-in [] type) of types (Type from Data.Kind). Every type defined in Haskell can be lifted to the type level. You've already seen how to lift natural number literals (which are a bit of a special case, due to the special syntax surrounding them), but we can do the same to lists.

    VNil is only valid for for length zero and the empty type list, while VCons is valid for a nonempty list of length n + 1 and is made up of an element t (the head of the type-level list t ': ts) and a tail Vector n ts.

    There are apostrophes in front of the constructors that we're lifting from the value level to the type level. '[] is just the value constructor [] (i.e. the empty list) lifted to the type level. Without the quote, in a type context, [] is a type constructor of kind * -> *, so we have to lift it to fix the ambiguity. And it's generally good practice to do this, even when it's not ambiguous.

    I also define VCons to be right-associative when used in infix form, which will make actually constructing these vectors marginally easier down the road.

    Now, at this juncture, I would recommend we actually omit the n parameter entirely. You can do pretty much everything else I suggest here with an n parameter, but since we also have the list, we still know how long our vector is statically. So what I would recommend is

    data Vector (xs :: [Type]) where
  VNil :: Vector '[]
  VCons :: t -> Vector ts -> Vector (t ': ts)

infixr 9 `VCons`

    We can recover the length at the type-level using a type-level function. In fact, this will be good practice for hMap in a minute, so let's write it out.

    When we want to write a function that recurses on a complicated GADT type like this, we usually do so as a typeclass. In this case, we want a type-level function called VectorLength, so we'll write a typeclass which defines a type family to give us our result.

    In normal value-level Haskell, you write a type signature, then you write the cases to pattern match against. We do the exact same thing in type-level Haskell. However, our "type signature" is a class and our cases are instances. Here's our type signature.

    class HasLength (ts :: [Type]) where
    type VectorLength ts :: Nat

    Now our base case is an instance for the empty list type-level value '[]. Read that sentence again and make sure you understand what I'm overloading here.

    instance HasLength '[] where
    type VectorLength '[] = 0

    Finally, our recursive case.

    instance HasLength xs => HasLength (x ': xs) where
    type VectorLength (x ': xs) = 1 + VectorLength xs

    A vector containing (x ': xs) has a length if the tail (which contains xs) has a length. And specifically, the length is 1 + VectorLength xs. You can think of our instance's context (HasLength xs in this case) as being a sort of dependency list for our function. Our function needs to call VectorLength xs, so we have to declare that in our instance header.

    Now let's write hMap. This will also be in a typeclass, but it'll be a regular Haskell function, not a type family, since we want to operate at the value level. It still has to be a typeclass since we're going to dispatch on things at the type level (namely, our list of constituent types).

    Here's the type signature.

    class CanHMap (fs :: [Type]) (a :: Type) (bs :: [Type]) | fs -> bs where
    hMap :: Vector fs -> a -> Vector bs

    That funny little syntax after the vertical bar | is called a functional dependency, and it really helps with type inference. It says "If I know the value fs (of functions), then I can deduce the value bs (of results of those functions)".

    Now we write our base case.

    instance CanHMap '[] a '[] where
    hMap VNil _ = VNil

    The empty list of functions can be hMapped to the empty list of results, and the type a in the middle doesn't matter. Specifically, this mapping takes VNil to VNil.

    Moving on to our recursive case.

    instance CanHMap fs a bs => CanHMap ((a -> b) ': fs) a (b ': bs) where
    hMap (VCons f fs) a = VCons (f a) (hMap fs a)

    If we can take fs to bs with an input of type a, then we can also take ((a -> b) ': fs) to (b ': bs) with an input of type a.

    The neat thing here is that, after all of the insane type-level juggling is done, the function bodies are actually remarkably simple and beautiful.

    Let's test it out. Here are some functions.

    myFunctions :: Vector '[Int -> Int, Int -> String, Int -> ()]
myFunctions = (\n -> n + 1) `VCons` show `VCons` (\_ -> ()) `VCons` VNil

    This is why I declared the infixr declaration earlier: So we could chain VCons calls here.

    Now here's the list of results when we apply those functions to 0.

    myVector :: Vector [Int, String, ()]
myVector = hMap myFunctions (0 :: Int)

    This typechecks, but does it work? Well, to figure that out, we'll need to write some quick Show instances to be able to print them out.

    -- I ignore the precedence parameter here. Feel free
-- to fill that in on your own time. :)

instance Show (Vector '[]) where
    showsPrec _ VNil = ("VNil" ++)

instance (Show x, Show (Vector xs)) => Show (Vector (x ': xs)) where
    showsPrec _ (VCons x xs) = ("VCons " ++) . shows x . (" (" ++) . shows xs . (")" ++)

    And finally

    main :: IO ()
main = print myVector

    And the verdict?

    $ runhaskell example.hs
VCons 1 (VCons "0" (VCons () (VNil)))

    Success!

    You can see a complete working example of this code on Try it online!