Skip to content

Instantly share code, notes, and snippets.

@minoki

minoki/Sing.hs

Last active Dec 10, 2020
Embed
What would you like to do?
{-# 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))
{-# 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 ()
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment