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 `instance`

s. 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 `hMap`

ped 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!

- Haskell fails to infer the return type of a monad after using the sequence operator
- Does extracting values from a multiple Value return in Haskell invoke the function more than once?
- Why do I get "Unexpected reply type" from notify-send when using this Haskell notification server?
- Don't understand notation of morphisms in Monoid definition
- Foldln in haskell
- Is this property of a functor stronger than a monad?
- How to Instantiate a Custom Data Type with Record Syntax and Multiple Constructors
- How do I make a minimal working example for the a DBus server?
- Is it safe to downgrade Haskell stack version?
- Haskell, list of natural number
- unfamiliar syntax in Haskell / Clash function type signature
- foldM with monad State does not type check
- Why does my Runge-Kutta implementation oscillate to 0?
- How do I get the desired behavior in my TCP server?
- Why does the Haskell PVP describe new functions as non-breaking?
- How do I correctly use toLower in Haskell?
- How can I write a notification server in Haskell?
- Every Lens' is a Traversal'... how?
- How do I crate a value of type a{sv} for a call to org.freedesktop.Notifications.Notify via DBus?
- Web Scraping With Haskell
- Double exclamation marks in Haskell
- Haskell Servant POST FormUrlEncoded for (Vector String) field
- Confusion about list types in Haskell
- Idiomatic way to define new vs persisted types in Haskell
- Why does Cabal, unlike GHC, not automatically enable GeneralizedNewtypeDeriving if I explicitly enabled DerivingStrategies?
- What is the proper way of wrapping an Int (not a general type) in another type if type safety is the only motive?
- Parsing inside `between` with Megaparsec
- takeWhile implementation in JavaScript - Looking for better ideas
- How to setup MINGW environment variables for Haskell language server in vscode?
- mysql-haskell no invoke of Right case of try function