Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

How to define a usable Applicative instance for a vector type enforcing length 2^n

Tags:

haskell

For some application I need vectors of length $2^n$. To enforce that the lengths match for some operations, I defined my type with ist applicative instance as follows:

{-# LANGUAGE GADTs, DataKinds, FlexibleInstances, FlexibleContexts #-}
data Nat = Z | N Nat
data Vector n t where
  S :: t -> Vector Z t
  V :: Vector n t -> Vector n t -> Vector (N n) t

instance Functor (Vector n) where
  fmap f (S t ) = S (f t)
  fmap f (V t t') = V (fmap f t) (fmap f t')

instance Applicative (Vector Z) where
  pure = S
  S f <*> S a = S (f a)

instance Applicative (Vector n) => Applicative (Vector (N n)) where
  pure a = let a' = pure a in V a' a'
  V f f' <*> V a a' = V (f <*> a) (f' <*> a')

The language extensions I chose as suggested by ghci to make the code compile. The whole structure is inspired by How to make fixed-length vectors instance of Applicative?.

Trouble starts when I try to use it:

instance Num t => Num (Vector n t) where
  v + v' = (+) <$> v <*> v'
  (*) = undefined
  abs = undefined
  signum = undefined
  fromInteger = undefined
  negate = undefined

Adding these lines Triggers following error:

• Could not deduce (Applicative (Vector n)) arising from a use of ‘<*>’ from the context: Num t bound by the instance declaration at ...

• In the expression: (+) v <> v' In an equation for ‘+’: v + v' = (+) v <> v' In the instance declaration for ‘Num (Vector n t)’

I'm using Haskell Platform 8.0.2-a on Windows 7.

Any idea what's going? In the linked question the same trick seems to work!? (Adding KindSignatures in the first line does not help, and without FlexibleInstances/Contexts I get a Compiler error.)

like image 288
John Poe Avatar asked May 17 '19 10:05

John Poe


2 Answers

You should add a type constraint in your Num (Vector n t) instance declaration, that specifies that Vector n a is an instance of Applicative, otherwise you can not use (<*>) here.

You thus can fix the problems with:

instance (Num t, Applicative (Vector n)) => Num (Vector n t) where
  v + v' = (+) <$> v <*> v'
  -- ...

We here thus say that Vector n t is an instance of Num given t is an instance of Num, and Vector n is an instance of Applicative.

Since you defined your instance Applicative for your Vector n in such way that it holds for all ns, all Vector n ts are members of Num given Num t, regardless of the value for n, but it needs to be part of the signature of the instance declaration.

like image 181
Willem Van Onsem Avatar answered Nov 19 '22 01:11

Willem Van Onsem


I think it's a bit nicer to use an auxiliary class. I also tend to prefer liftA2 to <*> for instances, so I'll use that; it's not essential. Note that you only need to differentiate between sizes for pure; the zipping operation doesn't need that. There's a trade-off: if you make the zipping operation a method, then it'll tend to inline, whereas if it's a function it generally won't. This could balance code size against speed when the vectors are small enough. Still, this is how I'd probably do it.

class App' n where
  pure' :: a -> Vector n a

instance App' 'Z where
  pure' = S

instance App' n => App' ('N n) where
  pure' a = let a' = pure' a in V a' a'

liftA2'
  :: (a -> b -> c)
  -> Vector n a
  -> Vector n b
  -> Vector n c
liftA2' f = \xs -> go xs
  where
    go (S x) (S y) = S (f x y)
    go (V l1 r1) (V l2 r2) =
      V (go l1 l2) (go r1 r2)

instance App' n => Applicative (Vector n) where
  pure = pure'
  -- import Control.Applicative to get the liftA2 method
  liftA2 = liftA2'
like image 2
dfeuer Avatar answered Nov 19 '22 00:11

dfeuer