I tried to whip up an example of vectorOf'
for you. I’ve added a lot of comments, so hopefully it is clear what is going on.
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE ExplicitNamespaces #-}
import Test.QuickCheck (Gen)
import GHC.TypeLits (type (+), Nat, KnownNat, Natural)
import Data.Kind (Type)
import Data.Singletons.Decide ((:~:) (Refl), Decision (Proved, Disproved), (%~), Refuted)
import GHC.TypeLits.Singletons (SNat)
import Data.Singletons (sing, Sing, TyCon1, TyCon)
import Data.Singletons.Sigma (Sigma ((:&:)))
import Prelude.Singletons (PNum((-)), SNum ((%-)))
import Unsafe.Coerce (unsafeCoerce)
data SomeVect a where
SomeVect :: KnownNat n => Vect n a -> SomeVect a
deriving instance Show a => Show (SomeVect a)
data Vect :: Nat -> Type -> Type where
VNil :: Vect 0 a
VCons :: a -> Vect n a -> Vect (n + 1) a
deriving instance Show a => Show (Vect n a)
vectorOf' :: forall n a. SNat n -> a -> Vect n a
vectorOf' sn q =
-- First, we check whether @n@ is 0, or greater than 0.
case natIsGt0 sn of
-- If @n@ is 0, then we know we need to return @Vect 0 a@, which is of course
-- just 'VNil'.
Proved (Refl :: n :~: 0) -> VNil
-- If @n@ is greater than 0, then we get proof of this fact in the
-- @refuted@ variable.
Disproved (refuted :: Refuted (n :~: 0)) ->
-- Now, we can pass both @n@ and our proof of @n@ being greater than zero to
-- 'neq0', and we get back @m@, which is equal to @n - 1@.
case neq0 sn refuted of
(x :: SNat m) :&: Refl ->
let
-- Now we can build @Vect m a@ by calling 'vectorOf'' recursively.
vectM = vectorOf' x q :: Vect m a
-- Just need to add one more 'a' to the tip, and we get a
-- @Vect (m + 1) a@. We, as the programmer, know that
-- @m + 1 = n@, so @Vect (m + 1) a@ is the same thing as
-- @Vect n a@. So we should be able to directory return
-- @vectN@. However, GHC can't tell this fact is true yet.
vectN = VCons q vectM :: Vect (m + 1) a
in
-- The last step is to prove that @m + 1 = n@.
-- In our environment, we have the constraint floating around that says
-- @m ~ (n - 1)@. We also know that @n /= 0@. With these two facts in
-- hand, we use can 'minus1EqPlus1 to prove that @m + 1 = n@.
case minus1EqPlus1 refuted of
(Refl :: m + 1 :~: n) ->
-- After we've proven everything, GHC is finally happy and we can
-- return 'vectN'.
vectN
-- | This function determines whether or not a given @n@ is equal to zero, or
-- above zero.
--
-- This is important, because we need to take a different code path in 'vectorOf''
-- depending on whether or not the passed-in @n@ is zero.
natIsGt0 :: SNat n -> Decision (n :~: 0)
natIsGt0 sn = sn %~ (sing @0)
-- | This function basically says the following:
--
-- > If you pass in an @n@, and proof that it is not zero, then I can give you
-- > a Natural that is equal to @n - 1@.
neq0 :: SNat n -> Refuted (n :~: 0) -> Sigma Natural (TyCon ((:~:) (n - 1)))
neq0 sn _ = (:&:) (sn %- sing @1) Refl
-- | This function basically says the following:
--
-- > If you have an @m@ that is equal to @n - 1@, and you can prove that @n@
-- > is not equal to 0, then I can produce proof that @m + 1@ is equal to @n@.
--
-- Internally this function uses 'unsafeCoerce', because GHC is not yet smart
-- enough to be able to figure out this relationship between addition,
-- subtraction, and inequality to zero. There are however type checker plugins
-- and various Haskell libraries that you could likely use instead of doing
-- this yourself.
minus1EqPlus1 :: m ~ (n - 1) => Refuted (n :~: 0) -> m + 1 :~: n
minus1EqPlus1 _ = unsafeCoerce Refl
I’m running it in the following environment (I think you’re a Nix user, right??):
$ nix-shell -I nixpkgs=https://github.com/NixOS/nixpkgs/archive/405d3d38b3f21b05be5344b0dbf31aafc1e72659.tar.gz -p 'haskellPackages.ghcWithPackages (p: [p.singletons p.QuickCheck p.reflection p.constraints p.singletons-th p.singletons-base])' -p haskellPackages.haskell-language-server
$ ghci ./my-haskell-file.hs
> :set -XDataKinds
> import Data.Singletons
> vectorOf' (sing @4) "hello"
VCons "hello" (VCons "hello" (VCons "hello" (VCons "hello" VNil)))
There are definitely various ways to clean up this code. I’m also leaning hard into singletons
, but there are other (simpler?) ways to express this as well. Hopefully this is at least something to get you started with.
It seems the SomeVect doesn’t achieve what’s needed here yet?
In some ways, writing SNat n -> a -> Vect n a
is easier than Int -> a -> SomeVect a
, since you already have the SNat n
in the type signature, and you don’t have to wrap everything up in SomeVect
.
As others have said above, the difficulty here is that GHC doesn’t have much knowledge of how to work with Nats on the type level out of the box, so you’re forced to either use type-checker plugins, or manually prove things (as I’ve done above). This is somewhat annoying in practice.