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)))