Sing.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators, NoStarIsType #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
module Sing where
import qualified Data.Singletons.Prelude as S
import qualified Data.Singletons.TypeLits as S
import GHC.TypeNats
import Data.Type.Equality
import Unsafe.Coerce
import Data.Proxy

data NatCons (n :: Nat) where
  Zero :: NatCons 0
  Succ :: KnownNat m => Proxy m -> NatCons (1 + m)

{-# NOINLINE isZero #-}
isZero :: (1 <=? n) :~: 'False -> n :~: 0
isZero Refl = unsafeCoerce Refl

natCons :: forall n. KnownNat n => Proxy n -> NatCons n
natCons _proxy =
  case S.sing @1 S.%<=? S.sing @n of
    S.SFalse -> case isZero @n Refl of Refl -> Zero
    {-
    -- without GHC.TypeLits.KnownNat.Solver:
    S.STrue -> case S.sing @n S.%- S.sing @1 of
      (S.SNat :: S.SNat m) -> Succ (Proxy @m)
    -}
    -- with GHC.TypeLits.KnownNat.Solver:
    S.STrue -> Succ (Proxy @(n - 1))

SizedVect.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators, NoStarIsType #-}
{-# LANGUAGE DataKinds #-}
import qualified Data.Vector.Sized as V
import GHC.TypeNats
import Data.Type.Equality
import Unsafe.Coerce
import Data.Proxy

data NatCons (n :: Nat) where
  Zero :: NatCons 0
  Succ :: KnownNat m => Proxy m -> NatCons (1 + m)

{-# NOINLINE natCons #-}
natCons :: KnownNat n => Proxy n -> NatCons n
natCons proxy = case sameNat proxy (Proxy :: Proxy 0) of
                  Just Refl -> Zero
                  Nothing -> case someNatVal (natVal proxy - 1) of
                               SomeNat proxy' -> unsafeCoerce (Succ proxy')

raccum :: (KnownNat m, Num a) => V.Vector m a -> V.Vector m a
raccum v = case natCons (V.length' v) of
             Zero -> v
             Succ proxy -> V.cons (V.sum v) (raccum $ V.tail v)

main :: IO ()
main = case V.fromList [3,1,4,1] of
         Just v -> print (raccum v :: V.Vector 4 Int)
         Nothing -> return ()