Applicative instance of a vector with kind nats

Question

I'm playing around with kind nats for the moment and got stuck when trying to define an applicative instance of a vector data type.

A reasonable instance, I think, would be that pure 1 :: Vec 3 Int would give me a vector of length 3 all elements of the value 1 and the <*> operator would zip together functions with values.

The problem where I'm stuck is that it will be recursive but depending on the value of the nat kind.

As you see below I've used a lot of pragmas (I don't even know which are necessary) and a few tricks I found (n ~ (1 + n0) and OVERLAPPING pragmas) but none seems to work for me.

The question is if it possible to encode in Haskell and if it is, what have I missed?

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE InstanceSigs #-}

import GHC.TypeLits


data Vec :: (Nat -> * -> *) where
  Nil  :: Vec 0 a
  Cons :: a -> Vec n a -> Vec (1 + n) a

instance Functor (Vec n) where
  fmap f Nil = Nil
  fmap f (Cons a as) = Cons (f a) (fmap f as)

instance {-# OVERLAPPING #-} Applicative (Vec 0) where
  pure _ = Nil
  a <*> b = Nil

instance {-# OVERLAPPABLE #-} n ~ (1 + n0) => Applicative (Vec n) where
  pure :: n ~ (1 + n0) => a -> Vec n a
  pure v = Cons v (pure v :: Vec n0 a)

  (<*>) :: n ~ (1 + n0) => Vec n (a -> b) -> Vec n a -> Vec n b
  (Cons f fs) <*> (Cons v vs) = Cons (f v) (fs <*> vs :: Vec n0 b)

EDIT:

The error I get is:

Could not deduce (a ~ a1)
from the context (Functor (Vec n), n ~ (1 + n0))
  bound by the instance declaration at Vectors.hs:27:31-65
  ‘a’ is a rigid type variable bound by
      the type signature for pure :: (n ~ (1 + n0)) => a -> Vec n a
      at Vectors.hs:28:11
  ‘a1’ is a rigid type variable bound by
       an expression type signature: Vec n1 a1 at Vectors.hs:29:20
Relevant bindings include
  v :: a (bound at Vectors.hs:29:8)
  pure :: a -> Vec n a (bound at Vectors.hs:29:3)
In the first argument of ‘pure’, namely ‘v’
In the second argument of ‘Cons’, namely ‘(pure v :: Vec n0 a)’

The Applicative instance for Vec n is given on page 4 of the Hasochism paper, along with some discussion. Doesn't use TypeLits but it shouldn't be too hard to translate. — Benjamin Hodgson
@BenjaminHodgson, TypeLits have no inductive structure, so they may not really be viable option. — dfeuer

pigworker pigworker · Accepted Answer · 2015-10-25T16:55:18

There's more than one way to cook this Applicative instance. Benjamin's comment points to the way I usually do it. The way you're trying to do it makes sense, too. In principle, at least. I fear it will struggle in practice, because the TypeLits machinery doesn't know enough about numbers (yet). Here's the problem boiled down:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ScopedTypeVariables #-}

module AV where

import GHC.TypeLits

grumble :: forall (f :: Nat -> *) (n :: Nat)(j :: Nat)(k :: Nat).
           (n ~ (1 + j), n ~ (1 + k)) => f j -> f k
grumble x = x

gives

Could not deduce (j ~ k)
from the context (n ~ (1 + j), n ~ (1 + k))

It'll be awfully tricky to persuade GHC that the two tails have the same length in the case of Cons for <*> without the acknowledgement that 1 + is injective.

Applicative instance of a vector with kind nats

1 Answers