Show how to use Sigma from singletons with type-indexed lists.

vect-with-sigma.hs

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeInType #-}

module VectStuff9 where

import Data.Constraint (Dict(Dict))
import Data.Kind (Type)
import Data.Proxy (Proxy(Proxy))
import GHC.Natural (Natural)
import Data.Singletons
       (Apply, Sing, SomeSing(SomeSing), TyFun, fromSing, sing, toSing)
import Data.Singletons.Prelude (PNum((-), (+)))
import Data.Singletons.Decide
       ((:~:)(Refl), Decision(Disproved, Proved), Refuted, (%~))
import Data.Singletons.Sigma (Sigma((:&:)))
import Data.Singletons.TypeLits (Nat, Sing(SNat))
import Unsafe.Coerce (unsafeCoerce)

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)

plusMinus1Law :: forall (n :: Nat) m. n :~: ((n - m) + m)
plusMinus1Law = unsafeCoerce Refl

data Magic = Magic Natural

natToSing :: forall (n :: Nat). Natural -> Sing n
natToSing = unsafeCoerce Magic

gtZeroMinusNat :: Sing n -> Refuted (n :~: 0) -> Sing (n - 1)
gtZeroMinusNat sNat _ = natToSing (fromSing sNat - 1)

replicateVec :: forall n a. Sing n -> a -> Vect n a
replicateVec sNatN a =
  case sNatN %~ (sing @_ @0) of
    Proved Refl -> VNil
    Disproved f ->
      case plusMinus1Law @n @1 of
        Refl ->
          case gtZeroMinusNat sNatN f of
            snatNMinus1 -> VCons a $ replicateVec snatNMinus1 a

testReplicateVec :: Vect 3 String
testReplicateVec = replicateVec (sing @_ @3) "hello"

data Foo a b (m :: TyFun Nat Type)

type instance Apply (Foo a b) (n :: Nat) = a n b

replicateVecSigma :: Natural -> Sigma Nat (Foo Vect String)
replicateVecSigma i =
  case toSing i of
    SomeSing snat -> snat :&: replicateVec snat "hello"

showSigmaVec :: Show a => Sigma Nat (Foo Vect a) -> IO ()
showSigmaVec (SNat :&: vec) = print vec

testSigmaVec :: IO ()
testSigmaVec = showSigmaVec $ replicateVecSigma 5