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.
For completeness, I put together an example using just base, no singletons:
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE PatternSynonyms #-}
import GHC.TypeLits (OrderingI (EQI, GTI, LTI))
import GHC.TypeNats (type (+), type (-), Nat, KnownNat (natSing), Natural, type (<=), cmpNat, CmpNat, withSomeSNat, natVal, pattern SNat, SNat)
import Data.Kind (Type)
import Unsafe.Coerce (unsafeCoerce)
import Data.Void (Void, absurd)
import Data.Type.Equality ((:~:) (Refl))
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)
vectOf :: forall (n :: Nat) a. KnownNat n => a -> Vect n a
vectOf a =
-- Compare @n@ and 0.
case cmpNat (natSing @n) (natSing @0) of
-- In this case, @n@ is 0, so we need to return @Vect 0 a@.
EQI -> VNil
-- In this case, @n@ is less than 0. We know this can't be the case
-- since @n@ is a Nat, and Nats can't be less than zero.
LTI -> absurd $ nothingLessThanZero @n
-- In this case @n@ is greater than 0.
GTI ->
-- Given that @n@ is greater than 0, we need to generate @m@, which is
-- equal to @n - 1@.
case natGtZero @n of
SNat @m ->
let
-- Call 'vectOf' recursively to generate @Vect m a@.
vectm = (vectOf @m a :: Vect m a)
-- At this point, GHC knows that @m@ is equal to @n - 1@, so
-- GHC can tell that @vectm@ has type @Vect (n - 1) a@.
vectnSubOne = vectm :: Vect (n - 1) a
-- Add an additional element onto the end of @vectnSubOne@. This gives
-- us a @Vect (m + 1) a@, or @Vect ((n - 1) + 1) a@. We, as the
-- programmer, know that this is the same as @Vect n a@, but GHC
-- does not yet know this.
vectn = VCons a vectnSubOne :: Vect ((n - 1) + 1) a
in
-- At this point, we have a value of @Vect ((n - 1) + 1) a@, and we
-- know that @n@ is greater than 0. It is obvious by simple facts
-- about addition that this is the same as @Vect n a@, but we have to
-- make GHC aware of this fact.
case minusOnePlusOne @n of
Refl -> vectn
-- | This function says:
--
-- > It is not true that that @n@ is both less than 0 and a nat. (Nats cannot
-- > be less than 0)
nothingLessThanZero :: forall n. (CmpNat n 0 ~ 'LT, KnownNat n) => Void
nothingLessThanZero = unsafeCoerce (\case{})
-- | This function says:
--
-- > Given a Nat @n@, and proof that @n@ is greater than 0, we can produce a
-- > Nat that is one less than @n@.
natGtZero :: forall n. (KnownNat n, CmpNat n 0 ~ 'GT) => SNat (n - 1)
natGtZero = withSomeSNat (natVal (SNat @n) - 1) unsafeCoerce
-- | This is a simple mathematical lemma about addition and subtraction. This
-- says:
--
-- > Given a Nat @n@, and proof that @n@ is greater than 0, we know that
-- > @(n - 1) + 1 = n@.
--
-- Why do we need proof that @n@ is greater than 0? Because if @n@ is
-- 0, then @((n - 1) + 1)@ becomes @((0 - 1) + 1)@, which simplifies to @(0 + 1)@,
-- which is equal to 1, not 0 as the equation suggests.
minusOnePlusOne :: forall n. (CmpNat n 0 ~ 'GT) => (n - 1) + 1 :~: n
minusOnePlusOne = unsafeCoerce (Refl @99)
This can be run the following environment:
$ nix-shell -I nixpkgs=https://github.com/NixOS/nixpkgs/archive/405d3d38b3f21b05be5344b0dbf31aafc1e72659.tar.gz -p haskell.compiler.ghc96 -p haskell.packages.ghc96.haskell-language-server
$ ghci my-dependent-vector.hs
> :set -XDataKinds
> vectOf @4 "hello"
VCons "hello" (VCons "hello" (VCons "hello" (VCons "hello" VNil)))
A few comments:
-
In some ways,
cmpNatisn’t the best function to use when you just want to figure out if something is zero or greater than zero. It may be slightly nicer to define your owncmpNatfunction that made more sense for this use-case. If you look at the source code ofcmpNat, it should be pretty straightforward on how to do this. -
You can use the helper functions from
constraintsin order to easily introduce and eliminate constraints, as @Bj0rn suggests in How to create Arbitrary instance for dependent types? - #23 by Bj0rn. I would of course advise against doing this when you’re just learning, since the code can get quite “golfy”. -
Again, as @Bj0rn suggests, you can use the various proofs about Nats provided by
constraintsinstead of defining them yourself: Data.Constraint.Nat. If you’re just learning, I’d recommend trying to write them yourself as a good learning experience.
6 Likes
Nice! This version is very clear.
1 Like
Thank you @cdepillabout ! With your help, I manage to have a complete example with the additional dependency of constraints only, where the only “magic” I have to include is a proof of nat_gte that does not come from constraints library:
This is a cabal run friendly script, you can run like this:
$ cabal run arbitrarynvec.hs
#!/usr/bin/env cabal
{- cabal:
default-language: GHC2021
ghc-options: -Wall
build-depends: base, constraints, QuickCheck
-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE GADTs #-}
import Data.Constraint (Dict (Dict), (:-) (Sub), (\\))
import Data.Constraint.Nat (minusNat)
import Data.Kind (Type)
import Data.Type.Ord (Compare)
import GHC.TypeLits (KnownNat, Nat, OrderingI (..), cmpNat, natSing, type (+), type (-), type (<=))
import Test.QuickCheck (Arbitrary (..), Gen, sample)
import Unsafe.Coerce (unsafeCoerce)
-- | A version of lenght indexed vector.
data Vect :: Nat -> Type -> Type where
VNil :: Vect 0 a
-- NOTE: Using ~(n - 1)~ to makes sure that there is an evidence of ~1 <= n~
VCons :: a -> Vect (n - 1) a -> Vect n a
deriving instance Show a => Show (Vect n a)
-- | Provide axiomatic proof, make sure you wrote it on paper!
axiom :: Dict c
axiom = unsafeCoerce (Dict :: Dict ())
-- | Axiom: For natural numbers, if m > n then n + 1 <= m.
--
-- Note: 1) more unmerged axioms available at: https://github.com/ekmett/constraints/issues/63, e.g. flipGT ltIsSuccLe.
-- 2) To avoid introducing AllowAmbiguousTypes in this small example, proxy types are used instead.
nat_gt_is_flipsucclte :: forall proxy1 proxy2 (m :: Nat) (n :: Nat) . proxy1 m -> proxy2 n -> (Compare m n ~ 'GT) :- (n + 1 <= m)
nat_gt_is_flipsucclte _ _ = Sub axiom
-- | Helper function to generate arbitrary values for a lenght-n vector.
vect_n_of :: forall {a} (n :: Nat) . KnownNat n => Gen a -> Gen (Vect n a)
vect_n_of g = case cmpNat (natSing @n) (natSing @0) of
EQI -> pure VNil -- Note: with the cmpNat pattern matching, GHC has no trouble to infer ~KnownNat 0~.
GTI -> -- Note: in order to use recursively call ~vect_n_f~, we must prove ~KnownNat (n - 1)~.
-- -- We can either use 'withDict', or its operator form '\\'. Note the order of '\\' when chaining evidences.
--
-- Alternatively:
-- ~withDict (nat_gt_is_flipsucclte @n @0) $ withDict (minusNat @n @1) $~
VCons <$> g <*> vect_n_of g
-- Note: with the evidence 1<=n, we can prove n-1 is KnownNat too.
\\ minusNat @n @1
-- Note: now we have evidence that ~(Compare n 0 ~ GT)~ (n>0), let's hand wave and prove 1<=n.
\\ nat_gt_is_flipsucclte (natSing @n) (natSing @0)
LTI -> error "Nothing less than zero"
instance (KnownNat n, Arbitrary a) => Arbitrary (Vect n a) where
-- arbitrary :: Gen (Vect n a)
arbitrary = vect_n_of @n arbitrary
main :: IO ()
main = do
sample (arbitrary :: Gen (Vect 0 ()))
sample (arbitrary :: Gen (Vect 1 Int))
sample (arbitrary :: Gen (Vect 2 Float))
sample (arbitrary :: Gen (Vect 4 String))
Example output:
VNil
VNil
VNil
VNil
VNil
VNil
VNil
VNil
VNil
VNil
VNil
VCons 0 VNil
VCons 2 VNil
VCons (-1) VNil
VCons (-2) VNil
VCons 4 VNil
VCons (-4) VNil
VCons 7 VNil
VCons (-9) VNil
VCons (-10) VNil
VCons 3 VNil
VCons 18 VNil
VCons 0.0 (VCons 0.0 VNil)
VCons 1.0 (VCons 1.0 VNil)
VCons 3.0 (VCons 4.0 VNil)
VCons 0.9176629 (VCons (-1.0) VNil)
VCons 2.6666667 (VCons 0.95433694 VNil)
VCons 4.7777777 (VCons 2.0 VNil)
VCons (-1.5) (VCons 0.5 VNil)
VCons 12.571428 (VCons 7.0 VNil)
VCons (-0.46153846) (VCons (-15.357142) VNil)
VCons (-2.0) (VCons 6.4545455 VNil)
VCons (-4.0) (VCons (-1.5) VNil)
VCons "" (VCons "" (VCons "" (VCons "" VNil)))
VCons "\b\160027" (VCons ";" (VCons "/o" (VCons "\641" VNil)))
VCons "Y\154730\DC4" (VCons "\1027113" (VCons "8\1022520Y" (VCons "" VNil)))
VCons "^/\157482\44110" (VCons "w\t\EOT9$E" (VCons "\1004373\NULu" (VCons "" VNil)))
VCons "%zi#p=" (VCons "" (VCons "\998804@\r" (VCons "^\1088217&Vb\1044702l" VNil)))
VCons "\1062651NKq8\t\1049501zx" (VCons "\1088809H'P4" (VCons "2n " (VCons "\DC3\1109479\&0\1108971\DC3\1033951h^\1065521" VNil)))
VCons "$v\54208\STX$" (VCons "{\1062731r\1102472)\45437u" (VCons "%4k" (VCons "\63422" VNil)))
VCons "\177792\EOT\49494\GS" (VCons "\NUL`\STXLb;t\n\DC1C\66700s" (VCons ",q" (VCons "\NUL>]U'&" VNil)))
VCons "\SUB\135831\4839l\14639b\RS\1063068K\CAN2Z)Vu\983110" (VCons "d\985391\SI\DC3I" (VCons "T\n%<\f[K\15156\&4\184744:v\59060\1065295\1098885\ETB" (VCons "\ri\171545\DC2o\a;\989009z\15146\&0zgB\64127\&0" VNil)))
VCons "\SYN:\DEL|" (VCons "" (VCons "&\nEk\62663n&(n" (VCons "" VNil)))
VCons "\39888\ESC\138225\37996r" (VCons "tML >{\162073]t\183124%A\n;{hu" (VCons "" (VCons "h{P\vE\1006239~J\CAN\1002613\CANIy\1036496ix\1044908\1043368v " VNil)))
3 Likes
Thanks, all. There is a lot happening here, and I haven’t quite processed it yet.
In the example by hellwolf, would it be possible to have something like this at the end?
main :: IO ()
main = do
n <- arbitrary
sample (arbitrary :: Gen (Vect n Int))
Not correct Haskell, obviously, but I want QuickCheck to be able to decide what value of n to use.
My understanding is that, fundamentally, you are asking for a compile-time unknown number. As the name suggests in KnownNat, you can’t construct such Vect n Int in runtime.
Hence, as other people in thread have been suggesting, you should always create SomeVect, “some”* seems a naming convention indicating it is a demoted value which is only known in runtime. I think that naming convention may have come from the original singletons paper: https://richarde.dev/papers/2012/singletons/paper.pdf
Or put in another way, what you are looking for is equivalent to the built-in “vectorOf” from quikcheck, you would just need to provide a trivial conversion: [a] -> SomeVect a
Yes, you can. See my post about reifyNat. If you couldn’t create dependently-typed vectors with size only known at runtime they would be almost useless!
1 Like
Yes. Sorry I am still trying to develop my intuition around these, and I wiped my comments on that, and working on a version for what OP is asking for.
2 Likes
You got it, thanks @tomjaguarpaw for correcting my misunderstanding. I made a complete example working.
I did not use reifyNat, since it would introduce another library. Instead withSomeSNat from base suffices.
#!/usr/bin/env cabal
{- cabal:
default-language: GHC2021
ghc-options: -Wall
build-depends: base, constraints, QuickCheck
-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PatternSynonyms #-}
{-|
Origin: https://discourse.haskell.org/t/how-to-create-arbitrary-instance-for-dependent-types/6990/31
Problem: QuickCheck-style generator for arbitary Length-indexed vector.
The QuickCheck library provides a function 'vectorOf' with the following signature:
@
-- | Generates a list of the given length.
vectorOf :: Int -> Gen a -> Gen [a]
@
We trust the code generates a list of "a"s with the length provided. But can we do better to encode the length guarantee
in type?
We know how to define length-indexed vector, say @Vect :: Nat -> Type -> Type@. A QuickCheck generator for it could look
like:
@
-- | function to generate arbitrary values for a lenght-n vector.
vect_n_of :: forall {a} (n :: Nat) . KnownNat n => Gen a -> Gen (Vect n a)
@
Upon close inspection, we can see that the type information encodes that the generated vector is guaranteed to have n
elements. That is a step-up from its inferior 'vectorOf' variant. But the flip side is that it becomes harder to
construct the correct implementation of this type.
This annotated Haskell script (invokable with "cabal run") provides an example of how it should be implemented. It uses
the "constraints" library for the required machinery working with constraints, including arithmetic for 'KnownNat'.
-}
import Data.Constraint (Dict (Dict), (:-) (Sub), (\\))
import Data.Constraint.Nat (minusNat)
import Data.Kind (Type)
import Data.Type.Ord (Compare)
import GHC.TypeLits
( KnownNat
, Nat
, OrderingI (..)
, SNat
, cmpNat
, natSing
, pattern SNat
, type (+)
, type (-)
, type (<=)
, withSomeSNat
)
import Test.QuickCheck (Arbitrary (..), Gen, sample)
import Unsafe.Coerce (unsafeCoerce)
-- | A version of length indexed vector.
data Vect :: Nat -> Type -> Type where
VNil :: Vect 0 a
-- NOTE: Using @(n - 1)@ to makes sure that there is an evidence of @1 <= n@.
VCons :: a -> Vect (n - 1) a -> Vect n a
deriving instance Show a => Show (Vect n a)
-- | Provide axiomatic proof, make sure you wrote it on paper!
axiom :: Dict c
axiom = unsafeCoerce (Dict :: Dict ())
-- | Axiom: For natural numbers, if m > n then n + 1 <= m.
--
-- Note: 1) more unmerged axioms available at: https://github.com/ekmett/constraints/issues/63, e.g. flipGT ltIsSuccLe.
-- 2) To avoid introducing AllowAmbiguousTypes in this small example, proxy types are used instead.
nat_gt_is_flipsucclte :: forall proxy1 proxy2 (m :: Nat) (n :: Nat) . proxy1 m -> proxy2 n -> (Compare m n ~ 'GT) :- (n + 1 <= m)
nat_gt_is_flipsucclte _ _ = Sub axiom
-- | Helper function to generate arbitrary values for a lenght-n vector.
vect_n_of :: forall {a} (n :: Nat) . KnownNat n => SNat n -> Gen a -> Gen (Vect n a)
vect_n_of _ g = case cmpNat (natSing @n) (natSing @0) of
EQI -> pure VNil -- Note: with the cmpNat pattern matching, GHC has no trouble to infer @KnownNat 0@.
GTI -> -- Note: in order to use recursively call @vect_n_f@, we must prove @KnownNat (n - 1)@.
-- -- We can either use 'withDict', or its operator form '\\'. Note the order of '\\' when chaining evidences.
--
-- Alternatively:
-- @withDict (nat_gt_is_flipsucclte @n @0) $ withDict (minusNat @n @1) $@
VCons <$> g <*> vect_n_of (natSing @(n - 1)) g
-- Note: with the evidence 1<=n, we can prove n-1 is KnownNat too.
\\ minusNat @n @1
-- Note: now we have evidence that @(Compare n 0 ~ GT)@ (n>0), let's hand wave and prove 1<=n.
\\ nat_gt_is_flipsucclte (natSing @n) (natSing @0)
LTI -> error "Nothing less than zero"
instance (KnownNat n, Arbitrary a) => Arbitrary (Vect n a) where
-- arbitrary :: Gen (Vect n a)
arbitrary = vect_n_of (natSing @n) arbitrary
main :: IO ()
main = do
-- Trying some compile-time known nats...
putStrLn "> arbitrary :: Gen (Vect 0 ())"
sample (arbitrary :: Gen (Vect 0 ()))
putStrLn "> arbitrary :: Gen (Vect 1 Int)"
sample (arbitrary :: Gen (Vect 1 Int))
putStrLn "> arbitrary :: Gen (Vect 2 Float)"
sample (arbitrary :: Gen (Vect 2 Float))
putStrLn "> arbitrary :: Gen (Vect 1 String)"
sample (arbitrary :: Gen (Vect 4 String))
-- Now an user input nat...
putStrLn "> How many elements do you want?"
n <- readLn :: IO Integer
withSomeSNat n $ \case
-- Note: you have to use @SNat@ pattern matching to bring @n@ to the scope, since only @natSing@ can give the
-- evidence of @KnownNat n@.
(Just (SNat @n)) -> sample (arbitrary :: Gen (Vect n Char))
_ -> putStrLn "Not all integers are born SNats"
Example output:
...
> How many elements do you want??
5
VCons '\165348' (VCons '\SOH' (VCons '\1094401' (VCons 'P' (VCons '^' VNil))))
VCons 'O' (VCons '\ETX' (VCons '\156463' (VCons '\164606' (VCons 'l' VNil))))
VCons '{' (VCons 'L' (VCons 'P' (VCons 'n' (VCons 'e' VNil))))
VCons ':' (VCons 'W' (VCons '\SUB' (VCons '\202109' (VCons 'A' VNil))))
VCons '?' (VCons '+' (VCons 'j' (VCons '\b' (VCons '\DC4' VNil))))
VCons '\181578' (VCons 'R' (VCons 'i' (VCons '\RS' (VCons '\1078712' VNil))))
VCons '\6983' (VCons '1' (VCons ']' (VCons '\1075706' (VCons 'i' VNil))))
VCons 'Z' (VCons '\28601' (VCons 'd' (VCons '\41165' (VCons 'Z' VNil))))
VCons '#' (VCons 'h' (VCons '\172348' (VCons '\174228' (VCons 'r' VNil))))
VCons '^' (VCons '\STX' (VCons 'L' (VCons '\1006381' (VCons '*' VNil))))
VCons '\f' (VCons '7' (VCons '\22980' (VCons 'a' (VCons 'Y' VNil))))
3 Likes