Also, how would you actually define replicateV? I would need to pattern match on n, but it isn’t actually available
Ah, that probably needs a KnownNat constraint too. KnownNat n => is exactly what allows you to pattern match on n.
1 Like
What’s known about it is its runtime representation, so you can pattern match/branch on it.
Yes, you may need a GHC plugin to solve these constraints. I can’t remember which one. Maybe this one:
I spent some time reading the blog posts about Singeltons
It seems that KnownNat n => and SNat n -> should be the same thing. However, I am confused.
I cannot seem to access the SNat type:
ghci> import GHC.TypeNats
ghci> :i Nat
type Nat :: *
type Nat = Natural
-- Defined in ‘GHC.TypeNats’
ghci> :i SNat
I also cannot get the witness from the KnownNat
ghci> :i KnownNat
type KnownNat :: Nat -> Constraint
class KnownNat n where
GHC.TypeNats.natSing :: GHC.TypeNats.SNat n
{-# MINIMAL natSing #-}
-- Defined in ‘GHC.TypeNats’
ghci> :t natSing
<interactive>:1:1: error: Variable not in scope: natSing
I imagine that the correct way to write the replicateV function would be like replicateV :: forall n m a. (Monad m, KnownNat n) => m a -> m (Vect n a) and I probably need to able to pattern match on the SNat witness so that I know how many times to repeat.
You probably don’t need the SNat itself. You should be able to access all its functionality through KnownNat. For example, to pattern match you use
natVal :: forall n proxy. KnownNat n => proxy n -> Integer
https://hackage.haskell.org/package/base-4.18.0.0/docs/GHC-TypeLits.html#v:natVal
What type constructor should I plugin for the variable proxy?
Easiest to use Data.Proxy.Proxy
I guess you’ll need an operator that can do a type level pred on a KnownNat constraint, and I don’t see where that is, but there must be one somewhere …
[EDIT: pred, not succ]
How would you get the value n :: Int from the value Proxy :: Proxy n?
Bind it in the type signature \(_ :: Proxy n) -> ...
You’ll need ScopedTypeVariables enabled (and exact behaviour may depend on GHC version, I’m not entirely sure.)
EDIT: Oh, to get the Int out (or rather Nat), just apply natVal, quoted above.
ignore my gibberish attempt
You probably need to enable a GHC plugin. I don’t know which one, but if you type “ghc plugins for type arithmetic” into your favourite search engine you will probably find some good candidates.
I recall watching Richard Eisenburg live coding this, e.g.: @rae: Type families help define functions over length-indexed vectors - YouTube https://github.com/goldfirere/video-resources/blob/main/2021-04-27-vectors/Vec.hs
I should give it a try too before I give up.
The linked typechecker plugin should help solve those trivial constraints, like KnownNat (n + 1), given KnownNat n. But a plugin is not a necessity.
The constraints library comes packed with many useful “proofs” about Nat arithmetic in the Data.Constraint.Nat module.
constraints defines its own concepts of Dicts (a constraint captured as a value) and :- (an “entailment” or implication; a :- b means that the constraint a “entails” the constraint b).
Those concepts may seem a bit abstract in the beginning. But let’s look at how we can use the library to solve the Could not deduce (KnownNat (n + 1)) issue.
Some necessary extensions:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
We need to produce a forall n. KnownNat n :- KnownNat (n + 1) value and then we need to “dispatch” it, so to speak, around the problematic expression.
For a first part, Data.Constraint.Nat has
plusNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n + m)
That’s what we need, with m ~ 1 (GHC finds the KnownNat 1 instance automatically).
The problematic expression from earlier was SomeVect on the rhs of
someVectCons x (SomeVect xs) = SomeVect $ VCons x xs
constraints has the \\ operator for “dispatching” an entailment. It’s used like this:
someVectCons x (SomeVect @n xs) = (SomeVect \\ plusNat @n @1) $ VCons x xs
And now it compiles!
2 Likes
... (SomeVect @n xs)
Didn’t know you can bind type variables in patterns like this. Which extension allows this?
1 Like
I think this feature was added rather silently with GHC 9.2. Here it is in the GHC user guide. No new extension was introduced for it, but both TypeApplications and ScopedTypeVariables must be enabled.
2 Likes
Still have trouble defining the dependent type alternative of
vectorOf :: Int -> Gen a -> Gen [a]
to, say
vectorOf' :: SNat n -> Gen a -> Gen (Vect n a)
where the type level information guarantee that output is corresponding to the input (compile time) known nat “n”. It seems the SomeVect doesn’t achieve what’s needed here yet?
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.
1 Like
Also, I’m not sure if anyone has brought it up yet, but when you’re trying to play around with dependently-typed vectors in Haskell, it can often be easier to index them in Peano numbers, because you can easily destructure them with case-statements. Most Haskellers are pretty familiar with this style of programming.
Here’s what this might look like:
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeFamilies #-}
import Data.Kind (Type)
data Peano = Z | S Peano deriving Show
data SPeano (n :: Peano) where
SZ :: SPeano 'Z
SS :: SPeano n -> SPeano ('S n)
data Vect :: Peano -> Type -> Type where
VNil :: Vect 'Z a
VCons :: a -> Vect n a -> Vect ('S n) a
deriving instance Show a => Show (Vect n a)
vectorOf' :: forall n a. a -> SPeano n -> Vect n a
vectorOf' q = \case
SZ -> VNil
SS (x :: SPeano m) ->
let vectm = vectorOf' q x :: Vect m a
vectn = VCons q vectm
in vectn
You can see this is much simpler than trying to use SNat, since you can’t easily destructure SNat.