understanding type-level functions in haskell

Question

I am trying to understand how the Plus and Times functions in the code below work. What I do not understand is:

1. How do you call these functions in ghci to operate on a vector?
2. Why do they have to operate on the type level? What type do they operate on?
3. How do they evaluate the result?

For plus, we have, Plus (S m) n = S (Plus m n), but how is (Plus m n) evaluated. Similarly, how is (Times n m) evaluated?

{-# LANGUAGE DataKinds, KindSignatures, TypeFamilies, GADTs #-}
{-# LANGUAGE UndecidableInstances, StandaloneDeriving #-}

module Vector where

-- Natural numbers, values will be promoted to types
data Nat
  = Z     -- Zero
  | S Nat -- Successor (+1)

data Vec (a :: *) :: Nat -> * where
  -- Nil has zero length
  Nil :: Vec a Z
  -- Cons has length of the tail + 1
  Cons :: a -> Vec a n -> Vec a (S n)

deriving instance Show a => Show (Vec a n)

-- head :: [a] -> a
hd :: Vec a (S n) -> a
hd (Cons x xs) = x

-- tail :: [a] -> [a]
tl :: Vec a (S n) -> Vec a n
tl (Cons x xs) = xs

-- map :: (a -> b) -> [a] -> [b]
vMap :: (a -> b) -> Vec a n -> Vec b n
vMap f Nil = Nil
vMap f (Cons x xs) = Cons (f x) (vMap f xs)

-- (++) :: [a] -> [a] -> [a]
vAppend :: Vec a n -> Vec a m -> Vec a (Plus n m)
vAppend Nil         xs = xs
vAppend (Cons y ys) xs = Cons y (vAppend ys xs)

-- Type-level addition
type family Plus (x :: Nat) (y :: Nat) :: Nat where
  Plus Z     n = n
  Plus (S m) n = S (Plus m n)


-- concat :: [[a]] -> [a]
vConcat :: Vec (Vec a n) m -> Vec a (Times m n)
vConcat Nil = Nil
vConcat (Cons xs xss) = xs `vAppend` vConcat xss

-- Type-level multiplication
type family Times (x :: Nat) (y :: Nat) :: Nat where
  Times Z     m = Z
  Times (S n) m = Plus m (Times n m)

vFilter :: (a -> Bool) -> Vec a n -> [a]
vFilter p Nil = []
vFilter p (Cons x xs)
  | p x = x : vFilter p xs
  | otherwise = vFilter p xs

Answer 1

Let me first define a more convenient synonym for Cons:

infixr 5 #:
(#:) :: a -> Vec a n -> Vec a (S n)
(#:) = Cons

---

How do you call these functions in ghci to operate on a vector?

The value-level functions you can call from GHCi like any other value-level functions. That'll first of all invoke any type-level computations that are necessary, and then run the typechecked code like you would run other Haskell code.

*Vector> :set -XDataKinds
*Vector> let v = 4 #: 9 #: 13 #:Nil

*Vector> :t v
v :: Num a => Vec a ('S ('S ('S 'Z)))
*Vector> v
Cons 4 (Cons 9 (Cons 13 Nil))

*Vector> let w = 7 #: 8 #: 6 #:Nil

*Vector> :t vAppend v w
vAppend v w :: Num a => Vec a ('S ('S ('S ('S ('S ('S 'Z))))))
*Vector> vAppend v w
Cons 4 (Cons 9 (Cons 13 (Cons 7 (Cons 8 (Cons 6 Nil)))))

To evaluate type families as type-level functions by themselves, use GHCi's :kind! command:

*Vector> :kind! Plus ('S 'Z) ('S ('S ('S 'Z)))
Plus ('S 'Z) ('S ('S ('S 'Z))) :: Nat
= 'S ('S ('S ('S 'Z)))

---

Why do they have to operate on the type level? What type do they operate on?

The purpose, in this example, of having them operate on the type level is that any length-mismatch errors should be caught by the compiler, not result in runtime errors. For example, you may want to write a function accepting two lists that are supposed to have the same length. This is then unsafe:

foo :: [a] -> [a] -> String

but this expresses exactly that the lengths must be identical:

foo' :: Vec a n -> Vec a n -> String

A concrete example is a zip. Prelude.zip does allow lists of different lengths but this means the longer list is basically trimmed to the length of the shorter, which may result in unexpected behaviour. With the Vector version

vZip :: Vec a n -> Vec b n -> Vec (a,b) n
vZip Nil Nil = Nil
vZip (Cons x xs) (Cons y ys) = Cons (x,y) $ vZip xs ys

this can't happen:

*Vector> vZip v w
Cons (4,7) (Cons (9,8) (Cons (13,6) Nil))

*Vector> vZip (vAppend v v) w
<interactive>:22:7: error:
    • Couldn't match type ‘'S ('S ('S 'Z))’ with ‘'Z’
      Expected type: Vec a ('S ('S ('S 'Z)))
        Actual type: Vec a (Plus ('S ('S ('S 'Z))) ('S ('S ('S 'Z))))
    • In the first argument of ‘vZip’, namely ‘(vAppend v v)’
      In the expression: vZip (vAppend v v) w
      In an equation for ‘it’: it = vZip (vAppend v v) w

Note that even if this expression were written somewhere deep down in a big program, you would immediately get the error at compile-time, instead of runtime problems sometime later on.

---

How do they evaluate the result?

It depends, and you don't really need to care, but the important bit is that the compiler weeds out anything that could go wrong^† and immediately gives you an error message. If all the type calculations are provably right, then the compiler hard-wires the code corresponding to those types into your program, erases the types themselves, and the runtime works essentially like in a Haskell program with plain old lists.

---

^†_{Sometimes unfortunately it will also give you an error message when the code is actually correct&safe, but the compiler can't prove it.}