import Test.QuickCheck
import GHC.TypeLits
import Data.Kind
data Vect :: Nat -> Type -> Type where
VNil :: Vect 0 a
VCons :: a -> Vect n a -> Vect (n + 1) a
I want to be able to write some QuickChecks about my values, so I want to write an Arbitrary instance.
sizedVect :: Int -> Gen a -> Gen (Vect n a)
sizedVect 0 _ = pure VNil
sizedVect n g = VCons <$> g <*> sizedVect (n - 1) g
instance Arbitrary (Vect n a) where
arbitrary :: Gen (Vect n a)
arbitrary = sized sizedVect
But it doesn’t work because, e.g, VNil does not have the type forall n . Vect n a, but Vect 0 a.
Perhaps I should be able to write something like this:
sizedVect :: (n :: Nat) -> Gen a -> Gen (Vect (n :: Nat) a)
arbitrary :: Gen (n :: Nat, Vect (n :: Nat) a)
This is like a Sigma type, but it is not clear to me how to write this type in Haskell syntax (and then how to write the QuickCheck tests)
Here’s a more complete solution. Does it do what you want?
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeApplications #-}
import Test.QuickCheck
import Data.Reflection
import GHC.TypeLits
import Data.Kind
import Data.Proxy
data SomeVect a where
SomeVect :: KnownNat n => Vect n a -> SomeVect a
example :: Arbitrary a => Gen (SomeVect a)
example = do
i <- arbitrary
reifyNat i $ \(_ :: Proxy n) -> do
v <- replicateV @n arbitrary
pure (SomeVect v)
----
data Vect (n :: Nat) (a :: Type) where
replicateV :: forall n m a. Monad m => m a -> m (Vect n a)
replicateV = undefined
Interesting. This is probably harder than I thought.
What is SNat n? And also what is KnownNat n? What user tomjaguarpaw seems very much like Sigma types but with these additional constructs.
I am not really sure what the connection with the enumeration concept here is. I watched about 5 minutes of the video. Also, shouldn’t it be relatively easy to express Sigma types in Agda since it is a language with first class support for dependent types.
To explain these concepts in more detail, you want a Sigma type
(n :: Nat, Vect (n :: Nat) a)
But we don’t have those in Haskell. Instead you can have a second class existential type by writing it as a GADT:
data SomeVect a where
SomeVect :: (n :: Nat) -> Vect (n :: Nat) a -> SomeNat a
-- ^ This is not yet valid Haskell!
But we don’t have dependent types either! Instead there is a singleton type SNat :: Nat -> Type that does a similar job. It’s called a “singleton” because there is one value of type SNat n for each literal type n :: Natural. Using SNat we can write the desired Sigma type equivalent as
data SomeVect a where
SomeVect :: SNat (n :: Nat) -> Vect (n :: Nat) a -> SomeNat a
-- ^ This is now valid Haskell
For convenience there is a class KnownNat (n :: Nat) where natSing :: SNat n. This makes the above type equivalent to
data SomeVect a where
SomeVect :: KnownNat (n :: Nat) => Vect (n :: Nat) a -> SomeNat a
In order to reify a value level Nat (or Integer) to a type level Nat we need to use reifyNat. That is we pass in an i :: Integer (actually I should have put a guard that it is non-negative) and we “get out” a type level n :: Nat.
I’ve never used Agda, but I guess in Agda SNat vanishes and reifyNat is roughly just function application.
I am still trying to wrap my head around the KnownNat constraint. What exactly is known about it?
Consider the following code. How do I make it typecheck?
data Vect :: Nat -> Type -> Type where
VNil :: Vect 0 a
VCons :: a -> Vect n a -> Vect (n + 1) a
data SomeVect a where
SomeVect :: KnownNat n => Vect n a -> SomeVect a
someVectCons :: a -> SomeVect a -> SomeVect a
someVectCons x (SomeVect xs) = SomeVect $ VCons x xs
The compiler says:
• Could not deduce (KnownNat (n + 1))
arising from a use of ‘SomeVect’
from the context: KnownNat n
bound by a pattern with constructor:
SomeVect :: forall (n :: Nat) a.
KnownNat n =>
Vect n a -> SomeVect a,
in an equation for ‘someVectCons’
at /Users/agnishom/code/stl-workspace/server/src/PatternMatching/MITL.hs:96:17-27
• In the first argument of ‘($)’, namely ‘SomeVect’
In the expression: SomeVect $ VCons x xs
In an equation for ‘someVectCons’:
someVectCons x (SomeVect xs) = SomeVect $ VCons x xs
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.
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 …
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.