Consider this definition of zip
for the usual vectors length indexed by Peano numerals:
{-# language DataKinds #-}
{-# language KindSignatures #-}
{-# language GADTs #-}
{-# language TypeOperators #-}
{-# language StandaloneDeriving #-}
{-# language FlexibleInstances #-}
{-# language FlexibleContexts #-}
module Vector
where
import Prelude hiding (zip)
data N
where
Z :: N
S :: N -> N
data Vector (n :: N) a
where
VZ :: Vector Z a
(:::) :: a -> Vector n a -> Vector (S n) a
infixr 1 :::
deriving instance Show a => Show (Vector n a)
class Zip z
where
zip :: z a -> z b -> z (a, b)
instance Zip (Vector n) => Zip (Vector (S n))
where
zip (x ::: xs) (y ::: ys) = (x, y) ::: zip xs ys
instance Zip (Vector Z)
where
zip _ _ = VZ
-- ^
-- λ :t zip (1 ::: 2 ::: 3 ::: VZ) (4 ::: 5 ::: 6 ::: VZ)
-- zip (1 ::: 2 ::: 3 ::: VZ) (4 ::: 5 ::: 6 ::: VZ)
-- :: (Num a, Num b) => Vector ('S ('S ('S 'Z))) (a, b)
-- λ zip (1 ::: 2 ::: 3 ::: VZ) (4 ::: 5 ::: 6 ::: VZ)
-- (1,4) ::: ((2,5) ::: ((3,6) ::: VZ))
Typing in unary numbers is wearysome (even though I have a macro for that). Fortunately, there is GHC.TypeLits
. Let us use it:
module Vector
where
import Prelude hiding (zip)
import GHC.TypeLits
data Vector (n :: Nat) a
where
VZ :: Vector 0 a
(:::) :: a -> Vector n a -> Vector (n + 1) a
infixr 1 :::
deriving instance Show a => Show (Vector n a)
class Zip z
where
zip :: z a -> z b -> z (a, b)
instance Zip (Vector n) => Zip (Vector (n + 1))
where
zip (x ::: xs) (y ::: ys) = (x, y) ::: zip xs ys
instance Zip (Vector 0)
where
zip _ _ = VZ
— But no:
• Illegal type synonym family application in instance:
Vector (n + 1)
• In the instance declaration for ‘Zip (Vector (n + 1))’
|
28 | instance Zip (Vector n) => Zip (Vector (n + 1))
| ^^^^^^^^^^^^^^^^^^^^
So I replace the class with an ordinary function:
zip :: Vector n a -> Vector n b -> Vector n (a, b)
zip (x ::: xs) (y ::: ys) = (x, y) ::: zip xs ys
zip VZ VZ = VZ
— But now I cannot make use of inductive reasoning anymore:
Vector.hs:25:47: error:
• Could not deduce: n2 ~ n1
from the context: n ~ (n1 + 1)
bound by a pattern with constructor:
::: :: forall a (n :: Nat). a -> Vector n a -> Vector (n + 1) a,
in an equation for ‘zip’
at Vector.hs:25:6-13
or from: n ~ (n2 + 1)
bound by a pattern with constructor:
::: :: forall a (n :: Nat). a -> Vector n a -> Vector (n + 1) a,
in an equation for ‘zip’
at Vector.hs:25:17-24
‘n2’ is a rigid type variable bound by
a pattern with constructor:
::: :: forall a (n :: Nat). a -> Vector n a -> Vector (n + 1) a,
in an equation for ‘zip’
at Vector.hs:25:17-24
‘n1’ is a rigid type variable bound by
a pattern with constructor:
::: :: forall a (n :: Nat). a -> Vector n a -> Vector (n + 1) a,
in an equation for ‘zip’
at Vector.hs:25:6-13
Expected type: Vector n1 b
Actual type: Vector n2 b
• In the second argument of ‘zip’, namely ‘ys’
In the second argument of ‘(:::)’, namely ‘zip xs ys’
In the expression: (x, y) ::: zip xs ys
• Relevant bindings include
ys :: Vector n2 b (bound at Vector.hs:25:23)
xs :: Vector n1 a (bound at Vector.hs:25:12)
|
25 | zip (x ::: xs) (y ::: ys) = (x, y) ::: zip xs ys
| ^^
Am I failing to observe something obvious? These TypeLits
cannot be useless?.. How is it supposed to work?
There is no induction on TypeLits
, which by default does make them nearly useless, but you can improve the situation in two ways.
Use ghc-typelits-natnormalise
. It's a GHC plugin which adds an arithmetic solver to the type checker, and causes GHC to consider many equal Nat
expressions equal. This is very convenient and is compatible with the next solution. Your zip
works with this out of the box.
Postulate whatever properties you need. You should only postulate proofs of true statements, and only proofs of equalities or other computationally irrelevant data types, in order to avoid potential memory safety issues. For example, your zip
works the following way:
{-# language
RankNTypes, TypeApplications, TypeOperators,
GADTs, TypeInType, ScopedTypeVariables #-}
import GHC.TypeLits
import Data.Type.Equality
import Unsafe.Coerce
data Vector (n :: Nat) a
where
VZ :: Vector 0 a
(:::) :: a -> Vector n a -> Vector (n + 1) a
lemma :: forall n m k. (n :~: (m + 1)) -> (n :~: (k + 1)) -> m :~: k
lemma _ _ = unsafeCoerce (Refl @n)
vzip :: Vector n a -> Vector n b -> Vector n (a, b)
vzip VZ VZ = VZ
vzip ((a ::: (as :: Vector m a)) :: Vector n a)
((b ::: (bs :: Vector k b)) :: Vector n b) =
case lemma @n @m @k Refl Refl of
Refl -> (a, b) ::: vzip as bs
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With